CMU CS 15414 - Chaff: Engineering an Efficient SAT Solver (38 pages)

Previewing pages 1, 2, 3, 18, 19, 36, 37, 38 of 38 page document View the full content.
View Full Document

Chaff: Engineering an Efficient SAT Solver



Previewing pages 1, 2, 3, 18, 19, 36, 37, 38 of actual document.

View the full content.
View Full Document
View Full Document

Chaff: Engineering an Efficient SAT Solver

68 views


Pages:
38
School:
Carnegie Mellon University
Course:
Cs 15414 - Bug Catching: Automated Program Verification and Testing

Unformatted text preview:

Chaff Engineering an Efficient SAT Solver Matthew W Moskewicz Concor F Madigan Ying Zhao Lintao Zhang Sharad Malik Princeton University Slides Tamir Heyman Some are from Malik s presentation Last modified by Will Klieber on Sep 7 2011 1 Boolean Algebra Notation denotes logical OR denotes logical AND Overbar or postfix denotes negation Example A B C corresponds to A B C 2 Chaff Philosophy Make the core operations fast profiling driven most time consuming parts Boolean Constraint Propagation BCP and Decision Emphasis on coding efficiency Emphasis on optimizing data cache behavior Search space pruning conflict resolution and learning 3 Chaff s Main Procedures Efficient BCP Efficient decision heuristic Two watched literals Fast backtracking Localizes search space Restarts Increases robustness 4 Implication What causes an implication When can it occur All literals in a clause but one are assigned False 5 Implication example The clause v1 v2 v3 implies values only in the following cases In case F F v3 In case F v2 F implies v3 T implies v2 T In case v1 F F implies v1 T 6 Implication for N literal clause Implication occurs after N 1 assignments to False to its literals We can ignore the first N 2 assignments to this clause The first N 2 assignments won t have any effect on the BCP 7 Watched Literals Each clause has two watched literals Ignore any assignments to the other literals in the clause BCP maintains the following invariant By the end of BCP one of the watched literals is true or both are unassigned Can watch a false literal only if other watch is true Guaranteed to find all implications found by normal unit prop 8 BCP with watched Literals Identifying conflict clauses Identifying unit clauses Identifying associated implications Maintaining BCP Invariant 9 Example 1 13 Input formula has the following clauses v2 v1 v1 v1 v3 v1 v4 v2 v3 v2 v4 v1 means v1 10 Example 2 13 Initially we identify any two literals in each clause as the watched on Watched literals v2 v1 v1



View Full Document

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Chaff: Engineering an Efficient SAT Solver and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Chaff: Engineering an Efficient SAT Solver and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?