| [1] |
Proceedings of the 39th Annual Symposium on Foundations of Computer
Science. (FOCS-98), Palo Alto, CA, November 1998. BibTeX entry |
| [2] |
Proceedings of the Seventeenth National Conference in Artificial
Intelligence (AAAI'00), Austin, Texas, USA, July 30-August 3 2000. BibTeX entry, Available here |
| [3] |
Parosh Aziz Abdulla, Per Bjesse, and Niklas Eén.
Symbolic Reachability Analysis Based on SAT-Solvers.
In Proceedings of the 6th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS'2000), 2000. BibTeX entry, PS |
| [4] |
Yuichi Asahiro, Kazuo Iwama, and Eiji Miyano.
Random generation of test instances with controlled attributes.
In Johnson and Trick [92], pages 377-393. BibTeX entry |
| [5] |
B. Aspvall, M. Plass, and R. Tarjan.
A linear-time algorithm for testing the truth of certain quantified
boolean formulas.
Information Processing Letters, 8:121-123, 1979. BibTeX entry |
| [6] |
Gilles Audemard, Belaid Benhamou, and Pierre Siegel.
La méthode d'avalanche AVAL : une méthode énumérative pour SAT.
In Actes des Cinquièmes Journées Nationales sur la Résolution
Pratique de Problèmes NP-Complets (JNPC'99), pages 17-25, Lyon, 1999. BibTeX entry |
| [7] |
Gilles Audemard, Belaid Benhamou, and Pierre Siegel.
AVAL: An enumerative method for SAT.
In Proceedings of the First international conference on
Computational Logic (CL'00), pages 373-383, Londres, July 2000. BibTeX entry |
| [8] |
Fahiem Bacchus.
Enhancing davis putnam with extended binary clause reasoning.
In Proceedings of National Conference on Artificial Intelligence
(AAAI-2002), 2002.
to appear. BibTeX entry, PDF |
| [9] |
Fahiem Bacchus.
Exploring the computational tradeoff of more reasoning and less
searching.
In Proceedings of Fifth International Symposium on Theory and
Applications of Satisfiability Testing, pages 7-16, 2002. BibTeX entry, PDF |
| [10] |
Olivier Bailleux and Pierre Marquis.
DISTANCE-SAT : complexité et algorithmes.
In Actes des Cinquièmes Journées Nationales sur la Résolution
Pratique de Problèmes NP-Complets (JNPC'99), pages 199-206, Lyon, 1999. BibTeX entry |
| [11] |
Olivier Bailleux and Pierre Marquis.
DISTANCE-SAT: Complexity and algorithms.
In Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99), pages 642-647, Orlando, Florida, 1999. BibTeX entry |
| [12] |
Luís Baptista and João P. Marques-Silva.
Using randomization and learning to solve hard real-world instances
of satisfiability.
In in Proceedings of the 6th International Conference on
Principles and Practice of Constraint Programming (CP), September 2000. BibTeX entry, Compressed PS |
| [13] |
Roberto J. Jr. Bayardo and Robert C. Schrag.
Using CSP look-back techniques to solve real-world SAT instances.
In Proceedings of the Fourteenth National Conference on
Artificial Intelligence (AAAI'97), pages 203-208, Providence, Rhode Island,
1997. BibTeX entry, Compressed PS |
| [14] |
Belaïd Benhamou and Lakhdar Saïs.
Tractability through symmetries in propositional calculus.
Journal of Automated Reasoning, 12:89-102, 1994. BibTeX entry |
| [15] |
Belaid Benhamou, Lakhdar Sais, and Pierre Siegel.
Two proof procedures for a cardinality based language in
propositional calculus.
In Proceedings of the Eleventh Annual Symposium on Theoretical
Aspects of Computer Science (STACS), volume 775 de Lecture Notes in Computer
Science, pages 71-82, Caen (France), 1994. Springer Verlag. BibTeX entry |
| [16] |
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, M. Fujita, and Y. Zhu.
Symbolic model checking using SAT procedures instead of bdds.
In Proceedings of Design Automation Conference (DAC'99), 1999. BibTeX entry, Compressed PS |
| [17] |
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Y. Zhu.
Symbolic Model Checking without BDDs.
In Proceedings of Tools and Algorithms for the Analysis and
Construction of Systems (TACAS'99), number 1579 in LNCS, 1999. BibTeX entry, Compressed PS |
| [18] |
A. Billionnet and A. Sutter.
An efficient algorithm for the 3 satisfiability problem.
Operation Research Letters, 12:29-36, 1992. BibTeX entry |
| [19] |
Yacine Boufkhad.
Aspects probabilistes et algorithmiques du problème de
satisfiabilité.
PhD thesis, Thèse de doctorat de l'Université de Paris 6, 1996. BibTeX entry |
| [20] |
Yacine Boufkhad, Eric Grégoire, Pierre Marquis, Bertrand Mazure, and Lakhdar
Saïs.
Tractable cover compilations.
In IJCAI97 [86], pages 122-127. BibTeX entry |
| [21] |
Ronen I. Brafman.
A simplifier for propositional formulas with many binary clauses.
Technical Report 00-04, Departement of Computer Science, Ben-Gurion
University, Beer-Sheva, Israel, 2000. BibTeX entry |
| [22] |
Ronen I. Brafman.
A simplifier for propositional formulas with many binary clauses.
In IJCAI01 [84]. BibTeX entry, PS |
| [23] |
Laure Brisoux-Devendeville.
Satisfaisabilité propositionnelle en informatique : aspects
algorithmiques et extensions du formalisme.
PhD thesis, Thèse de doctorat de l'Université d'Artois, Lens, 1999. BibTeX entry |
| [24] |
R. E. Bryant.
Graph-based algorithms for boolean function manipulation.
IEEE Transactions in Computers, 8(35):677-691, 1986. BibTeX entry |
| [25] |
M. Buro and H. Kleine Büning.
Report on a SAT competition.
Bulletin of the European Association for Theoretical Computer
Science, 49:143-151, 1993. BibTeX entry, Available here |
| [26] |
Thierry Castell.
Résolution arrière dans la procédure de davis et putnam.
In Actes du Dixième Congrès Reconnaissance des Formes et
Intelligence Artificielle (RFIA'96), pages 109-117, Rennes (France), 1996. BibTeX entry |
| [27] |
Thierry Castell.
Consistance et déduction en logique propositionnelle.
PhD thesis, Thèse de doctorat de l'Université Paul Sabatier,
Toulouse, 1997. BibTeX entry |
| [28] |
Thierry Castell and Michel Cayrol.
Computation of prime implicates and prime implicants by the davis and
putnam procedure.
In Proceedings of the ECAI'96 Workshop on Advances in
Propositional Deduction, pages 5-10, Budapest (Hungary), 1996. BibTeX entry |
| [29] |
Thierry Castell and Hélène Fargier.
Entre SAT et CSP : Problèmes de satisfaction propositionnels et
CSPs clausaux.
In Actes du Onzième Congrès Reconnaissance des Formes et
Intelligence Artificielle (RFIA'98), pages 117-126, Clermont-Ferrand, 1998. BibTeX entry |
| [30] |
Srimat T. Chakradhar and Vishwani D. Agrawal.
A transitive closure based algorithm for test generation.
In Proceedings of the 28th ACM/IEEE Design Automation
Conference, pages 353-358, 1991. BibTeX entry, PDF |
| [31] |
Ming-Te Chao and John V. Franco.
Probabilistic analysis of two heuristics for the 3-satisfiability
problem.
SIAM Journal of Computation, 15(4):1106-1118, 1986. BibTeX entry |
| [32] |
P. Chatalic and L. Simon.
Multi-Resolution on compressed sets of clauses.
In Twelfth International Conference on Tools with Artificial
Intelligence (ICTAI'00), pages 2-10, 2000. BibTeX entry, Compressed PS |
| [33] |
P. Chatalic and L. Simon.
Zres: The old Davis-Putnam procedure meets ZBDDs.
In David McAllester, editor, 17th International Conference on
Automated Deduction (CADE'17), number 1831 in Lecture Notes in Artificial
Intelligence (LNAI), pages 449-454, June 2000. BibTeX entry, Compressed PS |
| [34] |
Philippe Chatalic and Laurent Simon.
Davis et putnam, 40 ans après : une première expérimentation.
In Actes des Cinquièmes Journées Nationales sur la Résolution
Pratique de Problèmes NP-Complets (JNPC'99), pages 9-16, Lyon, 1999. BibTeX entry |
| [35] |
Peter Cheesemann, Bob Kanefsky, and William M. Taylor.
Where the really hard problems are.
In J. Mylopoulos and R. Reiter, editors, Proceedings of the
Twelfth International Joint Conference on Artificial Intelligence
(IJCAI'91), pages 331-337, 1991. BibTeX entry |
| [36] |
Cristian Coarfa, Demitrios D. Demopoulos, Alfonso San Miguel Aguirre, Devika
Subramanian, and Moshe Vardi.
Random 3-SAT: The plot thickens.
In Proceedings of the International Conference on Constraint
Programming, 2000. BibTeX entry, Compressed PS |
| [37] |
Stephen A. Cook.
The complexity of theorem-proving procedures.
In Proceedings of the Third IEEE Symposium on the Foundations of
Computer Science, pages 151-158, 1971. BibTeX entry |
| [38] |
Stephen A. Cook and David G Mitchell.
Finding hard instances of the satisfiability problem: A survey.
In Du, Gu, and Pardalos, editors, Satisfiability Problem: Theory
and Applications, volume 35 of Dimacs Series in Discrete Mathematics
and Theoretical Computer Science, pages 1-17. American Mathematical
Society, 1997. BibTeX entry |
| [39] |
J. M. Crawford and L. D. Auton.
Experimental results on the crossover point in satisfiability
problems.
In Proceedings of the Eleventh National Conference on Artificial
Intelligence (AAAI'93), pages 21-27, 1993. BibTeX entry |
| [40] |
James Crawford, Matthew Ginsberg, Eugene Luks, and Amitabha Roy.
Symmetry-breaking predicates for search problems.
In Proceedings of the Fifth International Conference on
Principles of Knowledge Representation and Reasoning (KR'96), pages
148-159, 1996. BibTeX entry |
| [41] |
Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, Ravi Kannan, Jon Kleinberg,
Christos Papadimitriou, Prabhakar Raghavan, , and Uwe Schöning.
A deterministic (2-2/(k+1))n algorithm for k-SAT based on local
search.
In Proceedings of the twenty-seventh International Colloquium on
Automata, Languages and Programming (ICALP2000), Geneva, Switzerland, 2000.
To appear in Theoretical Computer Science. BibTeX entry, Compressed PS |
| [42] |
Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, and Uwe Schöning.
Deterministic Algorithms for k-SAT Based on Covering Codes and Local
Search.
In Proceeding of ICALP'00, number 1853 in LNSC, pages 236-243.
Springer Verlag, 2000. BibTeX entry |
| [43] |
Martin Davis, George Logemann, and Donald Loveland.
A machine program for theorem proving.
Communications of the ACM, 5(7):394-397, July 1962. BibTeX entry, PDF |
| [44] |
Martin Davis and Hilary Putnam.
A computing procedure for quantification theory.
Journal of the ACM, 7(3):201-215, July 1960. BibTeX entry, PDF |
| [45] |
Rina Dechter and Irina Rish.
Directional resolution: the davis-putnam procedure, revisited.
In 4th International Conference on Knowledge Representation and
Reasoning (KR'94), pages 134-145, 1994. BibTeX entry, PS |
| [46] |
Olivier Dubois, Pascal André, Yacine Boufkhad, and Jacques Carlier.
SAT versus UNSAT.
In Johnson and Trick [92], pages 415-436. BibTeX entry |
| [47] |
Olivier Dubois and Gilles Dequen.
A backbone-search heuristic for efficient solving of hard 3-sat
formulae.
In IJCAI01 [84]. BibTeX entry, Compressed PS |
| [48] |
Uwe Egly, Rainer Feldmann, and Hans Tompits, editors.
Proceedings of QBF2001 workshop at IJCAR'01, Siena, Italy, June
2001. BibTeX entry, Available here |
| [49] |
Michael D. Ernst, Todd D. Millstein, and Daniel S. Weld.
Automatic SAT-compilation of planning problems.
In IJCAI97 [86], pages 1169-1176. BibTeX entry |
| [50] |
S. Even, A. Ital, and A. Shamir.
On the complexity of timetable and multicommodity flow problems.
SIAM Journal on Computing, 5:691-703, 1976. BibTeX entry |
| [51] |
John Franco.
Elimination of infrequent variables improves average case performance
of satisfiability algorithms.
SIAM Journal on Computing, 20:1119-1127, 1991. BibTeX entry |
| [52] |
John Franco and Marvin Paull.
Probabilistic analysis of the davis putnam procedure for solving the
satisfiability problem.
Discrete Applied Mathematics, 5:77-87, 1983. BibTeX entry |
| [53] |
Jon W. Freeman.
Improvements to Propositional Satisfiability Search Algorithms.
PhD thesis, Departement of computer and Information science,
University of Pennsylvania, Philadelphia, 1995. BibTeX entry, Compressed PS |
| [54] |
Richard Génisson and Pierre Siégel.
A polynomial method for sub-clauses production.
In Proceedings of the Sixth International Conference on
Artificial Intelligence: Methodology, Systems, Applications (AIMSA'94),
pages 25-34, 1994. BibTeX entry |
| [55] |
Ian Gent, Hans van Maaren, and Toby Walsh, editors.
SAT20000: Highlights of Satisfiability Research in the
year 2000.
Frontiers in Artificial Intelligence and Applications. Kluwer
Academic, 2000. BibTeX entry |
| [56] |
Ian P. Gent, Holger H. Hoos, Patrick Prosser, and Toby Walsh.
Morphing: Combining structure and randomness.
In Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99), pages 654-660, Orlando, Florida, 1999. BibTeX entry |
| [57] |
Ian P. Gent and Toby Walsh.
The SAT phase transition.
In Proceedings of the Eleventh European Conference on Artificial
Intelligence (ECAI'94), pages 105-109, 1994. BibTeX entry, PS |
| [58] |
E. Giunchiglia, M. Maratea, A. Tacchella, and D. Zambonin.
Evaluating search heuristics and optimization techniques in
propositional satisfiability.
In Proceedings of International Joint Conference on Automated
Reasoning (IJCAR'01), Siena, June 2001.
to appear. BibTeX entry, Compressed PS |
| [59] |
F. Glover and M. Laguna.
Tabu search.
In Modern Heuristic Techniques for Combinatorial Problems,
pages 70-141. Blackwell Scientific Publishing, Oxford, 1993. BibTeX entry |
| [60] |
E. Goldberg and Y. Novikov.
BerkMin: A fast and robust SAT-solver.
In Design, Automation, and Test in Europe (DATE '02), pages
142-149, March 2002. BibTeX entry, PDF |
| [61] |
Carla P. Gomes, Bart Selman, Nuno Crato, and Henry Kautz.
Heavy-Taily Phenomena in Satisfiability.
In Gent et al. [55], pages 15-41. BibTeX entry |
| [62] |
Carla P. Gomes, Bart Selman, and Henry Kautz.
Boosting combinatorial search through randomization.
In Proceedings of the Fifteenth National Conference on
Artificial Intelligence (AAAI'98), pages 431-437, Madison, Wisconsin, 1998. BibTeX entry, PS |
| [63] |
D. Grigoriev.
Tseitin's tautologies and lower bounds for Nullstellensatz
proofs.
In Proceedings of the 39th Annual Symposium on Foundations of
Computer Science. (FOCS-98) [1]. BibTeX entry |
| [64] |
J. F. Groote and J. P. Warners.
The propositional formula checker heerhugo.
Technical Report SEN-R9905, Centrum voor Wiskunde en Informatica
(CWI), Amsterdam, 1999. BibTeX entry, Compressed PS |
| [65] |
J. F. Groote and J. P. Warners.
The propositional formula checker HeerHugo.
In Gent et al. [55], pages 261-281. BibTeX entry |
| [66] |
Jan Friso Zantema Groote and Hans Hans.
Resolution and binary decision diagrams cannot simulate each other
polynomially.
Technical Report CS-2000-14, Utrecht University, 2000. BibTeX entry, Compressed PS |
| [67] |
Jun Gu.
How to solve very large-scale satisfiability problem.
Technical report, Technical Report UUCS-TR-88-032, 1988. BibTeX entry |
| [68] |
Jun Gu.
Efficient local search for very large-scale satisfiability problems.
SIGART Bulletin, 3(1):8-12, 1992. BibTeX entry |
| [69] |
Jun Gu.
Parallel algorithms for satisfiability (SAT) problem.
In P. Pardalos, M. Resende, and K. Ramakrishnan, editors,
Parallel Processing of Discrete Optimization Problems, volume 22 of
DIMACS - Discrete Mathematics and Theoretical Computer Science, pages
105-161. American Mathematical Society, 1995. BibTeX entry |
| [70] |
Jun Gu, Paul W. Purdom, John Franco, and Benjamin W. Wah.
Algorithms for the satisfiability (SAT) Problem: A survey.
In Ding-Zhu Du, Jun Gu, and Panos Pardalos, editors,
Satisfiability Problem: Theory and applications, DIMACS Series in Discrete
Mathematics and Theoretical Computer Science, pages 19-152. American
Mathematical Society, 1997. BibTeX entry |
| [71] |
Venkatesan Guruswami, Daniel Lewin, Madhu Sudan, and Luca Trevisan.
A tight characterization of NP with 3 query PCPs.
In Proceedings of the 39th Annual Symposium on Foundations of
Computer Science. (FOCS-98) [1]. BibTeX entry |
| [72] |
Youssef Hamadi and David Merceron.
Reconfigurable architectures: A new vision for optimization problems.
In Gert Smolka, editor, Proceedings of the Third International
Conference on Principles and Practice of Constraint Programming (CP'97),
Lecture Notes in Computer Science N°1330, pages 209-221, Linz (Austria),
1997. BibTeX entry |
| [73] |
Youssef Hamadi and David Merceron.
Architectures reconfigurables et traitement de problèmes
NP-difficiles : un nouveau domaine d'application.
Technique et Science Informatiques (A paraitre), 1999. BibTeX entry |
| [74] |
John Harrison.
Stålmarck's algorithm as a HOL derived rule.
In Joakim von Wright, Jim Grundy, and John Harrison, editors,
Theorem Proving in Higher Order Logics: 9th International Conference,
TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, Turku,
Finland, 1996. Springer Verlag. BibTeX entry, Available here |
| [75] |
Johan Håstad.
Some optimal inapproximability results.
In Proceedings of the twenty-ninth annual ACM Symposium on
Theory of Computing, El Paso, TX, USA, pages 1-10. ACM Press, 1997. BibTeX entry |
| [76] |
Edward A. Hirsch.
New worst-case upper bounds for SAT.
Journal of Automated Reasonning, 24(4):397-420, 2000. BibTeX entry, Compressed PS |
| [77] |
Edward A. Hirsch.
SAT local search algorithms: Worst-case study.
Journal of Automated Reasonning, 24(1/2):127-143, February
2000. BibTeX entry, Compressed PS |
| [78] |
Edward A. Hirsch.
SAT local search algorithms: Worst-case study.
Journal of Automated Reasoning, 24(1/2):127-143, 2000.
Also reprinted in ``Highlights of Satisfiability Research in the Year
2000'', Volume 63 in Frontiers in Artificial Intelligence and Applications,
IOS Press. BibTeX entry |
| [79] |
J. N. Hooker and V. Vinay.
Branching rules for satisfiability.
Journal of Automated Reasoning, 15:359-383, 1995. BibTeX entry |
| [80] |
Holger H. Hoos.
On the run-time behaviour of stochastic local search algorithms for
sat.
In Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99), pages 661-666, Orlando, Florida, 1999. BibTeX entry, PS |
| [81] |
Holger H. Hoos.
Sat-encodings, search space structure, and local search performance.
In IJCAI99 [87], pages 296-302. BibTeX entry, Compressed PS |
| [82] |
Holger H. Hoos and Thomas Stützle.
Local search algorithms for SAT: An empirical evaluation.
Journal of Automated Reasoning, 24(4):421-481, 2000. BibTeX entry |
| [83] |
Holger H. Hoos and Thomas Stützle.
SATLIB: An Online Resource for Research on SAT.
In Gent et al. [55], pages 283-292. BibTeX entry, Compressed PS |
| [84] |
Proceedings of the Seventeenth International Joint Conference on
Artificial Intelligence (IJCAI'01), Seattle, Washington, USA, August
4th-10th 2001. BibTeX entry, Available here |
| [85] |
Proceedings of the Fourteenth International Joint Conference on Artificial
Intelligence (IJCAI'95), Montréal, Québec, Canada, August 20-25 1995. BibTeX entry, Available here |
| [86] |
Proceedings of the Fifteenth International Joint Conference on Artificial
Intelligence (IJCAI'97), Nagoya, Japan, August 23-29 1997. BibTeX entry, Available here |
| [87] |
Proceedings of the Sixteenth International Joint Conference on Artificial
Intelligence (IJCAI'99), Stockholm, Sweden, July 31-August 6 1999. Morgan
Kaufmann. BibTeX entry, Available here |
| [88] |
Proceedings of the International Joint Conference on Automated Reasoning
(IJCAR'01), Siena, Italy, June 2001. BibTeX entry, Available here |
| [89] |
Russel Impagliazzo, Ramamohan Paturi, and Francis Zane.
Which problems have strongly exponential complexity?
In Proceedings of the 39th Annual Symposium on Foundations of
Computer Science. (FOCS-98) [1], pages 653-662. BibTeX entry, PS |
| [90] |
S Jeannicot, Laurent Oxuzoff, and Antoine Rauzy.
Evaluation sémantique en calcul propositionnel : une propriété de
coupure pour rendre plus efficace la procédure de davis et putnam.
La Revue d'Intelligence Artificielle, 1(2):41-60, 1988. BibTeX entry |
| [91] |
R. J. Jeroslow and J. Wang.
Solving propositional satisfiability problems.
Annals of Mathematics and Artificial Intelligence, 1:167-188,
1990. BibTeX entry |
| [92] |
D. S. Johnson and M. A. Trick, editors.
Second DIMACS implementation challenge : cliques, coloring and
satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and
Theoretical Computer Science.
American Mathematical Society, 1996. BibTeX entry, Available here |
| [93] |
David S. Johnson.
Approximation algorithms for combinatorial problems.
Journal of Computer and System Sciences, 9:256-278, 1974. BibTeX entry |
| [94] |
Bernard Jurkowiak, Chu-Min Li, and Gil Utard.
Parallelizing SATZ Using Dynamic Workload Balancing.
In Kautz and Selman [97].
LICS 2001 Workshop on Theory and Applications of Satisfiability
Testing (SAT 2001). BibTeX entry |
| [95] |
Amit P. Kamath, Narendra K. Karmarkar, K. G. Ramakrishnan, and Mauricio G. C.
Resende.
Computational experience with an interior point algorithm on the
satisfiability problem.
Annals of Operations Research, 25:43-58, 1990. BibTeX entry |
| [96] |
Howard Karloff and Uri Zwick.
A 7/8-approximation algorithm for MAX 3SAT?
In Proceedings of the 38th Annual IEEE Symposium on Foundations
of Computer Science, Miami Beach, FL, USA. IEEE, IEEE Press, 1997. BibTeX entry |
| [97] |
Henry Kautz and Bart Selman, editors.
Proceedings of the Workshop on Theory and Applications of
Satisfiability Testing (SAT2001), volume 9. Elsevier Science Publishers,
June 2001.
LICS 2001 Workshop on Theory and Applications of Satisfiability
Testing (SAT 2001). BibTeX entry, Available here |
| [98] |
Henry A. Kautz, David McAllester, and Bart Selman.
Encoding plans in propositional logic.
In Proceedings of the Fifth International Conference on the
Principle of Knowledge Representation and Reasoning (KR'96), pages 374-384,
1996. BibTeX entry, PS |
| [99] |
Henry A. Kautz and Bart Selman.
Planning as satisfiability.
In Proceedings of the Tenth European Conference on Artificial
Intelligence (ECAI'92), pages 359-363, 1992. BibTeX entry, PS |
| [100] |
Henry A. Kautz and Bart Selman.
Pushing the envelope : Planning, propositional logic, and stochastic
search.
In Proceedings of the Twelfth National Conference on Artificial
Intelligence (AAAI'96), pages 1194-1201, 1996. BibTeX entry, PS |
| [101] |
Henry A. Kautz and Bart Selman.
Unifying SAT-based and graph-based planning.
In IJCAI99 [87], pages 318-325. BibTeX entry, PS |
| [102] |
Sun Kim and Hantao Zhang.
Modgen: Theorem proving by model generation.
In Proceedings of the Twelfth National Conference on Artificial
Intelligence (AAAI'94), pages 162-167, Seattle, 1994. BibTeX entry |
| [103] |
Scott Kirkpatrick, Géza Györgyi, Naftali Tishby, and Lidror Troyansky.
The statistical mechanics of k-satisfaction.
In Advances in Neural Information Processing Systems, volume 6,
pages 439-446. Morgan Kaufmann, 1994. BibTeX entry |
| [104] |
Elias Koutsoupias and Christos H. Papadimitriou.
On the greedy algorithm for satisfiability.
Information Processing Letters, 43(1):53-55, 1992. BibTeX entry |
| [105] |
R. A. Kowalsky and D. Kuehner.
Linear resolution with selection function.
Artificial Intelligence, 2:227-260, 1971. BibTeX entry |
| [106] |
O. Kullmann.
Heuristics for SAT algorithms: Searching for some foundations,
September 1998.
23 pages, updated September 1999 w.r.t. running times, url =
http://cs-svr1.swan.ac.uk/ csoliver/heur2letter.ps.gz. BibTeX entry |
| [107] |
Tracy Larrabee.
Test Pattern Generation Using Boolean Satisfiability.
IEEE Transactions on Computer-Aided Design, 11(1):6-22,
January 1992. BibTeX entry, PS |
| [108] |
Daniel Le Berre.
Exploiting the real power of unit propagation lookahead.
In Kautz and Selman [97].
LICS 2001 Workshop on Theory and Applications of Satisfiability
Testing (SAT 2001). BibTeX entry |
| [109] |
Chu-Min Li.
A constrained based approach to narrow search trees for
satisfiability.
Information processing letters, 71:75-80, 1999. BibTeX entry, PS |
| [110] |
Chu-Min Li.
Equivalency reasoning to solve a class of hard sat problems.
available at http://www.research.att.com/ selman/challenge, 1999. BibTeX entry, PS |
| [111] |
Chu-Min Li.
Integrating Equivalency reasoning into Davis-Putnam procedure.
In AAAI00 [2], pages 291-296. BibTeX entry, PS |
| [112] |
Chu-Min Li and Anbulagan.
Heuristics based on unit propagation for satisfiability problems.
In IJCAI97 [86], pages 366-371. BibTeX entry, PS |
| [113] |
Chu-Min Li and Sylvain Gérard.
On the limit of branching rules for hard random unsatisfiable
3-SAT.
In Proceedings of the 14th European Conference on Artificial
Intelligence (ECAI-2000), pages 98-102, Berlin, 2000. BibTeX entry, PS |
| [114] |
Dongmin Liang and Wei Li.
Multi-strategy local search for SAT problem.
In Proceedings of the Thirteenth European Conference on
Artificial Intelligence (ECAI'98), pages 234-238, 1998. BibTeX entry |
| [115] |
Michael L. Littman.
Initial experiments in stochastic satisfiability.
In Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99), pages 667-672, Orlando, Florida, 1999. BibTeX entry |
| [116] |
Inês Lynce.
Algebraic Simplification Techniques for Propositional
Satisfiability.
Master's thesis, Instituto Superior Técnico, Lisboa, Portugal,
March 2001. BibTeX entry, Compressed PS |
| [117] |
Inês Lynce, Luis Baptista, and Jo ao P. Marques Silva.
Stochastic systematic search algorithms for satisfiability.
In Kautz and Selman [97].
LICS 2001 Workshop on Theory and Applications of Satisfiability
Testing (SAT 2001). BibTeX entry, Compressed PS |
| [118] |
Joao P. Marques-Silva.
Algebraic Simplification Techniques for Propositional
Satisfiability.
In Proceedings of the 6th International Conference on Principles
and Practice of Constraint Programming (CP'2000), September 2000. BibTeX entry, Compressed PS |
| [119] |
Joao P. Marques-Silva and Thomas Glass.
Combinational Equivalence Checking Using Satisfiability and
Recursive Learning.
In Proceedings of the IEEE/ACM Design, Automation and Test in
Europe Conference (DATE), 1999. BibTeX entry, Compressed PS |
| [120] |
Joao P. Marques-Silva and Karem A. Sakallah.
GRASP - A New Search Algorithm for Satisfiability.
In Proceedings of IEEE/ACM International Conference on
Computer-Aided Design, pages 220-227, November 1996. BibTeX entry, Compressed PS |
| [121] |
Joao P. Marques-Silva and Karem A. Sakallah.
Boolean Satisfiability in Electronic Design Automation.
In Proceedings of the IEEE/ACM Design Automation Conference
(DAC), June 2000. BibTeX entry, Compressed PS |
| [122] |
Fabio Massacci.
Using walk-sat and rel-sat for cryptographic key search.
In IJCAI99 [87], pages 290-295. BibTeX entry |
| [123] |
B. Mazure, L. Saïs, and E. Grégoire.
Tabu search for sat.
In Proceedings of the Fourteenth National Conference on
Artificial Intelligence (AAAI'97), pages 281-285, Providence (Rhode Island
USA), 1997. BibTeX entry |
| [124] |
Bertrand Mazure.
De la Satisfiabilité à la Compilation de Bases de Connaissances
Propositionnelles.
PhD thesis, Thèse de doctorat de l'Université d'Artois, Lens, 1999. BibTeX entry |
| [125] |
Bertrand Mazure, Lakhdar Saïs, and Eric Grégoire.
Boosting complete techniques thanks to local search methods.
Annals of Mathematics and Artificial Intelligence, 22:319-331,
1998. BibTeX entry |
| [126] |
David McAllester, Bart Selman, and Henry Kautz.
Evidence for invariants in local search.
In Proceedings of the Fourteenth National Conference on
Artificial Intelligence (AAAI'97), pages 321-326, Providence, Rhode Island,
1997. BibTeX entry |
| [127] |
William McCune.
A davis-putnam program and its application to finite first-order
model search: Quasigroup existence problem.
Technical report, Technical Memorandum ANL/MCS-TM-194, 1994. BibTeX entry |
| [128] |
David Mitchell, Bart Selman, and Hector Levesque.
Hard and easy distribution of SAT problems.
In Proceedings of the Tenth National Conference on Artificial
Intelligence (AAAI'92), pages 440-446, 1992. BibTeX entry |
| [129] |
David Mitchell, Bart Selman, and Hector Levesque.
Problem solving: Hardness and easiness - hard and easy distributions
of SAT problems.
In Proceeding of the 10th National Conference on Artificial
Intelligence (AAAI-92), San Jose, California, pages 459-465. AAAI Press,
Menlo Park, California, USA, 1992. BibTeX entry |
| [130] |
Michael Molloy and Bruce Reed.
Further algorithmic aspects of the Local Lemma.
In Proceedings of the 39th Annual Symposium on Foundations of
Computer Science. (FOCS-98) [1]. BibTeX entry |
| [131] |
B Monien and E. Speckenmeyer.
Solving satisfiability in less than 2n steps.
Discrete Applied Mathematics, 10:287-295, 1985. BibTeX entry |
| [132] |
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad
Malik.
Chaff: Engineering an Efficient SAT Solver.
In Proceedings of the 38th Design Automation Conference
(DAC'01), June 2001. BibTeX entry, PDF |
| [133] |
Laurent Oxusoff and Antoine Rauzy.
L'évaluation sémantique en calcul propositionnel.
PhD thesis, Thèse de doctorat de l'Université de Provence,
GIA-Luminy, Marseille, 1989. BibTeX entry |
| [134] |
Andrew J. Parkes and Joachim P. Walser.
Tuning local search for satisfiability testing.
In Proceedings of the Thirteenth National Conference on
Artificial Intelligence (AAAI'96), pages 356-362, 1996. BibTeX entry |
| [135] |
Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane.
An improved exponential-time algorithm for k-SAT.
In Proceedings of the 39th Annual Symposium on Foundations of
Computer Science. (FOCS-98) [1], pages 628-637. BibTeX entry, PS |
| [136] |
D. Prawitz.
Natural Deduction: A Proof Theoretical Study.
Almquist & Wiksell, 1965. BibTeX entry |
| [137] |
Nicolas Prcovic and Bertrand Neveu.
Etude théorique sur les recherches entrelacées et à divergence
limitée.
In Actes de Cinquièmes Journées Nationales sur la Résolution
Pratique de Problèmes NP-Complets (JNPC'99), pages 85-94, Lyon, 1999. BibTeX entry |
| [138] |
Soraya Rana, Robert B. Heckendorn, and Darrell Whitley.
A tractable walsh analysis of SAT and its implications for genetic
algorithms.
In Proceedings of the Fifteenth National Conference on
Artificial Intelligence (AAAI'98), pages 392-397, 1998. BibTeX entry |
| [139] |
Antoine Rauzy, Lackdar Saïs, and L. Brisoux.
Calcul propositionnel : vers une extension du formalisme.
In Actes des Cinquièmes Journées Nationales sur la Résolution
Pratique de Problèmes NP-complets (JNPC'99), pages 189-198, Lyon, 1999. BibTeX entry |
| [140] |
Irina Rish.
Efficient Reasoning in Graphical Models.
PhD thesis, University of California, Irvine, 1999. BibTeX entry, PDF |
| [141] |
Irina Rish and Rina Dechter.
To guess or to think? hybrid algorithms for SAT.
In proceedings of the International Conference on Principles and
Pratice of Constraint Programming (CP'96), 1996. BibTeX entry, PS |
| [142] |
Irina Rish and Rina Dechter.
Resolution versus search: Two strategies for SAT.
Journal of Automated Reasoning, 24(1/2):225-275, 2000. BibTeX entry, PDF |
| [143] |
J. A. Robinson.
A machine-oriented logic based on the resolution principle.
Journal of the ACM, 12(1):23-41, January 1965. BibTeX entry, PDF |
| [144] |
Uwe Schöning.
A probabilistic algorithm for k-SAT and constraint satisfaction
problems.
In Proceedings of the 40th Annual IEEE Symposium on Foundations
of Computer Science, New York, NY, USA, pages 410-414. IEEE Press, 1999. BibTeX entry |
| [145] |
Robert C. Schrag.
Compilation of critically constrained knowledge bases.
In Proceedings of the Thirteenth National Conference on
Artificial Intelligence (AAAI'96), pages 510-515, 1996. BibTeX entry |
| [146] |
M. H. Schulz, E. Trischler, and T. M. Sarfert.
SOCRATES : A highly efficient automatic test pattern generation
system.
IEEE Transactions on Computer-Aided Design, 7(1):126-137,
1988. BibTeX entry |
| [147] |
Bart Selman and Henry A. Kautz.
Domain-independant extensions to GSAT : Solving large structured
variables.
In Proceedings of the Thirteenth International Joint Conference
on Artificial Intelligence (IJCAI'93), pages 290-295, 1993. BibTeX entry, PS |
| [148] |
Bart Selman, Henry A. Kautz, and Bram Cohen.
Noise strategies for improving local search.
In Proceedings of the Twelfth National Conference on Artificial
Intelligence (AAAI'94), pages 337-343, Seattle, 1994. BibTeX entry, PS |
| [149] |
Bart Selman, Henry A. Kautz, and Bram Cohen.
Local search strategies for satisfiability testing.
In Johnson and Trick [92], pages 521-532. BibTeX entry, PS |
| [150] |
Bart Selman, Henry A. Kautz, and David A. McAllester.
Ten challenges in propositional reasoning and search.
In Proceedings of the Fifteenth International Joint Conference
on Artificial Intelligence (IJCAI'97), pages 50-54, 1997. BibTeX entry, PS |
| [151] |
Bart Selman, Hector Levesque, and D. Mitchell.
A new method for solving hard satisfiability problems.
In Proceedings of the Tenth National Conference on Artificial
Intelligence (AAAI'92), pages 459-465, 1992. BibTeX entry |
| [152] |
Mary Sheeran and Gunnar Stålmark.
A tutorial on stålmark's proof procedure for propositional logic.
In Volume 152 of Lecture Notes in Computer Science, pages
82-99. Springer Verlag, 1998. BibTeX entry |
| [153] |
Pierre Siegel.
Représentation et utilisation de la connaissance en calcul
propositionnel.
PhD thesis, Thèse d'état, Université de Provence, GIA-Luminy,
Marseille, Marseille, 1987. BibTeX entry |
| [154] |
Laurent Simon.
SAT-Ex.
http://www.lri.fr/ simon/satex/satex.php3, 2000. BibTeX entry, Available here |
| [155] |
Laurent Simon and Philippe Chatalic.
SATEx: a web-based framework for SAT experimentation.
In Kautz and Selman [97].
http://www.lri.fr/ simon/satex/satex.php3. BibTeX entry, Compressed PS, PDF |
| [156] |
Josh Singer, Ian Gent, and Alan Smaill.
Backbone Fragility and the Local Search Cost Peak.
Journal of Artificial Intelligence Research, 12:235-270, 2000. BibTeX entry, PDF |
| [157] |
Ewald Speckenmeyer, Max Böhm, and Peter Heusch.
On the imbalance of distributions of solutions of CNF-formulas and
its impact on satisfiability solvers.
In Dingyhu Du, Jun Gu, and Panos M. Pardalos, editors,
Satisfiability Problem: Theory and Applications, volume 35 of DIMACS
Series in Discrete Mathematics and Theoretical Computer Science, pages
669-676. American Mathematical Society, 1997. BibTeX entry |
| [158] |
G. Stålmarck.
A system for determining propositional logic theorems by applying
values and rules to triplets that are generated from a formula.
Technical report, European Patent N° 0403 454 (1995), US Patent N° 5
276 897, Swedish Patent N° 467 076 (1989), 1989. BibTeX entry |
| [159] |
P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli.
Combinational Test Generation Using Satisfiability.
IEEE Transactions on Computer-Aided Design, 15(9):1167-1176,
September 1996. BibTeX entry |
| [160] |
P. Tafertshofer and A. Ganz.
SAT Based ATPG Using Fast Justification and Propagation in the
Implication Graph.
In Proceedings of the International Conference on Computer-Aided
Design, 1999. BibTeX entry, Compressed PS |
| [161] |
P. Tafertshofer, A. Ganz, and M. Henftling.
A SAT-Based Implication Engine for Efficient ATPG, Equivalence
Checking, and Optimization of Netlists.
In Proceedings of the International Conference on Computer-Aided
Design, pages 648-657, November 1997. BibTeX entry, Compressed PS |
| [162] |
G. S. Tseitin.
On the complexity of derivation in the propositional calculus.
Zapiski nauchnykh seminarov LOMI, 8:234-259, 1968.
English translation of this volume: Consultants Bureau, N.Y., 1970,
pp. 115-125. BibTeX entry |
| [163] |
Alasdair Urquhart.
Hard examples for resolution.
Journal of the Association for Computing Machinery,
34(1):209-219, 1987. BibTeX entry |
| [164] |
Allen Van Gelder and Yumi K. Tsuji.
Satisfiability Testing with More Reasoning and Less Guessing.
In Johnson and Trick [92]. BibTeX entry, Compressed PS |
| [165] |
M.N. Velev and R.E. Bryant.
Effective use of boolean satisfiability procedures in the formal
verification of superscalar and vliw microprocessors.
In Proceedings of the 38th Design Automation Conference (DAC
'01), pages 226-231, June 2001. BibTeX entry, Compressed PS |
| [166] |
Jinchang Wang.
Branching rules for propositionnal satisfiability test.
In Ding-Zhu Du and Panos Gu, Jun an Pardalos, editors,
Satisfiability Problem: Theory and applications, volume DIMACS Series in
Discrete Mathematics and Theoretical Computer Science, pages 351-364.
American Mathematical Society, 1997. BibTeX entry |
| [167] |
J. P. Warners and H. Van-Maaren.
A two phase algorithm for solving a class of hard satisfiability
problems.
Operations Research letters, 23:81-88, 1998. BibTeX entry, Compressed PS |
| [168] |
Poul F. Williams, Armin Biere, Edmund M. Clarke, and Anubhav Gupta.
Combining Decision Diagrams and SAT Procedures for Efficient
Symbolic Model Checking.
In Proceedings of CAV'00, 2000. BibTeX entry |
| [169] |
Steven A. Wolfman and Daniel S. Weld.
The lpsat engine and its application to resource planning.
In IJCAI99 [87], pages 310-316. BibTeX entry |
| [170] |
Zhe Wu and Benjamin W. Wah.
Trap escaping strategies in discrete lagrangian methods for solving
hard satisfiability and maximum satisfiability problems.
In Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99), pages 673-678, Orlando, Florida, 1999. BibTeX entry |
| [171] |
Makoto Yokoo, Takayuki Suyama, and Hiroshi Sawada.
Solving satisfiability problems using field programmable gate arrays:
First results.
In Proceedings of the Second International Conference on
Principles ans Practice of Constraint Programming (CP'96), pages 495-509,
Cambridge, MA, USA, 1996. BibTeX entry |
| [172] |
Francis Zane.
Circuits, CNFs, and Satisfiability.
PhD thesis, Dept. of Computer Science and Engineering, UCSD, 1998. BibTeX entry, PS |
| [173] |
H. Zhang and M. E. Stickel.
An efficient algorithm for unit propagation.
In Proceedings of the Fourth International Symposium on
Artificial Intelligence and Mathematics (AI-MATH'96), Fort Lauderdale
(Florida USA), 1996. BibTeX entry |
| [174] |
Hantao Zhang.
SATO: an efficient propositional prover.
In Proceedings of the International Conference on Automated
Deduction (CADE'97), volume 1249 of LNAI, pages 272-275, 1997. BibTeX entry |
| [175] |
Hantao Zhang and Mark Stickel.
Implementing the davis-putnam algorithm by tries.
Technical report, Dept. of Computer Science, University of Iowa,
1994. BibTeX entry |
| [176] |
Jian Zhang and Hantao Zhang.
Sem: a system for enumerating models.
In IJCAI95 [85], pages 298-303. BibTeX entry |
| [177] |
L. Zhang, C. F. Madigan, M. W. Moskewicz, and S. Malik.
Efficient conflict driven learning in a Boolean satisfiability
solver.
In International Conference on Computer-Aided Design
(ICCAD'01), pages 279-285, November 2001. BibTeX entry, PDF |
| [178] |
Uri Zwick.
Approximation algorithms for constraint satisfaction problems
involving at most three variables per constraint.
In Proceedings of the ninth Annual ACM-SIAM Symposium on
Discrete Algorithms, Baltimore, MD, USA, pages 201-210. ACM Press, 1998. BibTeX entry |