Hyojung Han
ABSTRACT
Satisfiability (SAT) solvers often benefit from a preprocessing of the formula to be decided. For formulae in conjunctive normal form (CNF), subsumed clauses may be removed or partial resolution may be applied. Preprocessing aims at simplifying the formula and at increasing the deductive power of the solver. These two objectives are sometimes competing. We present a new algorithm that combines simplification and increase of deductive power and we show its effectiveness in speeding up SAT solvers.
- A. V. Aho, J. E. Hopcroft, and J. D. Ullman. Data Structures and Algorithms. Addison-Wesley, Reading, MA, 1983. Google Scholar
Digital Library
- M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5:394--397, 1962. Google ScholarDigital Library
- M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7(3):201--215, July 1960. Google ScholarDigital Library
- N. Eén and A. Biere. Effective preprocessing in SAT through variable and clause elimination. In Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), St. Andrews, UK, June 2005. Springer-Verlag. LNCS 3569. Google ScholarDigital Library
- N. Eén and N. Sörensson. An extensible SAT-solver. In Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003), pages 502--518, S. Margherita Ligure, Italy, May 2003. Springer-Verlag. LNCS 2919.Google Scholar
- H. Jin, M. Awedh, and F. Somenzi. CirCUs: A satisfiability solver geared towards bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 519--522. Springer-Verlag, Berlin, July 2004. LNCS 3114.Google ScholarCross Ref
- H. Jin and F. Somenzi. An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science, 2004. Second International Workshop on Bounded Model Checking. http://www.elsevier.nl/locate/entcs/. Google ScholarDigital Library
- H. Jin and F. Somenzi. Strong conflict analysis for prepositional satisfiability. In Design, Automation and Test in Europe (DATE'06), pages 818--823, Munich, Germany, Mar. 2006. Google ScholarDigital Library
- J. P. Marques-Silva and K. A. Sakallah. GRASP-a search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506--521, 1999. Google ScholarDigital Library
- K. L. McMillan. Applying SAT methods in unbounded symbolic model checking. In E. Brinksma and K. G. Larsen, editors, Fourteenth Conference on Computer Aided Verification (CAV'02), pages 250--264. Springer-Verlag, Berlin, July 2002. LNCS 2404. Google ScholarDigital Library
- M. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference, pages 530--535, Las Vegas, NV, June 2001. Google ScholarDigital Library
- URL: http://www.lri.fr/simon/contest/results.Google Scholar
- URL: http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/MiniSat.html.Google Scholar
- N. Sörensson and N. Eén. MiniSat vl.13 - a SAT solver with conflict-clause minimization. In Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), St. Andrews, UK, June 2005. Springer-Verlag. LNCS 3569.Google Scholar
- URL: http://vlsi.colorado.edu/~vis.Google Scholar
- L. Zhang. On subsumption removal and on-the-fly CNF simplification. In Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), St. Andrews, UK, June 2005. Springer-Verlag. LNCS 3569. Google ScholarDigital Library
- L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. Efficient conflict driven learning in Boolean satisfiability solver. In Proceedings of the International Conference on Computer-Aided Design, pages 279--285, San Jose, CA, Nov. 2001. Google ScholarDigital Library
- Q. Zhu, N. Kitchen, A. Kuehlmann, and A. Sangiovanni-Vincentelli. SAT sweeping with local observability don't cares. In Proceedings of the Design Automation Conference, pages 229--234, San Francisco, CA, July 2006. Google ScholarDigital Library
Index Terms
- Alembic: an efficient algorithm for CNF preprocessing
Recommendations
Making deduction more effective in SAT solvers
Satisfiability (SAT) solvers often benefit from transformations of the formula to be decided that allow them to do more through deduction and decrease their reliance on enumeration. For formulae in conjunctive normal form, subsumed clauses may be ...
Prime clauses for fast enumeration of satisfying assignments to boolean circuits
DAC '05: Proceedings of the 42nd annual Design Automation ConferenceFinding all satisfying assignments of a propositional formula has many applications in the design of hardware and software. An approach to this problem augments a clause-recording propositional satisfiability solver with the ability to add blocking ...
A fast SAT solver algorithm best suited to reconfigurable hardware
SBCCI '06: Proceedings of the 19th annual symposium on Integrated circuits and systems designThe majority of the existing reconfigurable hardware SAT solvers employ some variation of the Davis-Putnam algorithm; we propose a new algorithm for organizing the search in SAT Solvers best suited to reconfigurable architectures due to its vector-like ...
Comments