SAT Paper Library

SAT Paper Library (For Internal Use)

Here is some of SAT papers we collected (mostly from SAT-LIB):

Bayardo Jr., R. J.; Schrag, R. C. Using CSP look-back techniques to solve real world SAT instances. In: Proc. of the 14th National Conf. on Artificial Intelligence, pp. 203-208, 1997.
[ SAT, complete algorithms, learning. ]
Barth, P. A Davis-Putnam Based Enumeration Algorithm for Linear pseudo-Boolean Optimization.
MPI Technical Report, MPI-I-95-2-003, 1995.
[ SAT, complete algorithms, Davis Putnam, constraint programming, 0-1 problems. ]
Barth, P.; Bockmayr, A. Modelling 0-1 problems in CLP(PB). MPI Technical Report, 1996.
[ Constraint programming, 0-1 problems. ]
Bockmayr, A.; Kasper, T. Pseudo-Boolean and Finite Domain Constraint Programming: A Case Study. MPI Technical Report, 1996.
[ Constraint programming, 0-1 problems. ]
Bayardo Jr., R. J.; Schrag, R. C. Using CSP look-back techniques to solve exceptionally hard SAT instances. In: Proc. of the Second Int'l Conf. on Principles and Practice of Constraint Programming (Lecture Notes in Computer Science 1118), pp. 46-60, Springer, 1996.
[ SAT, complete algorithms, learning. ]
Beringer, A.; Aschemann, G.; Hoos, Holger H.; Metzger, M.; Weiß, A. GSAT versus Simulated Annealing. In: Proc. of ECAI'94, pp. 130-134, John Wiley \& Sons, 1994.
[SAT, local search, random 3-sat, simulated annealing. ]
Cadoli, M.; Giovanardi, A.; Schaerf, M. Experimental Analysis of the Computational Cost of Evaluating Quantified Boolean Formulae. Proc. of AI*IA-97, Springer LNAI, 1997.
[ QSAT, algorithms, empirical analysis. ]
Cadoli, M.; Giovanardi, A.; Schaerf, M. An Algorithm to Evaluate Quantified Boolean Formulae. Proceedings of AAAI-98, July, 1998.
[ QSAT, algorithms. ]
Cadoli, M.; Schaerf, M.; Giovanardi, A.; Giovanardi, M. An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation. Technical report DIS 08-99, March 1999. Significantly extended version of AI*IA-97 and AAAI-98.
[ QSAT, algorithms, empirical analysis. ]
Clark, Dave; Frank, Jeremy; Gent, Ian; MacIntyre, Ewan; Tomov, Neven; Walsh, Toby. Local Search and the Number of Solutions. Proceedings of CP-96, 1996.
[ SAT, local search, search behaviour, search space analysis, empirical analysis. ]
Cook, S.A.; Mitchell, D.G. Finding Hard Instances of the Satisfiability Problem: A Survey . In: "Satisfiability Problem: Theory and Applications", DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997.
[ SAT, survey article, applications, hard instances. ]
Frank, J. Weighting for Godot: Learning heuristics for GSAT. J. Frank, Proc. AAAI-96.
[ SAT, local search algorithms, GSAT, clause weighting. ]
Freeman, J.W. Improvements to Propositional Satisfiability Search Algorithms . PhD thesis, The University of Pennsylvania, 1995.
[ SAT, complete algorithms, Davis Putnam. ]
Gent, I.; Walsh, T. An Empirical Analysis of Search in GSAT. Journal of Artificial Intelligence Research, Vol. 1, September 1993.
[ SAT, local search algorithms, GSAT. ]
Gent, Ian; MacIntyre, Ewan; Prosser, Patrick; Walsh, Toby. The Constrainedness of Search. Proceedings of AAAI-96, pages 246-252, 1996.
[ SAT, search, constrainedness, phase transition. ]
Gent, I.; Walsh, T. Towards an Understanding of Hill-climbing Procedures for SAT. Proceedings of AAAI-93.
[ SAT, local search algorithms, GenSAT. ]
Gent, I.; Walsh, T. Unsatisfied Variables in Local Search. In `Hybrid Problems, Hybrid Solutions' (Proceedings of AISB-95), Ed. J. Hallam, IOS Press, Amsterdam, 1995, pages 73-85.
[ SAT, local search algorithms, random walk. ]
Gent, Ian; Walsh, Toby. The SAT Phase Transition. Proceedings of ECAI-94, ed. A G Cohn, John Wiley & Sons, 105-109, 1994.
[ SAT, phase transition, random 3-sat. ]
Gent, Ian; Walsh, Toby. Easy Problems are Sometimes Hard. Artificial Intelligence, 70, 335-345, 1994.
[ SAT, phase transition, constant probability model. ]
Gent, Ian; Walsh, Toby. The Satisfiability Constraint Gap. Artificial Intelligence, 81 (1-2), 1996.
[ SAT, phase transition, random 3-sat. ]
Gent, Ian; Walsh, Toby. Beyond NP: the QSAT phase transition. Technical report, APES-05-1998, July 1998. To appear in Proceedings of AAAI-99.
[ QSAT, phase transition, empirical analysis. ]
Gent, Ian; Walsh, Toby. The Search for Satisfaction. Draft paper, 1999.
[ SAT, survey article. ]
Giunchiglia, F.; Sebastiani, R. Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. Proceedings of 13th International Conference on Automated Deduction (CADE-13), Lecture Notes on Artificial Intelligence series. New Brunswick, New Jersey, USA, 1996.
[ SAT, modal logic, complete algorithms. ]
Giunchiglia, F.; Sebastiani, R. A SAT-based decision procedure for ALC. Proceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning - KR'96, 1996.
[ SAT, modal logic, complete algorithms. ]
Giunchiglia, F; Roveri, M.; Sebastiani, R. A new method for testing decision procedures in modal and terminological logics. 1996 International Workshop on Description Logics - DL'96. Boston, MA, USA, 1996. Short version also published in Proceedings 14th International Conference on Automated Deduction (CADE-14) with the title "A new method for testing decision procedures in modal logics".
[ SAT, modal logic, complete algorithms. ]
Guerra e Silva, Luís; Marques-Silva, João P.; Silveira, Luís M.; Sakallah, Karem A. Timing Analysis Using Propositional Satisfiability. Proceedings of the IEEE International Conference on Electronics, Circuits and Systems (ICECS), September 1998.
[ SAT, applications, hardware. ]
Gu, J.; Purdom, P.W.; Franco, J.; Wah, B.W. Algorithms for the Satisfiability (SAT) Problem: A Survey . In: "Satisfiability Problem: Theory and Applications", DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, pp. 19-152, 1997.
[ SAT, survey article, algorithms. ]
Guerra e Silva, Luís; Marques-Silva, João P.; Silveira, Luís M.; Sakallah, Karem A. Realistic Delay Modeling in Satisfiability-Based Timing Analysis, Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS), May 1998.
[ SAT, applications, hardware. ]
Hogg, T.; Huberman, B. A.; Williams, C. Phase Transitions and the Search Problem. Tutorial paper, 1996.
[ SAT, search, phase transition. ]
Hoos, Holger H. SAT-Encodings, Search Space Structure, and Local Search Performance. In: Proc. of IJCAI'99, pp. 296-302, Morgan Kaufmann, 1999.
[SAT, local search, encodings, empirical analysis, search space analysis. ]
Hoos, Holger H. On the Run-time Behaviour of Stochastic Local Search Algorithms for SAT. In: Proc. of AAAI, pp. 661-666, MIT Press, 1999.
[SAT, local search, encodings, search behaviour, empirical analysis. ]
Hoos, Holger H. Stochastic Local Search - Methods, Models, Applications. PhD thesis, TU Darmstadt, 1998.
[ SAT, local search, random 3-sat, search behaviour, empirical analysis, parallel algorithms, applications, planning, search space analysis. ]
Hoos, Holger H.; Stützle, Thomas. Towards a Characterisation of the Behaviour of Stochastic Local Search Algorithms for SAT.. Artificial Intelligence, 112, 213-232, 1999.
[ SAT, phase transition, constant probability model. ]
Hoos, Holger H.; Stützle, Thomas Local Search Algorithms for SAT: An Empirical Evaluation.. To appear in Journal of Automated Reasoning, 2000.
[SAT, local search, search behaviour, empirical analysis.]
Hoos, Holger H.; Stützle, Thomas SATLIB: An Online Resource for Research on SAT.. In: SAT 2000, Ian Gent, Hans van Maaren, and Toby Walsh, editors, IOS Press. 2000.
[SAT, benchmark libraries, research resources.]
Hoos, Holger H. Solving Hard Combinatorial Problems with GSAT - A Case Study.. In: Proceedings of the German Conference on Artificial Intelligence (KI'96), pp. 197-212, LNCS 1138, 1996.
[SAT, local search, graph colouring.]
Jiang, Yueyun; Kautz, Henry; Selman, Bart. Solving Problems with Hard and Soft Constraints Using A Stochastic Algorithm for MAX-SAT". 1st International Joint Workshop on Artificial Intelligence and Operations Research, 1995.
[ MAX-SAT, applications, steiner trees. ]
Kautz, Henry; McAllester, David; Selman, Bart. Encoding Plans in Propositional Logic. Proceedings KR-96, 1996.
[ SAT, applications, planning. ]
Kautz, Henry; Selman, Bart. Planning as Satisfiability. Proceedings ECAI-92, 1992.
[ SAT, applications, planning. ]
Kautz, Henry; Selman, Bart. Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search. Proceedings AAAI-96, 1996
[ SAT, applications, planning. ]
Kautz, Henry; Selman, Bart. BLACKBOX: A New Approach to the Application of Theorem Proving to Problem Solving. Working notes of the Workshop on Planning as Combinatorial Search, held in conjunction with AIPS-98, Pittsburgh, PA, 1998.
[ SAT, applications, planning. ]
Kautz, Henry; Selman, Bart. The Role of Domain-Specific Knowledge in the Planning as Satisfiability Framework. Proceedings of AIPS-98, Pittsburgh, PA, 1998.
[ SAT, applications, planning. ]
Kautz, Henry; Selman, Bart; Jiang, Yueyun. General Stochastic Approach to Solving Problems with Hard and Soft Constraints". In The Satisfiability Problem: Theory and Applications, Dingzhu Gu, Jun Du, and Panos Pardalos (Eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, American Mathematical Society, 1997, pages 573-586.
[ MAX-SAT, applications, steiner trees. ]
Kim, S.; Zhang, H. ModGen: Theorem proving by model generation. Proc. of National Conference of American Association on Artificial Intelligence (AAAI-94), Seattle, WA. MIT Press, pp. 162-167.
[ SAT, First order logic, theorem proving, model generation. ]
Kirousis, L. M.; Kranakis, E.; Krizanc. D. A Better Upper Bound for the Unsatisfiability Threshold. Technical report TR-96-09, School of Computer Science, Carleton University, 1996.
[ SAT, phase transition, random 3-sat. ]
van Maaren, Hans. Highlights of Satisfiability Research in the Year 2000 - Preface. In: SAT 2000 - Highlights of Satisfiability Research in the Year 2000, Ian Gent, Hans van Maaren, and Toby Walsh, editors, IOS Press. 2000.
[ SAT, survey article. ]
Marques-Silva, João P. Search Algorithms for Satisfiability Problems in Combinational Switching Circuits. Ph.D. Dissertation, EECS Department, University of Michigan, May 1995.
[ SAT, applications, hardware. ]
Marques-Silva, João P. An Overview of Backtrack Search Satisfiability Algorithms. In: Fifth International Symposium on Artificial Intelligence and Mathematics, January 1998.
[ SAT, complete algorithms, Davis Putnam. ]
Marques-Silva, João P.; Sakallah, Karem A. Conflict Analysis in Search Algorithms for Propositional Satisfiability. In: Proceedings of the IEEE International Conference on Tools with Artificial Intelligence, November 1996.
[ SAT, complete algorithms, learning. ]
Marques-Silva, João P.; Sakallah, Karem A. Robust Search Algorithms for Test Pattern Generation. Proceedings of the IEEE Fault-Tolerant Computing Symposium, June 1997.
[ SAT, applications, hardware. ]
McAllester, D.; Selman, B.; Kautz, H. Evidence for Invariants in Local Search. Proc. AAAI-97, Providence, RI, 1997.
[ SAT, local search algorithms, WalkSAT. ]
Mitchell, David; Selman, Bart; Levesque, Hector. Hard and Easy Distribution of SAT Problems. Proceedings AAAI-92, 1992.
[ SAT, phase transition, random 3-sat. ]
Parkes, A.J.; Walser, J. Tuning Local Search for Satisfiability Testing. Proceedings of the 13th National Conference on Artificial Intelligence, Portland, OR, 1996.
[ SAT, local search, WalkSAT, empirical analysis, random-3-sat. ]
Rintanen, J. Improvements to the evaluation of quantified Boolean formulae. Proceedings of the 16th International Joint Conference in Artificial Intelligence, Stockholm, Sweden, August 1999.
[ QSAT, algorithms. ]
Rodosek, R. A New Approach on Solving 3-Satisfiability. In: Proceedings of the 3rd International Conference on Artificial Intelligence and Symbolic Mathematical Computation, pp. 197-212, LNCS 1138, Steyr, 1996.
[ SAT, complete algorithms, complexity analysis. ]
Selman, B.; Kautz, H. An Empirical Study of Greedy Local Search for Satisfiability Testing. Proc. AAAI-93.
[ SAT, local search algorithms, GSAT, clause weighting. ]
Selman, B.; Kautz, H. Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems. Proc. IJCAI-93.
[ SAT, local search algorithms, GSAT, random walk. ]
Selman, B.; Kautz, H.; Cohen, B. Local Search Strategies for Satisfiability Testing. Proceedings of 2nd DIMACS Challenge on Cliques, Coloring and Satisfiability, 1994.
[ SAT, local search algorithms, WalkSAT. ]
Selman, B.; Levesque, H.; Mitchell, D. GSAT - A New Method for Solving Hard Satisfiability Problems. Proceedings AAAI-92.
[ SAT, local search algorithms, GSAT. ]
Singer, Josh; Gent, Ian; Smaill, Alan. Backbone Fragility and the Local Search Cost Peak. Journal of Artificial Intelligence Research, Vol. 12, pp. 235-270, 2000.
[ SAT, local search, search behaviour, search space analysis, empirical analysis, phase transition, random 3-sat, WalkSAT. ]
Slaney, J.; Fujita, M.; Stickel, M. Automated reasoning and exhaustive search: quasigroup existence problems. Computers and Mathematics with Applications 29, 115-132, 1995.
[ SAT, applications, quasigroup existence. ]
Steinmann, Olaf; Strohmeier, Antje; Stützle, Thomas. Tabu Search vs. Random Walk. KI-97: Advances in Artificial Intelligence, Springer Verlag, LNCS, Vol. 1303, 1997
[ SAT, local search, tabu search, random walk, constraint satisfaction. ]
Uribe, T.E.; Stickel, M.E. Ordered binary decision diagrams and the Davis-Putnam procedure. Proceedings of the First International Conference on Constraints in Computational Logics, Munich, Germany, September 1994, 34-49.
[ SAT, complete algorithms, Davis Putnam, OBDDs. ]
Walser, Joachim. Solving Linear Pseudo-Boolean Constraint Problems with Local Search. Proceedings of the 14th National Conference on Artificial Intelligence, AAAI-97, Providence, RI, 1997.
[ SAT, local search, WalkSAT, constraint programming, 0-1 problems. ]
Zhang, H. SATO: An Efficient Propositional Prover. Proc. of International Conference on Automated Deduction (CADE-97), 1997.
[ SAT, complete algorithms, Davis Putnam. ]
Zhang, Hantao. Specifying Latin Square Problems in Propositional Logics.
[ SAT, applications, quasigroup existence. ]
Zhang, H.; Bonacina, Maria Paola. Cumulating Search in a Distributed Computing Environment: A Case Study in Parallel Satisfiability.. In: Proceedings of First Int. Symp. on Parallel Symbolic Computation, 1994.
[ SAT, complete algorithms, parallel algorithms. ]
Zhang, Hantao; Bonacina, Maria Paola; Hsiang, Jieh. PSATO: A Distributed Propositional Prover and Its Application to Quasigroup Problems. Journal of Symbolic Computation, 11, 1-18, 1996.
[ SAT, complete algorithms, parallel algorithms. ]
Zhang, Hantao; Hsiang, Jieh. Solving Open Quasigroup Problems by Propositional Reasoning.
[ SAT, applications, quasigroup existence. ]
Zhang, H.; Stickel, M. Implementing Davis-Putnam's method by tries. Technical Report, The University of Iowa, 1994.
[ SAT, complete algorithms, Davis Putnam. ]
Zhang, H.; Stickel, M. An efficient algorithm for unit-propagation. In: Proc. of the Fourth International Symposium on Artificial Intelligence and Mathematics. Ft. Lauderdale, Florida, 1996.
[ SAT, complete algorithms, Davis Putnam. ]