SAT solvers are tools that solve the “Boolean satisfiability problem” (malik:cacm:2009): finding a set of boolean variable values such that a boolean formula is true.
SAT is used to reason about hardware, to encode other problems (e.g., graph problems, etc.), in model checking, in SMT solvers and in many other applications.
todo:
- CACM overview malik:cacm:2009
- SAT competition website
- SMT solver
- DRAT
- Model counting
Notes related to SAT solver
Papers related to SAT solver
- Automated testing and debugging of SAT and QBF solvers [brummayer:sat:2010]
- Satisfiability modulo theories: Introduction and applications [demoura:cacm:2011]
- Efficient sampling of SAT solutions for testing [dutra:icse:2018]
- The human in formal methods [krishnamurthi:fm:2019]
- Boolean satisfiability from theoretical hardness to practical success [malik:cacm:2009]