The Boolean Satisfiability Problem (SAT)
Fundamental Algorithms for System Modeling, Analysis, and OptimizationEdward A. Lee, Jaijeet Roychowdhury, Sanjit A. SeshiaUC BerkeleyEECS 144/244Fall 2011Copyright 2010-11, E. A. Lee, J. Roychowdhury, S. A. Seshia, All rights reservedBoolean Satisfiability (SAT) Solving2The Boolean Satisfiability Problem (SAT) Given: A Boolean formula F(x1, x2, x3, ..., xn) Can F evaluate to 1 (true)? Is F satisfiable? If yes, return values to xi s (satisfying assignment) that make F true 3Why is SAT important? Theoretical importance: First NP-complete Problem (Cook, 1971) Many practical applications: Model Checking Automatic Test Pattern Generation Combinational Equivalence Checking Planning in AI Automated Theorem Proving Software Verification ...4An Example Inputs to SAT solvers are usually represented in CNF(a + b + c) (a + b + c) (a + b + c ) (a + b + c )5An Example Inputs to SAT solvers are usually represented in CNF(a+ b+ c) (a + b + c) (a+ b + c ) (a + b+ c )6Why CNF?
• Chronological Backtracking – Proposed in original DLL paper – Backtrack to highest (largest) decision level that has not been tried with both values • But does this decision level have to be the reason for the conflict? 32 ... • Backtracking is the reverse of BCP
Download The Boolean Satisfiability Problem (SAT)
Information
Domain:
Source:
Link to this page:
Please notify us if you found a problem with this document: