Resolution and CDCL
Symptom SAT is NP-complete (T027). It is the NP-complete problem, the one everything else reduces to. The textbook conclusion is that you should avoid it. Meanwhile: a hardware verification team routinely discharges instances with two million variables and ten million clauses in under a minute. Package managers solve dependency resolution with SAT. Every bounded model checker (T049) is a SAT solver with a front end. The planning community abandoned custom search for SAT encodings and got faster. ...