Awesome SAT and SMT solving

• SAT.

SAT

Algorithms

• DP (1960).
• DPLL (1962).
• PPZ (1997).
• PPSZ (1998).
• Chaff (2001).
• Incremental SAT (2003).
• CDCL (conflict driven clause learning):
  • Interactive DPLL and CDCL explanation.

Solvers

• GSAT, WSAT (1993).
• GRASP (1995).
• SATO (1997).
• zChaff, mChaff (Chaff) (2001).
• SATZOO, SATNIK.
• MiniSAT (2003).

Input formats

• DIMACS-CNF.