@COMMENT{{This file has been generated by bib2bib 1.46}}
@COMMENT{{Command line: bib2bib satbib.bib confs.bib -ob whole.bib}}
@COMMENT{{version1.47lastmodified2002/07/0217:09:10}}
@INPROCEEDINGS{Abdulla2000a,
AUTHOR = {Parosh Aziz Abdulla and Per Bjesse and Niklas E\'en},
TITLE = {{Symbolic Reachability Analysis Based on {SAT}-Solvers}},
BOOKTITLE = {Proceedings of the 6th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems
(TACAS'2000)},
YEAR = 2000,
URL = {http://www.docs.uu.se/~parosh/publications/smc.ps}
}
@ARTICLE{Aspvall1979a,
AUTHOR = {B. Aspvall and M. Plass and R. Tarjan},
TITLE = {A linear-time algorithm for testing the truth of certain quantified boolean formulas},
JOURNAL = {Information Processing Letters},
YEAR = 1979,
VOLUME = 8,
PAGES = {121--123}
}
@INPROCEEDINGS{Asahiro1996a,
AUTHOR = {Yuichi Asahiro and Kazuo Iwama and Eiji Miyano},
TITLE = {Random Generation of Test Instances with Controlled Attributes},
CROSSREF = {Johnson1996a},
PAGES = {377--393}
}
@INPROCEEDINGS{Audemard1999a,
AUTHOR = {Gilles Audemard and Belaid Benhamou and Pierre Siegel},
TITLE = {La méthode d'avalanche {AVAL} : une méthode énumérative
pour {SAT}},
BOOKTITLE = {Actes des Cinquièmes Journées Nationales sur la
Résolution Pratique de Problèmes NP-Complets (JNPC'99)},
PAGES = {17--25},
ADDRESS = {Lyon},
YEAR = 1999
}
@INPROCEEDINGS{Audemard2000a,
AUTHOR = {Gilles Audemard and Belaid Benhamou and Pierre Siegel},
TITLE = {{AVAL}: An enumerative method for {SAT}},
BOOKTITLE = {Proceedings of the First international conference on
Computational Logic (CL'00)},
PAGES = {373-383},
ADDRESS = {Londres},
MONTH = {July},
YEAR = 2000
}
@INPROCEEDINGS{Bacchus2002a,
AUTHOR = {Fahiem Bacchus},
TITLE = {Enhancing Davis Putnam with Extended Binary Clause Reasoning},
BOOKTITLE = {Proceedings of National Conference on Artificial Intelligence (AAAI-2002)},
YEAR = 2002,
NOTE = {to appear},
URL = {http://www.cs.toronto.edu/~fbacchus/Papers/BAAAI02.pdf}
}
@INPROCEEDINGS{Bacchus2002b,
AUTHOR = {Fahiem Bacchus},
TITLE = {Exploring the Computational Tradeoff of more Reasoning and Less Searching},
BOOKTITLE = {Proceedings of Fifth International Symposium on Theory and Applications of Satisfiability Testing},
PAGES = {7--16},
YEAR = 2002,
URL = {http://www.cs.toronto.edu/~fbacchus/Papers/Bsat2002.pdf}
}
@INPROCEEDINGS{Bailleux1999a,
AUTHOR = {Olivier Bailleux and Pierre Marquis},
TITLE = {{DISTANCE-SAT}: Complexity and Algorithms},
BOOKTITLE = {Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99)},
PAGES = {642-647},
ADDRESS = {Orlando, Florida},
YEAR = 1999
}
@INPROCEEDINGS{Bailleux1999b,
AUTHOR = {Olivier Bailleux and Pierre Marquis},
TITLE = {{DISTANCE-SAT} : complexité et algorithmes},
BOOKTITLE = {Actes des Cinquièmes Journées Nationales sur la
Résolution Pratique de Problèmes NP-Complets (JNPC'99)},
PAGES = {199-206},
ADDRESS = {Lyon},
YEAR = 1999
}
@INPROCEEDINGS{Baptista2000a,
AUTHOR = { Luís Baptista and João P. Marques-Silva},
TITLE = {Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability},
BOOKTITLE = {in Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP)},
YEAR = 2000,
MONTH = {September},
URL = {http://sat.inesc.pt/~jpms/research/papers/cp2000/cp2000-rand.ps.gz}
}
@INPROCEEDINGS{Bayardo1997a,
AUTHOR = {Roberto J. Jr. Bayardo and Robert C. Schrag},
TITLE = {Using {CSP} Look-Back Techniques to Solve Real-World {SAT}
Instances},
BOOKTITLE = {Proceedings of the Fourteenth National Conference on
Artificial Intelligence (AAAI'97) },
PAGES = {203-208},
ADDRESS = {Providence, Rhode Island},
YEAR = 1997,
URL = {http://www.almaden.ibm.com/cs/people/bayardo/ps/aaai97.ps.Z}
}
@ARTICLE{Benhamou1994a,
AUTHOR = {Belaïd Benhamou and Lakhdar Saïs},
TITLE = {Tractability Through Symmetries in Propositional
Calculus},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {12},
PAGES = {89-102},
PUBLISHER = {Springer Verlag},
YEAR = 1994
}
@INPROCEEDINGS{Benhamou1994b,
AUTHOR = {Belaid Benhamou and Lakhdar Sais and Pierre Siegel},
TITLE = {Two proof procedures for a cardinality based language
in propositional calculus},
BOOKTITLE = {Proceedings of the Eleventh Annual Symposium on
Theoretical Aspects of Computer Science (STACS), volume
775 de Lecture Notes in Computer Science},
PAGES = {71-82},
ADDRESS = {Caen (France)},
PUBLISHER = {Springer Verlag},
YEAR = 1994
}
@INPROCEEDINGS{Biere1999a,
AUTHOR = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Y. Zhu},
TITLE = {{Symbolic Model Checking without BDDs}},
BOOKTITLE = {Proceedings of Tools and Algorithms for the Analysis
and Construction of Systems (TACAS'99), number 1579 in
LNCS},
YEAR = 1999,
URL = {http://www.inf.ethz.ch/personal/biere/papers/BiereCimattiClarkeZhu-TACAS99.ps.gz}
}
@INPROCEEDINGS{Biere1999b,
AUTHOR = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and M. Fujita
and Y. Zhu},
TITLE = {Symbolic Model Checking using {SAT} procedures instead
of BDDs},
BOOKTITLE = {Proceedings of Design Automation Conference (DAC'99)},
YEAR = 1999,
URL = {http://www.inf.ethz.ch/personal/biere/papers/BiereCimattiClarkeFujitaZhu-DAC99.ps.gz}
}
@ARTICLE{Billionnet1992a,
AUTHOR = {A. Billionnet and A. Sutter},
TITLE = {An efficient algorithm for the 3 satisfiability
problem},
JOURNAL = {Operation Research Letters},
VOLUME = {12},
PAGES = {29-36},
YEAR = 1992
}
@PHDTHESIS{Boufkhad1996a,
AUTHOR = {Yacine Boufkhad},
TITLE = {Aspects probabilistes et algorithmiques du problème de
satisfiabilité},
SCHOOL = {Thèse de doctorat de l'Université de Paris 6},
YEAR = 1996
}
@INPROCEEDINGS{Boufkhad1997a,
AUTHOR = {Yacine Boufkhad and Eric Gr\'egoire and Pierre Marquis
and Bertrand Mazure and Lakhdar Saïs},
TITLE = {Tractable Cover Compilations},
CROSSREF = {IJCAI97},
PAGES = {122-127}
}
@INPROCEEDINGS{Brafman2001a,
AUTHOR = {Ronen I. Brafman},
TITLE = {A simplifier for Propositional Formulas with Many Binary clauses},
CROSSREF = {IJCAI01},
URL = {http://www.cs.bgu.ac.il/~brafman/ijcai01-binsat.ps}
}
@TECHREPORT{Brafman2000a,
AUTHOR = {Ronen I. Brafman},
TITLE = {A simplifier for Propositional Formulas with Many
Binary clauses},
NUMBER = {00-04},
INSTITUTION = {Departement of Computer
Science, Ben-Gurion University},
ADDRESS = {Beer-Sheva, Israel},
YEAR = 2000
}
@PHDTHESIS{Brisoux-Devendeville1999a,
AUTHOR = {Laure Brisoux-Devendeville},
TITLE = {Satisfaisabilité propositionnelle en informatique :
aspects algorithmiques et extensions du formalisme},
SCHOOL = {Thèse de doctorat de l'Université d'Artois},
ADDRESS = {Lens},
YEAR = 1999
}
@ARTICLE{Bryant1986a,
AUTHOR = {R. E. Bryant},
TITLE = {Graph-based Algorithms for Boolean Function
Manipulation},
JOURNAL = {IEEE Transactions in Computers},
VOLUME = {8},
NUMBER = {35},
PAGES = {677-691},
YEAR = 1986
}
@ARTICLE{Buro1993a,
AUTHOR = {M. Buro and H. Kleine B{\"u}ning},
TITLE = {Report on a {SAT} Competition},
JOURNAL = {Bulletin of the European Association for Theoretical Computer Science},
VOLUME = 49,
PAGES = {143--151},
YEAR = 1993,
URL = {citeseer.nj.nec.com/buro92report.html}
}
@INPROCEEDINGS{Castell1996a,
AUTHOR = {Thierry Castell and Michel Cayrol},
TITLE = {Computation of Prime Implicates and Prime Implicants
by the Davis and Putnam Procedure},
BOOKTITLE = {Proceedings of the ECAI'96 Workshop on Advances in
Propositional Deduction},
PAGES = {5-10},
ADDRESS = {Budapest (Hungary)},
YEAR = 1996
}
@INPROCEEDINGS{Castell1996b,
AUTHOR = {Thierry Castell},
TITLE = {Résolution arrière dans la procédure de Davis et
Putnam},
BOOKTITLE = {Actes du Dixième Congrès Reconnaissance des Formes et
Intelligence Artificielle (RFIA'96)},
PAGES = {109-117},
ADDRESS = {Rennes (France)},
YEAR = 1996
}
@PHDTHESIS{Castell1997a,
AUTHOR = {Thierry Castell},
TITLE = {Consistance et d\'eduction en logique propositionnelle},
ADDRESS = {Toulouse},
SCHOOL = {Th\`ese de doctorat de l'Universit\'e Paul Sabatier},
YEAR = 1997
}
@INPROCEEDINGS{Castell1998a,
AUTHOR = {Thierry Castell and Hélène Fargier},
TITLE = {Entre {SAT} et {CSP} : Problèmes de Satisfaction
Propositionnels et {CSPs} clausaux},
BOOKTITLE = {Actes du Onzième Congrès Reconnaissance des Formes et
Intelligence Artificielle (RFIA'98)},
PAGES = {117-126},
ADDRESS = {Clermont-Ferrand},
YEAR = 1998
}
@INPROCEEDINGS{Chakradhar1991a,
AUTHOR = {Srimat T. Chakradhar and Vishwani D. Agrawal},
TITLE = {A transitive closure based algorithm for test generation},
BOOKTITLE = {Proceedings of the 28th ACM/IEEE Design Automation Conference},
PAGES = {353--358},
YEAR = 1991,
URL = {http://www.sigda.org/Archives/ProceedingArchives/Dac/Dac91/papers/1991/dac91/22_3/dac91_353.pdf}
}
@INPROCEEDINGS{Chatalic1999a,
AUTHOR = {Philippe Chatalic and Laurent Simon},
TITLE = {Davis et Putnam, 40 ans après : une première
expérimentation},
BOOKTITLE = {Actes des Cinquièmes Journées Nationales sur la
Résolution Pratique de Problèmes NP-Complets (JNPC'99)},
PAGES = {9-16},
ADDRESS = {Lyon},
YEAR = 1999
}
@INPROCEEDINGS{Chatalic2000a,
AUTHOR = {P. Chatalic and L. Simon},
TITLE = {ZRes: The old {Davis}-{Putnam} procedure meets {ZBDDs}},
BOOKTITLE = {17th International Conference on Automated Deduction ({CADE'17})},
PAGES = {449-454},
YEAR = {2000},
EDITOR = {David McAllester},
NUMBER = {1831},
SERIES = {Lecture Notes in Artificial Intelligence ({LNAI})},
MONTH = {June},
URL = {http://www.lri.fr/~simon/recherche/papiers/cade2000.ps.gz}
}
@INPROCEEDINGS{Chatalic2000b,
AUTHOR = {P. Chatalic and L. Simon},
TITLE = {Multi-{Resolution} on Compressed Sets of Clauses},
BOOKTITLE = {Twelfth International Conference on Tools with Artificial Intelligence ({ICTAI'00})},
PAGES = {2-10},
YEAR = {2000},
URL = {http://www.lri.fr/~simon/recherche/papiers/ictai00.ps.gz}
}
@ARTICLE{Chao1986a,
AUTHOR = {Ming-Te Chao and John V. Franco},
TITLE = {Probabilistic Analysis of Two Heuristics for the 3-Satisfiability Problem},
JOURNAL = {SIAM Journal of Computation},
YEAR = 1986,
VOLUME = 15,
NUMBER = 4,
PAGES = {1106--1118}
}
@INPROCEEDINGS{Cheeseman1991a,
AUTHOR = {Peter Cheesemann and Bob Kanefsky and William M. Taylor},
TITLE = {Where the really hard problems are},
BOOKTITLE = {Proceedings of the Twelfth International Joint Conference on
Artificial Intelligence (IJCAI'91)},
PAGES = {331-337},
YEAR = 1991,
EDITOR = {J. Mylopoulos and R. Reiter}
}
@INPROCEEDINGS{Coarfa2000a,
AUTHOR = {Cristian Coarfa and Demitrios D. Demopoulos and Alfonso {San Miguel Aguirre} and Devika Subramanian and Moshe Vardi},
TITLE = {Random {3-SAT}: The Plot Thickens},
BOOKTITLE = {Proceedings of the International Conference on Constraint Programming},
YEAR = 2000,
URL = {http://www.cs.rice.edu/~vardi/papers/cp00rj.ps.gz}
}
@INPROCEEDINGS{Cook1971a,
AUTHOR = {Stephen A. Cook},
TITLE = {The complexity of theorem-proving procedures},
BOOKTITLE = {Proceedings of the Third IEEE Symposium on the
Foundations of Computer Science},
PAGES = {151-158},
YEAR = 1971
}
@INCOLLECTION{Cook1997a,
AUTHOR = {Stephen A. Cook and David G Mitchell},
TITLE = {Finding Hard Instances of the Satisfiability Problem: A Survey},
BOOKTITLE = {Satisfiability Problem: Theory and Applications},
PAGES = {1--17},
PUBLISHER = {American Mathematical Society},
YEAR = 1997,
EDITOR = {Du and Gu and Pardalos},
VOLUME = 35,
SERIES = {Dimacs Series in Discrete Mathematics and Theoretical Computer Science}
}
@INPROCEEDINGS{Crawford1993a,
AUTHOR = {J. M. Crawford and L. D. Auton},
TITLE = {Experimental results on the crossover point in
satisfiability problems},
BOOKTITLE = {Proceedings of the Eleventh National Conference on
Artificial Intelligence (AAAI'93)},
PAGES = {21-27},
YEAR = 1993
}
@INPROCEEDINGS{Crawford1996a,
AUTHOR = {James Crawford and Matthew Ginsberg and Eugene Luks
and Amitabha Roy},
TITLE = {Symmetry-Breaking Predicates for Search Problems},
BOOKTITLE = {Proceedings of the Fifth International Conference on
Principles of Knowledge Representation and Reasoning
(KR'96)},
PAGES = {148-159},
YEAR = 1996
}
@INPROCEEDINGS{Dantsin2000a,
AUTHOR = {Evgeny Dantsin and Andreas Goerdt and Edward A. Hirsch and Ravi Kannan and Jon Kleinberg and Christos Papadimitriou and Prabhakar Raghavan and and Uwe Sch\"oning},
TITLE = {A deterministic $(2-2/(k+1))^n$ algorithm for k-{SAT} based on local search},
BOOKTITLE = {Proceedings of the twenty-seventh International Colloquium on Automata, Languages and Programming (ICALP2000), Geneva, Switzerland},
YEAR = 2000,
NOTE = {To appear in Theoretical Computer Science.},
URL = {http://logic.pdmi.ras.ru/~hirsch/papers/00tcs.ps.gz}
}
@INPROCEEDINGS{Dantsin2000b,
AUTHOR = {Evgeny Dantsin and Andreas Goerdt and Edward A. Hirsch and Uwe Sch\"oning},
TITLE = {{Deterministic Algorithms for k-SAT Based on Covering Codes and Local Search}},
BOOKTITLE = {Proceeding of ICALP'00},
PAGES = {236--243},
YEAR = 2000,
NUMBER = 1853,
SERIES = {LNSC},
PUBLISHER = {Springer Verlag},
ANNOTE = {1.481^N-time deterministic 3-SAT algorithm.},
KEYWORDS = {SAT,DERAND,WCRT,UB}
}
@ARTICLE{Davis1960a,
AUTHOR = {Martin Davis and Hilary Putnam},
TITLE = {A computing procedure for quantification theory},
JOURNAL = {Journal of the ACM},
VOLUME = 7,
NUMBER = 3,
MONTH = {July},
PAGES = {201--215},
YEAR = 1960,
URL = {http://www.acm.org/pubs/articles/journals/jacm/1960-7-3/p201-davis/p201-davis.pdf}
}
@ARTICLE{Davis1962a,
AUTHOR = {Martin Davis and George Logemann and Donald Loveland},
TITLE = {A machine program for theorem proving},
JOURNAL = {Communications of the ACM },
VOLUME = 5,
NUMBER = 7,
MONTH = {July},
PAGES = {394-397},
YEAR = 1962,
URL = {http://www.acm.org/pubs/articles/journals/cacm/1962-5-7/p394-davis/p394-davis.pdf}
}
@INPROCEEDINGS{Dechter1994a,
AUTHOR = {Rina Dechter and Irina Rish},
TITLE = {Directional Resolution: the Davis-Putnam procedure, revisited},
BOOKTITLE = {4th International Conference on Knowledge Representation and Reasoning (KR'94)},
YEAR = {1994},
PAGES = {134-145},
URL = {http://www.ics.uci.edu/~csp/r29-dr_KR94.ps}
}
@INCOLLECTION{Dubois1996a,
AUTHOR = {Olivier Dubois and Pascal Andr\'e and Yacine Boufkhad
and Jacques Carlier},
TITLE = {{SAT} versus {UNSAT}},
PAGES = {415-436},
CROSSREF = {Johnson1996a}
}
@INPROCEEDINGS{Dubois2001a,
AUTHOR = {Olivier Dubois and Gilles Dequen},
TITLE = {A backbone-search heuristic for efficient solving of hard 3-SAT formulae},
CROSSREF = {IJCAI01},
URL = {http://www.laria.u-picardie.fr/~dequen/sat/cnfs_ijcai01.ps.gz}
}
@INPROCEEDINGS{Ernst1997a,
AUTHOR = {Michael D. Ernst and Todd D. Millstein and Daniel S.
Weld},
TITLE = {Automatic {SAT}-Compilation of Planning Problems},
CROSSREF = {IJCAI97},
PAGES = {1169-1176}
}
@ARTICLE{Even1976a,
AUTHOR = {S. Even and A. Ital and A. Shamir},
TITLE = {On the complexity of timetable and multicommodity flow
problems},
JOURNAL = {SIAM Journal on Computing},
VOLUME = {5},
PAGES = {691-703},
YEAR = 1976
}
@ARTICLE{Franco1991a,
AUTHOR = {John Franco},
TITLE = {Elimination of infrequent variables improves average
case performance of satisfiability algorithms},
JOURNAL = {SIAM Journal on Computing },
VOLUME = {20},
PAGES = {1119-1127},
YEAR = 1991
}
@ARTICLE{Franco1983a,
AUTHOR = {John Franco and Marvin Paull},
TITLE = {Probabilistic analysis of the davis putnam procedure for solving the satisfiability problem},
JOURNAL = {Discrete Applied Mathematics},
YEAR = 1983,
VOLUME = 5,
PAGES = {77--87}
}
@PHDTHESIS{Freeman1995a,
AUTHOR = {Jon W. Freeman},
TITLE = {Improvements to Propositional Satisfiability Search
Algorithms},
SCHOOL = {Departement of computer and Information
science, University of Pennsylvania},
ADDRESS = {Philadelphia},
YEAR = 1995,
URL = {ftp://ftp.cis.upenn.edu/pub/freeman/thesis.ps.gz}
}
@INPROCEEDINGS{Genisson1994a,
AUTHOR = {Richard G\'enisson and Pierre Si\'egel},
TITLE = {A polynomial method for sub-clauses production},
BOOKTITLE = {Proceedings of the Sixth International Conference on
Artificial Intelligence: Methodology, Systems,
Applications (AIMSA'94)},
PAGES = {25-34},
YEAR = 1994
}
@INPROCEEDINGS{Gent1994a,
AUTHOR = {Ian P. Gent and Toby Walsh},
TITLE = {The {SAT} phase transition},
BOOKTITLE = {Proceedings of the Eleventh European Conference on
Artificial Intelligence (ECAI'94)},
PAGES = {105-109},
YEAR = 1994,
URL = {http://dream.dai.ed.ac.uk/group/tw/papers/ECAI94.ps}
}
@INPROCEEDINGS{Gent1999b,
AUTHOR = {Ian P. Gent and Holger H. Hoos and Patrick Prosser and
Toby Walsh},
TITLE = {Morphing: Combining Structure and Randomness},
BOOKTITLE = {Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99)},
PAGES = {654-660},
ADDRESS = {Orlando, Florida},
YEAR = 1999
}
@INPROCEEDINGS{GiunchigliaMaratea2001a,
AUTHOR = {E. Giunchiglia and M. Maratea and A. Tacchella and D. Zambonin},
TITLE = {Evaluating search heuristics and optimization techniques in propositional satisfiability},
BOOKTITLE = {Proceedings of International Joint Conference on Automated Reasoning (IJCAR'01)},
YEAR = 2001,
ADDRESS = {Siena},
MONTH = {June},
NOTE = {to appear},
URL = {http://www.mrg.dist.unige.it/~enrico/ftp/01ijcar-sim.ps.gz}
}
@INCOLLECTION{Glover1993a,
AUTHOR = {F. Glover and M. Laguna},
TITLE = {Tabu Search},
BOOKTITLE = {Modern Heuristic Techniques for Combinatorial Problems},
PUBLISHER = {Blackwell Scientific Publishing},
PAGES = {70-141},
ADDRESS = {Oxford},
YEAR = 1993
}
@INPROCEEDINGS{Gomes1998a,
AUTHOR = {Carla P. Gomes and Bart Selman and Henry Kautz},
TITLE = {Boosting Combinatorial Search Through Randomization},
BOOKTITLE = {Proceedings of the Fifteenth National Conference on
Artificial Intelligence (AAAI'98)},
PAGES = {431-437},
ADDRESS = {Madison, Wisconsin},
YEAR = 1998,
URL = {http://www.cs.washington.edu/homes/kautz/papers/aaai98boost.ps}
}
@INPROCEEDINGS{Goldberg2002a,
AUTHOR = {E. Goldberg and Y. Novikov},
TITLE = {{BerkMin}: A Fast and Robust
{SAT}-Solver},
BOOKTITLE = {Design, Automation, and Test in Europe (DATE '02)},
MONTH = MAR,
YEAR = {2002},
PAGES = {142--149},
URL = {http://www.ece.cmu.edu/~mvelev/goldberg_novikov_date02.pdf}
}
@INCOLLECTION{Gomes2000a,
AUTHOR = {Carla P. Gomes and Bart Selman and Nuno Crato and
Henry Kautz},
TITLE = {Heavy-{T}aily {P}henomena in {S}atisfiability},
CROSSREF = {SAT2000},
PAGES = {15-41}
}
@INPROCEEDINGS{Grigoriev1998a,
AUTHOR = {Grigoriev, D.},
TITLE = {{T}seitin's Tautologies and Lower Bounds for {N}ullstellensatz Proofs},
CROSSREF = {FOCS98}
}
@TECHREPORT{Groote1999a,
AUTHOR = {J. F. Groote and J. P. Warners},
TITLE = {The propositional formula checker HeerHugo},
ADDRESS = {Amsterdam},
NUMBER = {SEN-R9905},
INSTITUTION = {Centrum voor Wiskunde en Informatica (CWI)},
YEAR = 1999,
URL = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9905.ps.Z}
}
@INCOLLECTION{Groote2000a,
AUTHOR = {J. F. Groote and J. P. Warners},
TITLE = {The propositional formula checker {HeerHugo}},
CROSSREF = {SAT2000},
PAGES = {261--281}
}
@TECHREPORT{Groote2000b,
AUTHOR = {Jan Friso Zantema Groote and Hans Hans},
TITLE = {Resolution and Binary Decision Diagrams cannot
simulate each other polynomially},
NUMBER = {CS-2000-14},
YEAR = 2000,
INSTITUTION = {Utrecht University},
URL = {ftp://ftp.cs.uu.nl/pub/RUU/CS/techreps/CS-2000/2000-14.ps.gz}
}
@TECHREPORT{Gu1988a,
AUTHOR = {Jun Gu},
TITLE = {How to solve Very Large-Scale Satisfiability problem.},
YEAR = 1988,
INSTITUTION = {Technical Report UUCS-TR-88-032}
}
@INPROCEEDINGS{Gu1995a,
AUTHOR = {Jun Gu},
TITLE = {Parallel Algorithms for Satisfiability ({SAT}) Problem},
BOOKTITLE = {Parallel Processing of Discrete Optimization Problems},
PAGES = {105--161},
YEAR = 1995,
EDITOR = {P. Pardalos and M. Resende and K. Ramakrishnan},
VOLUME = 22,
SERIES = {DIMACS - Discrete Mathematics and Theoretical Computer Science},
ORGANIZATION = {American Mathematical Society}
}
@ARTICLE{Gu1992a,
AUTHOR = {Jun Gu},
TITLE = {Efficient Local Search for Very Large-Scale Satisfiability Problems},
JOURNAL = {SIGART Bulletin},
YEAR = 1992,
VOLUME = 3,
NUMBER = 1,
PAGES = {8--12}
}
@INCOLLECTION{Gu1997a,
AUTHOR = {Jun Gu and Paul W. Purdom and John Franco and Benjamin
W. Wah},
TITLE = {{Algorithms for the satisfiability ({SAT}) Problem: A
survey}},
BOOKTITLE = {Satisfiability Problem: Theory and applications},
PUBLISHER = {American Mathematical Society},
EDITOR = {Du, Ding-Zhu and Gu, Jun and Pardalos, Panos},
SERIES = {DIMACS Series in Discrete Mathematics and Theoretical
Computer Science},
PAGES = {19-152},
YEAR = 1997
}
@INPROCEEDINGS{GLST98a,
AUTHOR = {Guruswami, Venkatesan and Lewin, Daniel and Sudan, Madhu and Trevisan, Luca},
TITLE = {A tight characterization of {NP} with 3 query {PCPs}},
CROSSREF = {FOCS98}
}
@INPROCEEDINGS{Hamadi1997a,
AUTHOR = {Youssef Hamadi and David Merceron},
TITLE = {Reconfigurable Architectures: A new Vision for
Optimization Problems},
BOOKTITLE = {Proceedings of the Third International Conference on
Principles and Practice of Constraint Programming
(CP'97), Lecture Notes in Computer Science N°1330},
EDITOR = {Smolka, Gert},
PAGES = {209-221},
ADDRESS = {Linz (Austria)},
YEAR = 1997
}
@ARTICLE{Hamadi1999a,
AUTHOR = {Youssef Hamadi and David Merceron},
TITLE = {Architectures reconfigurables et traitement de
problèmes {NP}-difficiles : un nouveau domaine
d'application},
JOURNAL = {Technique et Science Informatiques (A paraitre)},
YEAR = 1999
}
@INPROCEEDINGS{Harrison1996a,
AUTHOR = {John Harrison},
TITLE = {St{\aa}lmarck's algorithm as a {HOL} Derived Rule},
EDITOR = {Joakim von Wright and Jim Grundy and John Harrison},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1125,
ADDRESS = {Turku, Finland},
DATE = {26--30 August 1996},
YEAR = 1996,
PUBLISHER = {Springer Verlag},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/stalmarck.html}
}
@INPROCEEDINGS{Hastad1997a,
AUTHOR = {Johan H{\aa}stad},
TITLE = {Some Optimal Inapproximability Results},
BOOKTITLE = {Proceedings of the twenty-ninth annual {ACM} Symposium on Theory of Computing, El Paso, TX, USA},
PAGES = {1--10},
YEAR = 1997,
PUBLISHER = {ACM Press}
}
@ARTICLE{Hirsch2000a,
AUTHOR = {Edward A. Hirsch},
TITLE = {{SAT} Local Search Algorithms: Worst-Case Study},
JOURNAL = {Journal of Automated Reasonning},
YEAR = 2000,
VOLUME = 24,
NUMBER = {1/2},
MONTH = {February},
PAGES = {127--143},
URL = {http://logic.pdmi.ras.ru/~hirsch/papers/swatfull.ps.gz}
}
@ARTICLE{Hircsh2000b,
AUTHOR = {Edward A. Hirsch},
TITLE = {New Worst-Case Upper Bounds for {SAT}},
JOURNAL = {Journal of Automated Reasonning},
YEAR = 2000,
VOLUME = 24,
NUMBER = 4,
PAGES = {397--420},
URL = {http://logic.pdmi.ras.ru/~hirsch/papers/sodafull.ps.gz}
}
@ARTICLE{Hir2000c,
AUTHOR = {Hirsch, Edward A.},
TITLE = {{SAT} Local Search Algorithms: Worst-Case Study},
YEAR = {2000},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {24},
NUMBER = {1/2},
PAGES = {127--143},
NOTE = {Also reprinted in ``Highlights of Satisfiability Research in the Year 2000'', Volume 63 in Frontiers in Artificial Intelligence and Applications, IOS Press}
}
@ARTICLE{Hooker1995a,
AUTHOR = {J. N. Hooker and V. Vinay},
TITLE = {Branching Rules for Satisfiability},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {15},
PAGES = {359-383},
YEAR = 1995
}
@INPROCEEDINGS{Hoos1999a,
AUTHOR = {Holger H. Hoos},
TITLE = {SAT-Encodings, Search Space Structure, and local
Search Performance},
CROSSREF = {IJCAI99},
PAGES = {296-302},
URL = {http://www.cs.ubc.ca/spider/hoos/Publ/ijcai99-enc.ps.gz}
}
@INPROCEEDINGS{Hoos1999b,
AUTHOR = {Holger H. Hoos},
TITLE = {On the Run-Time Behaviour of Stochastic Local Search
Algorithms for SAT},
BOOKTITLE = {Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99)},
PAGES = {661-666},
ADDRESS = {Orlando, Florida},
KEYWORDS = {A·lire, Algorithmes, Heuristique, kwDANIELpp,
Recherche·locale, SAT, },
YEAR = 1999,
URL = {http://www.cs.ubc.ca/spider/hoos/Publ/aaai99-pac.ps}
}
@ARTICLE{Hoos2000a,
AUTHOR = {Holger H. Hoos and Thomas St{\"u}tzle},
TITLE = {Local Search Algorithms for {SAT}: An Empirical Evaluation},
JOURNAL = {Journal of Automated Reasoning},
YEAR = 2000,
VOLUME = 24,
NUMBER = 4,
PAGES = {421--481}
}
@INCOLLECTION{Hoos2000b,
AUTHOR = {Holger H. Hoos and Thomas St{\"u}tzle},
TITLE = {{SATLIB: An Online Resource for Research on SAT}},
CROSSREF = {SAT2000},
PAGES = {283--292},
URL = {http://aida.intellektik.informatik.tu-darmstadt.de/~tom/publications/SATLIB.ps.gz}
}
@INPROCEEDINGS{IPZ98,
AUTHOR = {Impagliazzo, Russel and Paturi, Ramamohan and Zane, Francis},
TITLE = {Which Problems Have Strongly Exponential Complexity?},
PAGES = {653--662},
CROSSREF = {FOCS98},
URL = {http://cm.bell-labs.com/cm/ms/who/francis/papers/focs98-subexp.ps},
URL = {http://cm.bell-labs.com/cm/ms/who/francis/papers/focs98-subexp.pdf}
}
@ARTICLE{Jeannicot1988a,
AUTHOR = {S Jeannicot and Laurent Oxuzoff and Antoine Rauzy},
TITLE = {Evaluation sémantique en calcul propositionnel : une
propriété de coupure pour rendre plus efficace la
procédure de Davis et Putnam},
JOURNAL = {La Revue d'Intelligence Artificielle},
VOLUME = {1},
NUMBER = {2},
PAGES = {41-60},
YEAR = 1988
}
@ARTICLE{Jeroslow1990a,
AUTHOR = {R. J. Jeroslow and J. Wang},
TITLE = {Solving propositional satisfiability problems},
JOURNAL = {Annals of Mathematics and Artificial Intelligence},
VOLUME = {1},
PAGES = {167-188},
YEAR = 1990
}
@ARTICLE{Johnson1974a,
AUTHOR = {David S. Johnson},
TITLE = {Approximation Algorithms for Combinatorial Problems},
JOURNAL = {Journal of Computer and System Sciences},
YEAR = 1974,
VOLUME = 9,
PAGES = {256--278}
}
@INPROCEEDINGS{Jurkowiak2001a,
AUTHOR = {Bernard Jurkowiak and Chu-Min Li and Gil Utard},
TITLE = {{P}arallelizing {SATZ} {U}sing {D}ynamic {W}orkload {B}alancing},
CROSSREF = {SAT2001}
}
@ARTICLE{Kamath1990a,
AUTHOR = {Amit P. Kamath and Narendra K. Karmarkar and K. G. Ramakrishnan and Mauricio G. C. Resende},
TITLE = {Computational experience with an interior point algorithm on the satisfiability problem},
JOURNAL = {Annals of Operations Research},
YEAR = 1990,
VOLUME = 25,
PAGES = {43--58}
}
@INPROCEEDINGS{Karloff1997a,
AUTHOR = {Howard Karloff and Uri Zwick},
TITLE = {A 7/8-approximation algorithm for {MAX 3SAT}?},
BOOKTITLE = {Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, Miami Beach, FL, USA},
YEAR = 1997,
ORGANIZATION = {IEEE},
PUBLISHER = {IEEE Press}
}
@INPROCEEDINGS{Kautz1992a,
AUTHOR = {Henry A. Kautz and Bart Selman},
TITLE = {Planning as Satisfiability},
BOOKTITLE = {Proceedings of the Tenth European Conference on
Artificial Intelligence (ECAI'92)},
PAGES = {359-363},
YEAR = 1992,
URL = {http://www.cs.washington.edu/homes/kautz/papers/satplan.ps}
}
@INPROCEEDINGS{Kautz1996a,
AUTHOR = {Henry A. Kautz and Bart Selman},
TITLE = {Pushing the Envelope : Planning, Propositional Logic,
and Stochastic Search},
BOOKTITLE = {Proceedings of the Twelfth National Conference on
Artificial Intelligence (AAAI'96)},
PAGES = {1194-1201},
YEAR = 1996,
URL = {http://www.cs.washington.edu/homes/kautz/papers/plan.ps}
}
@INPROCEEDINGS{Kautz1996b,
AUTHOR = {Henry A. Kautz and David McAllester and Bart Selman},
TITLE = {Encoding Plans in Propositional Logic},
BOOKTITLE = {Proceedings of the Fifth International Conference on
the Principle of Knowledge Representation and Reasoning
(KR'96)},
PAGES = {374-384},
YEAR = 1996,
URL = {http://www.cs.washington.edu/homes/kautz/papers/plankr96.ps}
}
@INPROCEEDINGS{Kautz1999a,
AUTHOR = {Henry A. Kautz and Bart Selman},
TITLE = {Unifying {SAT}-based and Graph-based Planning},
CROSSREF = {IJCAI99},
PAGES = {318--325},
URL = {http://www.cs.washington.edu/homes/kautz/papers/ijcai99blackbox.ps}
}
@INPROCEEDINGS{Kim1994a,
AUTHOR = {Sun Kim and Hantao Zhang},
TITLE = {ModGen: Theorem proving by model generation},
BOOKTITLE = {Proceedings of the Twelfth National Conference on
Artificial Intelligence (AAAI'94)},
PAGES = {162-167},
ADDRESS = {Seattle},
YEAR = 1994
}
@INPROCEEDINGS{Kirkpatrick1994a,
AUTHOR = {Scott Kirkpatrick and G\'eza Gy\"orgyi and Naftali Tishby and Lidror Troyansky},
TITLE = {The Statistical Mechanics of $k$-Satisfaction},
BOOKTITLE = {Advances in Neural Information Processing Systems},
PAGES = {439--446},
YEAR = 1994,
VOLUME = 6,
PUBLISHER = {Morgan Kaufmann}
}
@ARTICLE{Koutsoupias1992a,
AUTHOR = {Elias Koutsoupias and Christos H. Papadimitriou},
TITLE = {On the Greedy Algorithm for Satisfiability},
JOURNAL = {Information Processing Letters},
YEAR = 1992,
VOLUME = 43,
NUMBER = 1,
PAGES = {53--55}
}
@ARTICLE{Kowalsky1971a,
AUTHOR = {R. A. Kowalsky and D. Kuehner},
TITLE = {Linear Resolution with Selection Function},
JOURNAL = {Artificial Intelligence},
VOLUME = {2},
PAGES = {227-260},
YEAR = 1971
}
@MISC{Kullmann1998a,
AUTHOR = {O. Kullmann},
TITLE = {Heuristics for {SAT} algorithms:
Searching for some foundations},
MONTH = SEP,
YEAR = {1998},
NOTE = {23 pages, updated September 1999 w.r.t. running times,
url = {http://cs-svr1.swan.ac.uk/~csoliver/heur2letter.ps.gz}}
}
@ARTICLE{Larrabee1992a,
AUTHOR = {Tracy Larrabee},
TITLE = {{Test Pattern Generation Using Boolean Satisfiability}},
JOURNAL = {IEEE Transactions on Computer-Aided Design},
PAGES = {6--22},
VOLUME = 11,
NUMBER = 1,
YEAR = 1992,
MONTH = {January},
URL = {http://sctest.cse.ucsc.edu/papers/1992/tcad.sat.ps}
}
@INPROCEEDINGS{LeBerre2001a,
AUTHOR = {{Le Berre}, Daniel},
TITLE = {Exploiting the real power of Unit Propagation Lookahead},
CROSSREF = {SAT2001}
}
@INPROCEEDINGS{Li1997a,
AUTHOR = {Chu-Min Li and Anbulagan},
TITLE = {Heuristics Based on Unit Propagation for
Satisfiability Problems},
CROSSREF = {IJCAI97},
PAGES = {366-371},
URL = {http://www.laria.u-picardie.fr/~cli/Publis/up.ps}
}
@UNPUBLISHED{Li1999a,
AUTHOR = {Chu-Min Li},
TITLE = {Equivalency Reasoning to Solve a Class of Hard Sat
Problems},
NOTE = {available at http://www.research.att.com/~selman/challenge},
YEAR = 1999,
URL = {http://www.laria.u-picardie.fr/~cli/Publis/parity.ps}
}
@ARTICLE{Li1999b,
AUTHOR = {Chu-Min Li},
TITLE = {A constrained based approach to narrow search trees
for satisfiability},
JOURNAL = {Information processing letters},
VOLUME = 71,
PAGES = {75--80},
YEAR = 1999,
URL = {http://www.laria.u-picardie.fr/~cli/Publis/ipl0199.ps}
}
@INPROCEEDINGS{Li2000a,
AUTHOR = {Chu-Min Li and Sylvain Gérard},
TITLE = {On the limit of Branching Rules for Hard Random
Unsatisfiable {3-SAT}},
BOOKTITLE = {Proceedings of the 14th European Conference on
Artificial Intelligence (ECAI-2000)},
PAGES = {98--102},
ADDRESS = {Berlin},
YEAR = 2000,
URL = {http://www.laria.u-picardie.fr/~cli/Publis/minweight.ps}
}
@INPROCEEDINGS{Li2000b,
AUTHOR = {Chu-Min Li},
TITLE = {{Integrating Equivalency reasoning into Davis-Putnam
procedure}},
CROSSREF = {AAAI00},
PAGES = {291--296},
URL = {http://www.laria.u-picardie.fr/~cli/Publis/aaai2000.ps}
}
@INPROCEEDINGS{Liang1998a,
AUTHOR = {Dongmin Liang and Wei Li},
TITLE = {Multi-Strategy Local Search for {SAT} problem},
BOOKTITLE = {Proceedings of the Thirteenth European Conference on
Artificial Intelligence (ECAI'98)},
PAGES = {234-238},
YEAR = 1998
}
@INPROCEEDINGS{Lynce2001b,
AUTHOR = {In\^es Lynce and Luis Baptista and Jo\~ao P. Marques Silva},
TITLE = {Stochastic Systematic Search Algorithms for Satisfiability},
CROSSREF = {SAT2001},
URL = {http://sat.inesc.pt/~ines/publications/sat-lics01.ps.gz}
}
@MASTERSTHESIS{Lynce2001a,
AUTHOR = {In\^es Lynce},
TITLE = {{Algebraic Simplification Techniques for Propositional Satisfiability}},
SCHOOL = {Instituto Superior T\'ecnico},
YEAR = 2001,
ADDRESS = {Lisboa, Portugal},
MONTH = {March},
URL = {http://sat.inesc.pt/~ines/publications/msc.ps.gz}
}
@INPROCEEDINGS{Littman1999a,
AUTHOR = {Michael L. Littman},
TITLE = {Initial Experiments in Stochastic Satisfiability},
BOOKTITLE = {Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99)},
PAGES = {667-672},
ADDRESS = {Orlando, Florida},
YEAR = 1999
}
@INPROCEEDINGS{Marques-Silva1996a,
AUTHOR = {Joao P. Marques-Silva and Karem A. Sakallah},
TITLE = {{GRASP - A New Search Algorithm for Satisfiability}},
BOOKTITLE = {Proceedings of IEEE/ACM International Conference on
Computer-Aided Design},
PAGES = {220-227},
MONTH = {November},
YEAR = 1996,
URL = {http://sat.inesc.pt/~jpms/research/papers/iccad96/iccad96.ps.gz}
}
@INPROCEEDINGS{Marques-Silva1999a,
AUTHOR = {Joao P. Marques-Silva and Thomas Glass},
TITLE = {{Combinational Equivalence Checking Using
Satisfiability and Recursive Learning}},
BOOKTITLE = {Proceedings of the IEEE/ACM Design, Automation and
Test in Europe Conference (DATE)},
YEAR = 1999,
URL = {http://sat.inesc.pt/~jpms/research/papers/date99/cec.ps.gz}
}
@INPROCEEDINGS{Marques-Silva2000a,
AUTHOR = {Joao P. Marques-Silva and Karem A. Sakallah},
TITLE = {{Boolean Satisfiability in Electronic Design Automation}},
BOOKTITLE = {Proceedings of the IEEE/ACM Design Automation
Conference (DAC)},
MONTH = {June},
YEAR = 2000,
URL = {http://sat.inesc.pt/~jpms/research/papers/dac2000/dac2000.ps.gz}
}
@INPROCEEDINGS{Marques-Silva2000b,
AUTHOR = {Joao P. Marques-Silva},
TITLE = {{Algebraic Simplification Techniques for Propositional
Satisfiability}},
BOOKTITLE = {Proceedings of the 6th International Conference on
Principles and Practice of Constraint Programming
(CP'2000)},
YEAR = 2000,
MONTH = {September},
URL = {http://sat.inesc.pt/~jpms/research/papers/cp2000/cp2000-algeb.ps.gz}
}
@INPROCEEDINGS{Massacci1999a,
AUTHOR = {Fabio Massacci},
TITLE = {Using Walk-SAT and Rel-SAT for Cryptographic Key
Search},
CROSSREF = {IJCAI99},
PAGES = {290--295}
}
@INPROCEEDINGS{Mazure1997a,
AUTHOR = {B. Mazure and L. Saïs and E. Grégoire},
TITLE = {Tabu search for SAT},
BOOKTITLE = {Proceedings of the Fourteenth National Conference on
Artificial Intelligence (AAAI'97)},
PAGES = {281-285},
ADDRESS = {Providence (Rhode Island USA)},
YEAR = 1997
}
@ARTICLE{Mazure1998a,
AUTHOR = {Bertrand Mazure and Lakhdar Saïs and Eric Grégoire},
TITLE = {Boosting Complete Techniques thanks to local search
methods},
JOURNAL = {Annals of Mathematics and Artificial Intelligence},
VOLUME = {22},
PAGES = {319-331},
YEAR = 1998
}
@PHDTHESIS{Mazure1999a,
AUTHOR = {Bertrand Mazure},
TITLE = {De la Satisfiabilité à la Compilation de Bases de
Connaissances Propositionnelles},
SCHOOL = {Thèse de doctorat de l'Université d'Artois},
ADDRESS = {Lens},
YEAR = 1999
}
@INPROCEEDINGS{McAllester1997a,
AUTHOR = {David McAllester and Bart Selman and Henry Kautz},
TITLE = {Evidence for Invariants in Local Search},
BOOKTITLE = {Proceedings of the Fourteenth National Conference on
Artificial Intelligence (AAAI'97)},
PAGES = {321-326},
ADDRESS = {Providence, Rhode Island},
YEAR = 1997
}
@TECHREPORT{McCune1994a,
AUTHOR = {William McCune},
TITLE = {A Davis-Putnam Program and its Application to Finite
First-Order Model Search: Quasigroup Existence Problem},
YEAR = 1994,
INSTITUTION = {Technical Memorandum ANL/MCS-TM-194}
}
@INPROCEEDINGS{Mitchell1992a,
AUTHOR = {David Mitchell and Bart Selman and Hector Levesque},
TITLE = {Problem Solving: Hardness and Easiness - Hard and Easy Distributions of {SAT} Problems},
BOOKTITLE = {Proceeding of the 10th National Conference on Artificial Intelligence (AAAI-92), San Jose, California},
PAGES = {459--465},
YEAR = 1992,
PUBLISHER = {AAAI Press, Menlo Park, California, USA}
}
@INPROCEEDINGS{MR98,
AUTHOR = {Molloy, Michael and Reed, Bruce},
TITLE = {Further Algorithmic Aspects of the {L}ocal {L}emma},
CROSSREF = {FOCS98}
}
@ARTICLE{Monien1985a,
AUTHOR = {B Monien and E. Speckenmeyer},
TITLE = {Solving Satisfiability in less than 2n steps},
JOURNAL = {Discrete Applied Mathematics},
VOLUME = {10},
PAGES = {287-295},
YEAR = 1985
}
@INPROCEEDINGS{Moskewicz2001a,
AUTHOR = {Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao
and Lintao Zhang and Sharad Malik},
TITLE = {{Chaff: Engineering an Efficient {SAT} Solver}},
BOOKTITLE = {Proceedings of the 38th Design Automation Conference (DAC'01)},
YEAR = 2001,
MONTH = {June},
URL = {http://www.ee.princeton.edu/~chaff/DAC2001v56.pdf}
}
@PHDTHESIS{Oxusoff1989a,
AUTHOR = {Laurent Oxusoff and Antoine Rauzy},
TITLE = {L'évaluation sémantique en calcul propositionnel},
SCHOOL = {Thèse de doctorat de l'Université de Provence,
GIA-Luminy},
ADDRESS = {Marseille},
YEAR = 1989
}
@INPROCEEDINGS{Parkes1996a,
AUTHOR = {Andrew J. Parkes and Joachim P. Walser},
TITLE = {Tuning Local Search for Satisfiability Testing},
BOOKTITLE = {Proceedings of the Thirteenth National Conference on
Artificial Intelligence (AAAI'96)},
PAGES = {356-362},
YEAR = 1996
}
@INPROCEEDINGS{PPSZ98,
AUTHOR = {Paturi, Ramamohan and Pudl\'{a}k, Pavel and Saks, Michael E. and Zane, Francis},
TITLE = {An Improved Exponential-time Algorithm for k-{SAT}},
CROSSREF = {FOCS98},
PAGES = {628--637},
URL = {http://cm.bell-labs.com/cm/ms/who/francis/papers/focs98-sat2.ps},
URL = {http://cm.bell-labs.com/cm/ms/who/francis/papers/focs98-sat2.pdf}
}
@BOOK{Prawitz1965a,
AUTHOR = {D. Prawitz},
TITLE = {Natural Deduction: A Proof Theoretical Study},
PUBLISHER = {Almquist & Wiksell},
YEAR = 1965
}
@INPROCEEDINGS{Prcovic1999a,
AUTHOR = {Nicolas Prcovic and Bertrand Neveu},
TITLE = {Etude théorique sur les recherches entrelacées et à
divergence limitée},
BOOKTITLE = {Actes de Cinquièmes Journées Nationales sur la
Résolution Pratique de Problèmes NP-Complets (JNPC'99)},
PAGES = {85-94},
ADDRESS = {Lyon},
YEAR = 1999
}
@INPROCEEDINGS{Rana1998a,
AUTHOR = {Soraya Rana and Robert B. Heckendorn and Darrell
Whitley},
TITLE = {A Tractable Walsh Analysis of {SAT} and its implications
for Genetic Algorithms},
BOOKTITLE = {Proceedings of the Fifteenth National Conference on
Artificial Intelligence (AAAI'98)},
PAGES = {392-397},
YEAR = 1998
}
@INPROCEEDINGS{Rauzy1999a,
AUTHOR = {Antoine Rauzy and Lackdar Saïs and L. Brisoux},
TITLE = {Calcul propositionnel : vers une extension du
formalisme},
BOOKTITLE = {Actes des Cinquièmes Journées Nationales sur la
Résolution Pratique de Problèmes NP-complets (JNPC'99)},
PAGES = {189-198},
ADDRESS = {Lyon},
YEAR = 1999
}
@PHDTHESIS{Rish1999a,
AUTHOR = {Irina Rish},
TITLE = {Efficient Reasoning in Graphical Models},
SCHOOL = {University of California, Irvine},
YEAR = {1999},
URL = {http://www.ics.uci.edu/~csp/r81-irina_thesis.pdf}
}
@INPROCEEDINGS{Rish1996a,
AUTHOR = {Irina Rish and Rina Dechter},
TITLE = {To Guess or to Think? Hybrid Algorithms for {SAT}},
BOOKTITLE = {proceedings of the International Conference on Principles and Pratice of Constraint Programming (CP'96)},
PAGES = {},
YEAR = {1996},
URL = {http://www.ics.uci.edu/~csp/r49-toguessorthinkCP96.ps}
}
@ARTICLE{Rish2000a,
AUTHOR = {Irina Rish and Rina Dechter},
TITLE = {Resolution versus Search: Two Strategies for {SAT}},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {24},
NUMBER = {1/2},
PAGES = {225-275},
YEAR = {2000},
URL = {http://www.ics.uci.edu/~csp/R80.pdf}
}
@ARTICLE{Robinson1965a,
AUTHOR = {J. A. Robinson},
TITLE = {A machine-oriented logic based on the resolution
principle},
JOURNAL = {Journal of the ACM},
VOLUME = 12,
NUMBER = 1,
MONTH = {January},
PAGES = {23-41},
YEAR = 1965,
URL = {http://www.acm.org/pubs/articles/journals/jacm/1965-12-1/p23-robinson/p23-robinson.pdf}
}
@INPROCEEDINGS{Schoning1999a,
AUTHOR = {Uwe Sch\"oning},
TITLE = {A Probabilistic Algorithm for k-{SAT} and Constraint Satisfaction Problems},
BOOKTITLE = {Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science, New York, NY, USA},
PAGES = {410-414},
YEAR = 1999,
PUBLISHER = {IEEE Press}
}
@INPROCEEDINGS{Schrag1996b,
AUTHOR = {Robert C. Schrag},
TITLE = {Compilation of critically Constrained Knowledge Bases},
BOOKTITLE = {Proceedings of the Thirteenth National Conference on
Artificial Intelligence (AAAI'96)},
PAGES = {510-515},
YEAR = 1996
}
@ARTICLE{Schulz1988a,
AUTHOR = {M. H. Schulz and E. Trischler and T. M. Sarfert},
TITLE = {{SOCRATES} : {A} Highly Efficient Automatic Test Pattern Generation System},
JOURNAL = {IEEE Transactions on Computer-Aided Design},
PAGES = {126--137},
VOLUME = 7,
NUMBER = 1,
YEAR = 1988
}
@INPROCEEDINGS{Selman1992a,
AUTHOR = {David Mitchell and Bart Selman and Hector Levesque },
TITLE = {Hard and easy distribution of {SAT} problems},
BOOKTITLE = {Proceedings of the Tenth National Conference on
Artificial Intelligence (AAAI'92)},
PAGES = {440-446},
YEAR = 1992
}
@INPROCEEDINGS{Selman1992b,
AUTHOR = {Bart Selman and Hector Levesque and D. Mitchell},
TITLE = {A new method for solving hard satisfiability problems},
BOOKTITLE = {Proceedings of the Tenth National Conference on
Artificial Intelligence (AAAI'92)},
PAGES = {459-465},
YEAR = 1992
}
@INPROCEEDINGS{Selman1993a,
AUTHOR = {Bart Selman and Henry A. Kautz},
TITLE = {Domain-independant Extensions to {GSAT} : Solving Large
Structured Variables},
BOOKTITLE = {Proceedings of the Thirteenth International Joint
Conference on Artificial Intelligence (IJCAI'93)},
PAGES = {290-295},
YEAR = 1993,
URL = {http://www.cs.cornell.edu/home/selman/papers-ftp/93.ijcai.gsatext.ps}
}
@INCOLLECTION{Selman1993b,
AUTHOR = {Bart Selman and Henry A. Kautz and Bram Cohen},
TITLE = {Local search strategies for satisfiability testing},
CROSSREF = {Johnson1996a},
PAGES = {521-532},
URL = {http://www.cs.cornell.edu/home/selman/papers-ftp/96.dimacs.walksat.ps}
}
@INPROCEEDINGS{Selman1994a,
AUTHOR = {Bart Selman and Henry A. Kautz and Bram Cohen},
TITLE = {Noise strategies for improving local search},
BOOKTITLE = {Proceedings of the Twelfth National Conference on
Artificial Intelligence (AAAI'94)},
PAGES = {337-343},
ADDRESS = {Seattle},
KEYWORDS = {Algorithmes, Heuristique, Recherche·locale, SAT, },
YEAR = 1994,
URL = {http://www.cs.cornell.edu/home/selman/papers-ftp/94.aaai.loc.ps}
}
@INPROCEEDINGS{Selman1997a,
AUTHOR = {Bart Selman and Henry A. Kautz and David A. McAllester},
TITLE = {Ten Challenges in Propositional Reasoning and Search},
BOOKTITLE = {Proceedings of the Fifteenth International Joint
Conference on Artificial Intelligence (IJCAI'97)},
PAGES = {50-54},
YEAR = 1997,
URL = {http://www.cs.cornell.edu/home/selman/papers-ftp/97.ijcai.challenge.ps}
}
@INPROCEEDINGS{Sheeran1998a,
AUTHOR = {Mary Sheeran and Gunnar St{\aa}lmark},
TITLE = {A tutorial on St{\aa}lmark's proof procedure for
propositional logic},
BOOKTITLE = {Volume 152 of Lecture Notes in Computer Science},
PAGES = {82-99},
PUBLISHER = {Springer Verlag},
YEAR = 1998
}
@PHDTHESIS{Siegel1987a,
AUTHOR = {Pierre Siegel},
TITLE = {Représentation et utilisation de la connaissance en
calcul propositionnel},
SCHOOL = {Thèse d'état, Université de Provence, GIA-Luminy,
Marseille},
ADDRESS = {Marseille},
YEAR = 1987
}
@INPROCEEDINGS{Simon2001a,
AUTHOR = {Laurent Simon and Philippe Chatalic},
TITLE = {{SATEx}: a Web-based Framework for {SAT} Experimentation},
CROSSREF = {SAT2001},
NOTE = {http://www.lri.fr/~simon/satex/satex.php3},
PS = {http://www.lri.fr/~simon/recherche/papiers/simon-sat2001.ps.gz},
PDF = {http://www.lri.fr/~simon/recherche/papiers/simon-sat2001.pdf}
}
@ARTICLE{Singer2000a,
AUTHOR = {Josh Singer and Ian Gent and Alan Smaill},
TITLE = {{Backbone Fragility and the Local Search Cost Peak}},
JOURNAL = {Journal of Artificial Intelligence Research},
YEAR = 2000,
VOLUME = 12,
PAGES = {235--270},
URL = {http://www.dai.ed.ac.uk/daidb/students/joshuas/frag_back5.pdf}
}
@INCOLLECTION{Speckenmeyer1997a,
AUTHOR = {Ewald Speckenmeyer and Max B{\"o}hm and Peter Heusch},
TITLE = {On the Imbalance of Distributions of Solutions of {CNF}-Formulas and its Impact on Satisfiability Solvers},
BOOKTITLE = {Satisfiability Problem: Theory and Applications},
PAGES = {669--676},
PUBLISHER = {American Mathematical Society},
YEAR = 1997,
EDITOR = {Dingyhu Du and Jun Gu and Panos M. Pardalos},
VOLUME = 35,
SERIES = {DIMACS Series in Discrete Mathematics and Theoretical Computer Science}
}
@TECHREPORT{Stalmarck1989a,
AUTHOR = {G. St{\aa}lmarck},
TITLE = {A system for determining Propositional Logic Theorems
by Applying Values and Rules to Triplets that are
generated from a formula},
INSTITUTION = {European Patent N° 0403 454 (1995), US Patent N° 5 276
897, Swedish Patent N° 467 076 (1989)},
YEAR = 1989
}
@ARTICLE{Stephan1996a,
AUTHOR = {P. Stephan and R. Brayton and A. Sangiovanni-Vincentelli},
TITLE = {{Combinational Test Generation Using Satisfiability}},
JOURNAL = {IEEE Transactions on Computer-Aided Design},
VOLUME = 15,
NUMBER = 9,
PAGES = {1167--1176},
MONTH = {September},
YEAR = 1996
}
@INPROCEEDINGS{Tafertshofer1999a,
AUTHOR = {P. Tafertshofer and A. Ganz},
TITLE = {{SAT Based ATPG Using Fast Justification and Propagation in the Implication Graph}},
BOOKTITLE = {Proceedings of the International Conference on Computer-Aided Design},
YEAR = 1999,
URL = {http://eda.ei.tum.de/~pat/pat_dir/publications/pat/iccad99.ps.gz}
}
@INPROCEEDINGS{Tafertshofer1997a,
AUTHOR = {P. Tafertshofer and A. Ganz and M. Henftling},
TITLE = {{A SAT-Based Implication Engine for Efficient ATPG, Equivalence Checking, and Optimization of Netlists}},
BOOKTITLE = {Proceedings of the International Conference on Computer-Aided Design},
MONTH = {November},
YEAR = 1997,
PAGES = {648--657},
URL = {http://eda.ei.tum.de/~pat/pat_dir/publications/pat/iccad97.ps.gz}
}
@ARTICLE{Tseitin1968a,
AUTHOR = {G. S. Tseitin},
TITLE = {On the complexity of derivation in the propositional calculus},
JOURNAL = {Zapiski nauchnykh seminarov LOMI},
VOLUME = {8},
PAGES = {234--259},
YEAR = {1968},
SERIES = {Studies in constructive mathematics and mathematical logic II},
EDITOR = {A. O. Slissenko},
NOTE = {English translation of this volume: Consultants Bureau, N.Y.,
1970, pp. 115--125}
}
@ARTICLE{Urquhart1987a,
AUTHOR = {Urquhart, Alasdair},
TITLE = {Hard Examples for Resolution},
YEAR = {1987},
JOURNAL = {Journal of the Association for Computing Machinery},
VOLUME = {34},
NUMBER = {1},
PAGES = {209--219}
}
@INCOLLECTION{VanGelder1996a,
AUTHOR = {Allen {Van Gelder} and Yumi K. Tsuji},
TITLE = {{Satisfiability Testing with More Reasoning and Less Guessing}},
CROSSREF = {Johnson1996a},
URL = {ftp://ftp.cse.ucsc.edu/pub/avg/kclose-tr.ps.gz}
}
@INPROCEEDINGS{Velev2001a,
AUTHOR = {M.N. Velev and R.E. Bryant},
TITLE = {Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors},
BOOKTITLE = {Proceedings of the 38th Design Automation Conference (DAC '01)},
PAGES = {226--231},
YEAR = 2001,
MONTH = {June},
URL = {http://www.ece.cmu.edu/~mvelev/DAC01.ps.gz}
}
@INCOLLECTION{Wang1997a,
AUTHOR = {Jinchang Wang},
TITLE = {Branching rules for propositionnal satisfiability test},
BOOKTITLE = {Satisfiability Problem: Theory and applications},
PUBLISHER = {American Mathematical Society},
EDITOR = {Du, Ding-Zhu and Gu, Jun an Pardalos, Panos},
VOLUME = {DIMACS Series in Discrete Mathematics and Theoretical
Computer Science},
PAGES = {351-364},
YEAR = 1997
}
@ARTICLE{Warners1998a,
AUTHOR = {J. P. Warners and H. Van-Maaren},
TITLE = {A two phase algorithm for solving a class of hard
satisfiability problems},
JOURNAL = {Operations Research letters},
VOLUME = {23},
PAGES = {81-88},
YEAR = 1998,
URL = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9802.ps.Z}
}
@INPROCEEDINGS{Williams2000a,
AUTHOR = {Poul F. Williams and Armin Biere and Edmund M. Clarke and Anubhav Gupta},
TITLE = {{Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking}},
BOOKTITLE = {Proceedings of CAV'00},
YEAR = 2000
}
@INPROCEEDINGS{Wolfman1999a,
AUTHOR = {Steven A. Wolfman and Daniel S. Weld},
TITLE = {The LPSAT Engine and its Application to Resource
Planning},
CROSSREF = {IJCAI99},
PAGES = {310--316}
}
@INPROCEEDINGS{Wu1999a,
AUTHOR = {Zhe Wu and Benjamin W. Wah},
TITLE = {Trap Escaping Strategies in Discrete Lagrangian
Methods for Solving Hard Satisfiability and Maximum
Satisfiability Problems},
BOOKTITLE = {Proceedings of the Sixteenth National Conference on
Artificial Intelligence (AAAI'99)},
PAGES = {673-678},
ADDRESS = {Orlando, Florida},
YEAR = 1999
}
@INPROCEEDINGS{Yokoo1996a,
AUTHOR = {Makoto Yokoo and Takayuki Suyama and Hiroshi Sawada},
TITLE = {Solving Satisfiability Problems Using Field
Programmable Gate Arrays: First Results},
BOOKTITLE = {Proceedings of the Second International Conference on
Principles ans Practice of Constraint Programming
(CP'96)},
PAGES = {495-509},
ADDRESS = {Cambridge, MA, USA},
YEAR = 1996
}
@PHDTHESIS{Zan98,
AUTHOR = {Zane, Francis},
TITLE = {Circuits, {CNFs}, and Satisfiability},
YEAR = {1998},
SCHOOL = {Dept. of Computer Science and Engineering, UCSD},
URL = {http://cm.bell-labs.com/cm/ms/who/francis/papers/thesis.ps},
URL = {http://cm.bell-labs.com/cm/ms/who/francis/papers/thesis.pdf}
}
@TECHREPORT{Zhang1994a,
AUTHOR = {Hantao Zhang and Mark Stickel},
TITLE = {Implementing the Davis-Putnam algorithm by Tries},
YEAR = 1994,
INSTITUTION = {Dept. of Computer Science, University of Iowa}
}
@INPROCEEDINGS{Zhang1995a,
AUTHOR = {Jian Zhang and Hantao Zhang},
TITLE = {SEM: a System for Enumerating Models},
CROSSREF = {IJCAI95},
PAGES = {298-303},
YEAR = 1995
}
@INPROCEEDINGS{Zhang1996a,
AUTHOR = {H. Zhang and M. E. Stickel},
TITLE = {An efficient Algorithm for Unit Propagation},
BOOKTITLE = {Proceedings of the Fourth International Symposium on
Artificial Intelligence and Mathematics (AI-MATH'96)},
ADDRESS = {Fort Lauderdale (Florida USA)},
YEAR = 1996
}
@INPROCEEDINGS{Zhang1997a,
AUTHOR = {Hantao Zhang},
TITLE = {{SATO}: an efficient propositional prover},
BOOKTITLE = {Proceedings of the International Conference on
Automated Deduction (CADE'97), volume 1249 of LNAI},
PAGES = {272-275},
YEAR = 1997
}
@INPROCEEDINGS{Zhang2001a,
AUTHOR = {L. Zhang and C. F. Madigan and M. W. Moskewicz and S. Malik},
TITLE = {Efficient Conflict Driven Learning in a {B}oolean Satisfiability
Solver},
BOOKTITLE = {International Conference on Computer-Aided Design (ICCAD'01)},
MONTH = NOV,
YEAR = {2001},
PAGES = {279--285},
URL = {http://www.ee.princeton.edu/~chaff/iccad2001_final.pdf}
}
@INPROCEEDINGS{Zwick1998a,
AUTHOR = {Uri Zwick},
TITLE = {Approximation Algorithms for Constraint Satisfaction Problems Involving at Most Three Variables Per Constraint},
BOOKTITLE = {Proceedings of the ninth Annual {ACM}-{SIAM} Symposium on Discrete Algorithms, Baltimore, MD, USA},
PAGES = {201--210},
YEAR = 1998,
PUBLISHER = {ACM Press}
}
@UNPUBLISHED{satex,
AUTHOR = {Simon, Laurent},
TITLE = {S{AT}-{E}x},
NOTE = {http://www.lri.fr/~simon/satex/satex.php3},
URL = {http://www.lri.fr/~simon/satex/satex.php3},
YEAR = 2000
}
@COMMENT{{placedhereforcrossreferencing}}
@BOOK{Johnson1996a,
EDITOR = {Johnson, {D. S.} and Trick, {M. A.}},
TITLE = {Second {DIMACS} implementation challenge : cliques,
coloring and satisfiability},
BOOKTITLE = {Second {DIMACS} implementation challenge : cliques,
coloring and satisfiability},
PUBLISHER = {American Mathematical Society},
VOLUME = 26,
SERIES = {DIMACS Series in Discrete Mathematics and Theoretical
Computer Science},
URL = {http://dimacs.rutgers.edu/Challenges/},
YEAR = 1996
}
@BOOK{SAT2000,
TITLE = {S{AT}20000: {H}ighlights of {S}atisfiability {R}esearch
in the year 2000},
BOOKTITLE = {S{AT}20000: {H}ighlights of {S}atisfiability {R}esearch
in the year 2000},
PUBLISHER = {Kluwer Academic},
EDITOR = {Ian Gent and Hans {van Maaren} and Toby Walsh},
SERIES = {Frontiers in Artificial Intelligence and Applications},
YEAR = 2000
}
@PROCEEDINGS{SAT2001,
TITLE = {Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001)},
BOOKTITLE = {Electronic Notes in Discrete Mathematics},
VOLUME = 9,
PUBLISHER = {Elsevier Science Publishers},
EDITOR = {Henry Kautz and Bart Selman},
YEAR = 2001,
MONTH = {June},
NOTE = {LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001)},
URL = {http://www.elsevier.nl/locate/endm/volume9.html}
}
@PROCEEDINGS{AAAI00,
KEY = {AAAI00},
TITLE = {Proceedings of the Seventeenth National Conference in Artificial Intelligence (AAAI'00)},
BOOKTITLE = {Proceedings of the Seventeenth National Conference in Artificial Intelligence (AAAI'00)},
ADDRESS = {Austin, Texas, USA},
MONTH = {July 30--August 3},
YEAR = 2000,
URL = {http://www.aaai.org/Conferences/National/2000/aaai00.html}
}
@PROCEEDINGS{FOCS98,
TITLE = {Proceedings of the 39th Annual Symposium on Foundations of Computer Science. (FOCS-98)},
BOOKTITLE = {Proceedings of the 39th Annual Symposium on Foundations of Computer Science. (FOCS-98)},
YEAR = 1998,
MONTH = {November},
ADDRESS = {Palo Alto, CA}
}
@PROCEEDINGS{IJCAI95,
KEY = {IJCAI95},
TITLE = {Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI'95)},
BOOKTITLE = {Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI'95)},
YEAR = 1995,
ADDRESS = {Montr\' eal, Qu\'ebec, Canada},
MONTH = {August 20--25},
URL = {http://www.ijcai.org/past/ijcai-95/}
}
@PROCEEDINGS{IJCAI97,
KEY = {IJCAI97},
TITLE = {Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97)},
BOOKTITLE = {Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97)},
YEAR = 1997,
ADDRESS = {Nagoya, Japan},
MONTH = {August 23--29},
URL = {http://www.ijcai.org/past/ijcai-97/}
}
@PROCEEDINGS{IJCAI99,
KEY = {IJCAI99},
TITLE = {Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99)},
BOOKTITLE = {Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99)},
YEAR = 1999,
MONTH = {July 31-August 6},
ADDRESS = {Stockholm, Sweden},
PUBLISHER = {Morgan Kaufmann},
URL = {http://www.dsv.su.se/ijcai-99/}
}
@PROCEEDINGS{IJCAI01,
KEY = {IJCAI01},
TITLE = {Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI'01)},
BOOKTITLE = {Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI'01)},
YEAR = 2001,
ADDRESS = {Seattle, Washington, USA},
MONTH = {August 4th-10th},
URL = {http://www.ijcai-01.org/}
}
@PROCEEDINGS{IJCAR01,
KEY = {IJCAR01},
TITLE = {Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'01)},
BOOKTITLE = {Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'01)},
YEAR = 2001,
ADDRESS = {Siena, Italy},
MONTH = {June},
URL = {http://www.dii.unisi.it/~ijcar/}
}
@PROCEEDINGS{QBF2001,
TITLE = {Proceedings of QBF2001 workshop at IJCAR'01},
BOOKTITLE = {Proceedings of QBF2001 workshop at IJCAR'01},
YEAR = 2001,
EDITOR = {Uwe Egly and Rainer Feldmann and Hans Tompits},
ADDRESS = {Siena, Italy},
MONTH = {June},
URL = {http://www.uni-paderborn.de/fachbereich/AG/monien/PERSONAL/qbf2001.tar.gz}
}
This file has been generated by
bibtex2html 1.46