dpll (761B)
1 # DPLL 2 3 https://en.wikipedia.org/wiki/DPLL_algorithm 4 5 [algorithm] for [satisfiability_boolean] of [CNF] 6 7 - if there is an empty clause, return UNSAT 8 - if there are no clauses, return SAT with current assignment 9 - if there is a clause containing a single [literal], instantiate that literal ([unit_propagation]) 10 - if there is a [literal_pure] aka one that occurs with only one polarity, insantiate that literal 11 - otherwise, select a literal ([branching_rule]), and explore first one polarity, then another 12 13 Can be modified for [sharp_SAT], but: 14 15 - not possible to handle [literal_pure] in a special way 16 - must explore both values of the chosen [literal], not just one 17 - must count [free_variables] 18 19 Up: [algorithm] for [satisfiability_boolean] 20 21 See also: [CDCL]