@comment{version 1.49 last modified 2002/07/03 19:49:51} @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{Copty2001a, author = {F. Copty and L. Fix and E. Giunchiglia and G. Kamhi and A. Tacchella and M. Vardi}, title = {Benefits of Bounded Model Checking at an Industrial Setting}, booktitle = {Proc. of CAV}, year = 2001, series = {LNCS}, publisher = {Springer Verlag}, url = {http://www.mrg.dist.unige.it/~sim/simo/Publications/Data/bmcsat.ps.gz} } @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{Hirsch2000b, 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{Hirsch2000c, 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", } @techreport{Hirsch2001a, author = "Hirsch, E. A. and Kojevnikov, A.", title = "{UnitWalk}: A new {SAT} solver that uses local search guided by unit clause elimination", institution = "Steklov Institute of Mathematics at St.Petersburg", year = "2001", type = "PDMI preprint", number = "9/2001", } @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} } @INPROCEEDINGS{Okushi2000a, Author = "Okushi, Fumiaki and Van Gelder, Allen", Title = "Persistent and Quasi-Persistent Lemmas in Propositional Model Elimination", BOOKTITLE = "(Electronic) Proc.\ 6th Int'l Symposium on Artificial Intelligence and Mathematics", NOTE = "To appear in special issue of {\it Annals of Math and AI}" (also at\newline url = {ftp://ftp.cse.ucsc.edu/pub/avg/Modoc/doc/persistent.ps.Z}, ANNOTE = "{\tt http://rutcor.rutgers.edu/\~{}amai}", YEAR = "2000" } @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{Prestwich2002a, author = {S. D. Prestwich}, title = {Randomised Backtracking for Linear Pseudo-Boolean Constraint Problems}, booktitle = {Proceedings of Fourth International Workshop on Integration of AI and OR techniques in Constraint Programming for Combinatorial Optimisation Problems}, year = 2002, url = {http://4c.ucc.ie/web/cpaior02.ps} } : in , . @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} } @Article{Shang1998a, author = {Y. Shang and B. W. Wah}, title = {A Discrete Lagrangian-Based Global-Search Method for Solving Satisfiability Problems}, journal = {Journal of Global Optimization}, year = 1998, volume = 12, number = 1, pages = {61--99}, month = {January}, publisher = {Kluwer Academic}, url = {http://manip.crhc.uiuc.edu/Wah/papers/Dirs/J60/J60.ps.gz} } @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}}, pages = {559--586}, crossref = {Johnson1996a}, url = {ftp://ftp.cse.ucsc.edu/pub/avg/kclose-tr.ps.gz}, annote = {Abstract: A new algorithm for testing satisfiability of propositional formulas in conjunctive normal form (CNF) is described. It applies reasoning in the form of certain resolution operations, and identification of equivalent literals. Resolution produces growth in the size of the formula, but within a global quadratic bound; most previous methods avoid operations that produce any growth, and generally do not identify equivalent literals. Computational experience so far suggests that the method does substantially less "guessing" than previously reported algorithms, while keeping a polynomial time bound on the work done between guesses. However, the time trade-off between reasoning and guessing is not yet clear. } } @INPROCEEDINGS{VanGelder2002a, Author = "Van Gelder, Allen", Title = "Extracting (Easily) Checkable Proofs from a Satisfiability Solver that Employs both Preorder and Postorder Resolution", BOOKTITLE = "Seventh Int'l Symposium on AI and Mathematics", ADDRESS = "Ft.\ Lauderdale, FL", PAGES = "", YEAR = 2002, url = {ftp://ftp.cse.ucsc.edu/pub/avg/CBJ/sat-pre-post.ps.gz} } @INPROCEEDINGS{VanGelder2002b, Author = "Van Gelder, Allen", Title = "Generalizations of Watched Literals for Backtracking Search", BOOKTITLE = "Seventh Int'l Symposium on AI and Mathematics", INSTITUTION = "Univ.\ Calif., Santa Cruz", ADDRESS = "Ft.\ Lauderdale, FL", PAGES = "", YEAR = 2002, url = {ftp://ftp.cse.ucsc.edu/pub/avg/CBJ/watched-lits.ps.gz} } @ARTICLE{VanGelder1999a, author = "Van Gelder, A.", title = "Autarky Pruning in Propositional Model Elimination Reduces Failure Redundancy", journal = "Journal of Automated Reasoning", year = "1999", volume = "23", number = "2", pages = "137--193", url = {ftp://ftp.cse.ucsc.edu/pub/avg/JAR/aut-jar-dist.ps.Z} } @ARTICLE{VanGelder1998a, author = "Van Gelder, A. and F. Okushi", title = "Lemma and Cut Strategies for Propositional Model Elimination", journal = "Annals of Mathematics and Artificial Intelligence", volume = "26", number = "1--4", pages = "113--132", url = {ftp://ftp.cse.ucsc.edu/pub/avg/AMAI/lemmas-dist.ps.Z}, year = 1999 } @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} } @Article{Warners2000a, author = {Joost Warners and Hans van Maaren}, title = {Solving satisfiability problems using elliptic approximations: effective branching rules}, journal = {Discrete Applied Mathematics}, year = 2000, volume = 107, pages = {241--259} } @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{placed here for cross referencing} @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} }