dpll (934B)
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 You may be able to: 14 - detect [subformulae] that you have already seen 15 - detect when there are multiple [connected_components] to do a [decomposable_AND] 16 17 Can be modified for [sharp_SAT], but: 18 19 - not possible to handle [literal_pure] in a special way 20 - must explore both values of the chosen [literal], not just one 21 - must count [free_variables] 22 23 Up: [algorithm] for [satisfiability_boolean] 24 25 See also: [CDCL], [exhaustive_DPLL]