008-a search algorithm for propositional satisfiability

1 .GRASP: A Search Algorithm for Propositional Satisfiability 

2 . Sat in a Nutshell • Given a Boolean formula, find a variable assignment such that the formula evaluates to 1, or prove that no such assignment exists. • For n variable,s there are 2n possible truth assignments to be checked. • NP-Complete problem. 

3 . Problem Representation • Conjunctive Normal Form – F = (a+b)(a’+b’+c) – Simple representation (more efficient data structures) • Logic circuit representation – Circuits have structural and direction information • Circuit –-> CNF conversion is straightforward 

4 . DLL Algorithm 

5 . DLL Algorithm • Davis, Logemann and Loveland – M. Davis, G. Logemann and D. Loveland, “A Machine Program for Theorem-Proving”, Communications of ACM, Vol. 5, No. 7, pp. 394-397, 1962 • Basic framework for many modern SAT solvers • Also known as DPLL for historical reasons • DFS – depth first search 

6 .

7 .

8 .

9 .

10 .

11 .

12 .

13 .

14 .

15 .

16 .

17 .

18 .

19 .

20 .

21 .

22 .

23 .

24 .

25 .

26 .

27 .

28 .Implications and Boolean Constraint Propagation 

29 . Implications and Boolean Constraint Propagation • Implication – A variable is forced to be assigned to be True or False based on previous assignments. • Unit clause rule (rule for elimination of one literal clauses) – An unsatisfied clause is a unit clause if it has exactly one unassigned literal. – The unassigned literal is implied because of the unit clause. • Boolean Constraint Propagation (BCP) – Iteratively apply the unit clause rule until there is no unit clause available • Workhorse of DLL based algorithms.