Satisfiability (SAT) Solvers

Most SAT solvers use a Conjunctive Normal Form (CNF) representation of the Boolean formula. In CNF representation the formula is represented as a conjunction of clauses, each clause is a disjunction of literals, and a literal is a variable or its negation. Each clause must evaluate to true to satisfy the formula. There exist polynomial algorithms to transform an arbitrary propositional formula into a satisfiability equivalent CNF formula that is satisfiable if and only if the original formula is satisfiable. The SAT solver may be modified to work directly on the Boolean circuit representation. Most modern SAT solvers are based on the Davis-Putnam- Logemann-Loveland (DPLL) algorithm. The DPLL algorithm finds a solution if and only if the formula is satisfiable. However, modern SAT solvers use conflict analysis techniques to analyze the reasons for a conflict.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques
Formal Verification Example