008-a search algorithm for propositional satisfiability

This chapter is mainly about a search algorithm for propositional satisfiability, which mainly includes sat in a nutshell,problem representation,DLL algorithm,implications and boolean constraint propagation and so on.
展开查看详情

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.