22c:295 - Seminar on Artificial Intelligence

Propositional Satisfiability (and Beyond)

Spring 2003

Readings

All on-line papers are in PDF format or PS format.

[Aud02] A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions.
by Gilles Audemard et al. In Proc. 18th "Int. Conference of Automated Deduction, CADE'02." LNAI, Springer Verlag.

[Bar02] Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.
by C. Barrett et el. In Ed Brinksma and Kim Guldstrand Larsen, editors, 14th International Conference on Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science, pages 236-249. Springer-Verlag, 2002. Copenhagen, Denmark.

[Bay97] Using CSP Look-Back Techniques to Solve Real-World SAT Instances
by Roberto Bayardo et al. Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI'97), 1997.

[Bie99] Symbolic Model Checking without BDDs
by Armin Biere et al. Proceedings of TACAS'99, 1999.

[Bry86] Graph-Based Algorithms for Boolean Function Manipulation
by Randal E. Bryant. IEEE Transactions on Computers, Vol. C-35, No. 8, August, 1986.

[Dav60] A Computing Procedure for Quantification Theory
by Martin Davis and Hilary Putnam. Journal of the ACM (JACM), July 1960 Volume 7 Issue 3.

[Dav62] A machine program for theorem-proving
by Martin Davis, George Logemann and Donald Loveland. Communications of the ACM, July 1962 Volume 5 Issue 7.

[deMo02] Lazy Theorem Proving for Bounded Model Checking over Infinite Domains
by L. de Moura et al. Proc. of International Conference on Automated Deduction (CADE-18), 2002.

[Gol02] Berkmin: A fast and robust SAT-solver
by E. Goldberg and Y. Novikov. In Design, Automation, and Test in Europe (DATE '02), 2002.

[Lyn02] Efficient data structures for backtrack search SAT solvers
by Inês Lynce and João P. Marques-Silva. In Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT), 2002.

[Mos01] Chaff: Engineering an Efficient SAT Solver
by Matthew W. Moskewicz et al. Proceedings of the 38th Design Automation Conference (DAC'01), 2001.

[Pnu99] Deciding Equality Formulas by Small Domains Instantiations
by A. Pnueli et al. Proc. of International Conference on Computer Aided Verification (CAV'99), 1999.

[Pnu02] The Small Model Property: How small can it be?
by A. Pnueli et al. Information and Computation, Vol 178(1), Oct 2002, pages 279-293, 2002.

[Seb02] SAT: Propositional Satisfiability and Beyond
by Roberto Sebastiani. 14th European Summer School on Logic, Language and Information, 2002.
Outstanding tutorial on all the topics of this seminar. We will follow it closely.

[Sil96] GRASP-A New Search Algorithm for Satisfiability
by J. E. Marques Silva and Karem A. Sakallah. Proceedings of IEEE/ACM International Conference on Computer-Aided Design, 1996.

[Str02] On Solving Presburger and Linear Arithmetic with SAT
by. O. Strichman. Proc. of Formal Methods in Computer-Aided Design (FMCAD 2002), 2002.

[Tin01] Introduction to Propositional Logic
by Cesare Tinelli. Course notes for "22c:145-Artificial Intelligence", The University of Iowa, Fall 2001.

[Tin02] A DPLL-based Calculus for Ground Satisfiability Modulo Theories
by Cesare Tinelli. In Proceedings of the 8th European Conference on Logic in Artificial Intelligence (JELIA'02), 2002.

[Vor01] Logic in Computer Science
by Andrei Voronkov. Course notes for "CS 3181: Logic in Computer Science". The University of Manchester, 2001.
Excellent, very well written course notes. At least half of the chapters are relevant to this seminar and provide great background reading.

[Wol99] The LPSAT Engine and its Application to Resource Planning
by Steven A. Wolfman and Daniel S. Weld. In Proceedings of IJCAI-99, 1999.

[Zha94] Implementing the Davis-Putnam Algorithm by Tries
by Hantao Zhang and Mark E. Stickel. Technical Report, University of Iowa, 1994.

[Zha97] SATO: an Efficient Propositional Prover
by Hantao Zhang. Proceedings of the International Conference on Automated Deduction (CADE'97), 1997.

[Zha01] Efficient conflict driven learning in a Boolean satisfiability solver
by L. Zhang et al. Proceedings of the International Conference on Computer-Aided Design (ICCAD'01), 2001.

[Zha02] The Quest for Efficient Boolean Satisfiability Solvers
by L. Zhang and S. Malik. Proceedings of 18th International Conference on Computer Aided Deduction (CADE 2002), 2002.
Invited paper. Nice and recent, if skimpy, overview of the state of the art in DPLL-based SAT solvers

Last Updated: Apr 4, 2003

[Aud02]	A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. by Gilles Audemard et al. In Proc. 18th "Int. Conference of Automated Deduction, CADE'02." LNAI, Springer Verlag.
[Bar02]	Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. by C. Barrett et el. In Ed Brinksma and Kim Guldstrand Larsen, editors, 14th International Conference on Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science, pages 236-249. Springer-Verlag, 2002. Copenhagen, Denmark.
[Bay97]	Using CSP Look-Back Techniques to Solve Real-World SAT Instances by Roberto Bayardo et al. Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI'97), 1997.
[Bie99]	Symbolic Model Checking without BDDs by Armin Biere et al. Proceedings of TACAS'99, 1999.
[Bry86]	Graph-Based Algorithms for Boolean Function Manipulation by Randal E. Bryant. IEEE Transactions on Computers, Vol. C-35, No. 8, August, 1986.
[Dav60]	A Computing Procedure for Quantification Theory by Martin Davis and Hilary Putnam. Journal of the ACM (JACM), July 1960 Volume 7 Issue 3.
[Dav62]	A machine program for theorem-proving by Martin Davis, George Logemann and Donald Loveland. Communications of the ACM, July 1962 Volume 5 Issue 7.
[deMo02]	Lazy Theorem Proving for Bounded Model Checking over Infinite Domains by L. de Moura et al. Proc. of International Conference on Automated Deduction (CADE-18), 2002.
[Gol02]	Berkmin: A fast and robust SAT-solver by E. Goldberg and Y. Novikov. In Design, Automation, and Test in Europe (DATE '02), 2002.
[Lyn02]	Efficient data structures for backtrack search SAT solvers by Inês Lynce and João P. Marques-Silva. In Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT), 2002.
[Mos01]	Chaff: Engineering an Efficient SAT Solver by Matthew W. Moskewicz et al. Proceedings of the 38th Design Automation Conference (DAC'01), 2001.
[Pnu99]	Deciding Equality Formulas by Small Domains Instantiations by A. Pnueli et al. Proc. of International Conference on Computer Aided Verification (CAV'99), 1999.
[Pnu02]	The Small Model Property: How small can it be? by A. Pnueli et al. Information and Computation, Vol 178(1), Oct 2002, pages 279-293, 2002.
[Seb02]	SAT: Propositional Satisfiability and Beyond by Roberto Sebastiani. 14th European Summer School on Logic, Language and Information, 2002. Outstanding tutorial on all the topics of this seminar. We will follow it closely.
[Sil96]	GRASP-A New Search Algorithm for Satisfiability by J. E. Marques Silva and Karem A. Sakallah. Proceedings of IEEE/ACM International Conference on Computer-Aided Design, 1996.
[Str02]	On Solving Presburger and Linear Arithmetic with SAT by. O. Strichman. Proc. of Formal Methods in Computer-Aided Design (FMCAD 2002), 2002.
[Tin01]	Introduction to Propositional Logic by Cesare Tinelli. Course notes for "22c:145-Artificial Intelligence", The University of Iowa, Fall 2001.
[Tin02]	A DPLL-based Calculus for Ground Satisfiability Modulo Theories by Cesare Tinelli. In Proceedings of the 8th European Conference on Logic in Artificial Intelligence (JELIA'02), 2002.
[Vor01]	Logic in Computer Science by Andrei Voronkov. Course notes for "CS 3181: Logic in Computer Science". The University of Manchester, 2001. Excellent, very well written course notes. At least half of the chapters are relevant to this seminar and provide great background reading.
[Wol99]	The LPSAT Engine and its Application to Resource Planning by Steven A. Wolfman and Daniel S. Weld. In Proceedings of IJCAI-99, 1999.
[Zha94]	Implementing the Davis-Putnam Algorithm by Tries by Hantao Zhang and Mark E. Stickel. Technical Report, University of Iowa, 1994.
[Zha97]	SATO: an Efficient Propositional Prover by Hantao Zhang. Proceedings of the International Conference on Automated Deduction (CADE'97), 1997.
[Zha01]	Efficient conflict driven learning in a Boolean satisfiability solver by L. Zhang et al. Proceedings of the International Conference on Computer-Aided Design (ICCAD'01), 2001.
[Zha02]	The Quest for Efficient Boolean Satisfiability Solvers by L. Zhang and S. Malik. Proceedings of 18th International Conference on Computer Aided Deduction (CADE 2002), 2002. Invited paper. Nice and recent, if skimpy, overview of the state of the art in DPLL-based SAT solvers