Many problems in CS can be reduced to checking * satisfiability*
of a propositional calculus formula.

Two efficient algorithms for satisfiability checking (SAT):

- The Davis-Putnam or DPLL algorithm uses heuristics for
*early termination*(determining the value from a partially specified model),*pure symbols*(those that have the same sign in all clauses) and*unit clauses*(those with a single literal).The CHAFF inplementation of DPLL solves hardware verification problems with a million variables.

- The WalkSAT algorithm uses a combination of hill climbing (selecting a literal assignment that makes the most clauses true) and random steps.