Lecture Notes in Computer Science 3569 CommencedPublicationin1973 FoundingandFormerSeriesEditors: GerhardGoos,JurisHartmanis,andJanvanLeeuwen EditorialBoard DavidHutchison LancasterUniversity,UK TakeoKanade CarnegieMellonUniversity,Pittsburgh,PA,USA JosefKittler UniversityofSurrey,Guildford,UK JonM.Kleinberg CornellUniversity,Ithaca,NY,USA FriedemannMattern ETHZurich,Switzerland JohnC.Mitchell StanfordUniversity,CA,USA MoniNaor WeizmannInstituteofScience,Rehovot,Israel OscarNierstrasz UniversityofBern,Switzerland C.PanduRangan IndianInstituteofTechnology,Madras,India BernhardSteffen UniversityofDortmund,Germany MadhuSudan MassachusettsInstituteofTechnology,MA,USA DemetriTerzopoulos NewYorkUniversity,NY,USA DougTygar UniversityofCalifornia,Berkeley,CA,USA MosheY.Vardi RiceUniversity,Houston,TX,USA GerhardWeikum Max-PlanckInstituteofComputerScience,Saarbruecken,Germany Fahiem Bacchus Toby Walsh (Eds.) Theory andApplications of Satisfiability Testing 8th International Conference, SAT 2005 St Andrews, UK, June 19-23, 2005 Proceedings 1 3 VolumeEditors FahiemBacchus UniversityofToronto,DepartmentofComputerScience 6King’sCollegeRoad,Toronto,Ontario,M5S3H5,Canada E-mail:[email protected] TobyWalsh NationalICTAustraliaandUniversityofNewSouthWales SchoolofComputerScienceandEngineering Sydney2502,Australia E-mail:[email protected] LibraryofCongressControlNumber:2005927321 CRSubjectClassification(1998):F.4.1,I.2.3,I.2.8,I.2,F.2.2,G.1.6 ISSN 0302-9743 ISBN-10 3-540-26276-8SpringerBerlinHeidelbergNewYork ISBN-13 978-3-540-26276-3SpringerBerlinHeidelbergNewYork Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. SpringerisapartofSpringerScience+BusinessMedia springeronline.com ©Springer-VerlagBerlinHeidelberg2005 PrintedinGermany Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SPIN:11499107 06/3142 543210 Preface The 8th International Conference on Theory and Applications of Satisfiability Testing(SAT2005)providedaninternationalforumforthemostrecentresearch on the satisfiablity problem (SAT). SAT is the classic problem of determining whether or not a propositional formula has a satisfying truth assignment. It was the first problem shown by Cook to be NP-complete. Despite its seemingly specialized nature, satisfiability testing has proved to extremely useful in a wide range of different disciplines, both from a practical as well as from a theoretical point of view. For example, work on SAT continues to provide insight into various fundamental problems in computation, and SAT solving technology has advanced to the point where it has become the most effective way of solving a number of practical problems. The SAT series of conferences are multidisciplinary conferences intended to bring together researchers from various disciplines who are interested in SAT. Topics of interest include, but are not limited to: proof systems and proof com- plexity;searchalgorithmsandheuristics;analysisofalgorithms;theoriesbeyond the propositional; hard instances and random formulae; problem encodings; in- dustrial applications; solvers and other tools. ThisvolumecontainsthepapersacceptedforpresentationatSAT2005.The conference attracted a record number of 73 submissions. Of these, 26 papers were accepted for presentation in the technical programme. In addition, 16 pa- pers were accepted as shorter papers and were presented as posters during the technicalprogramme.Theacceptedpapersandposterpaperscoverthefullrange of topics listed in the call for papers. We would like to thank a number of people and organizations: Ian Miguel, the Local Chair who helped us organize the conference remotely; our generous sponsors who helped us to keep costs down, especially for students; Daniel Le BerreandLaurentSimonforonceagainorganizingtheSATSolverCompetition; andMassimoNarizzanoandArmandoTacchellafortheQBFSolverEvaluation. WewouldalsoliketothankthemembersoftheProgrammeCommitteeandthe additional referees who contributed in the paper-reviewing process. St Andrews Fahiem Bacchus, Toby Walsh June 2005 Organization Conference Organization Conference Chairs:Fahiem Bacchus (University of Toronto, Canada) Toby Walsh (National ICT Australia and University of NSW, Australia) Local Chair: Ian Miguel (University of St Andrews, UK) Programme Committee Dimitris Achlioptas Ziyad Hanna Steve Prestwich Fadi Aloul Edward Hirsch Jussi Rintanen Clark Barrett Henry Kautz Lakhdar Sais Constantinos Bartzis Eleftherios Kirousis Karem Sakallah Paul Beame Hans Kleine Bu¨ning Laurent Simon Armin Biere Daniel Le Berre Stefan Szeider Ronen Brafman Chu-Min Li Mirek Truszczynski Alessandro Cimatti Fangzhen Lin Allen Van Gelder Adnan Darwiche Sharad Malik Hans van Maaren Alvaro del Val Jo˜ao Marques-Silva Lintao Zhang Enrico Giunchiglia Ilkka Niemela Eugene Goldberg Toniann Pitassi Sponsors Cadence Design Systems Intel Corporation Intelligence Information Systems Institute, Cornell Microsoft Research CoLogNet Network of Excellence Additional Referees Zaher S. Andraus Sylvie Coste-Marquis Gilles Dequen Pierre Bonami Nadia Creignou Laure Devendeville Uwe Bubeck Stefan Dantchev Niklas Een Yin Chen Sylvain Darras Malay K. Ganai VIII Organization Aarti Gupta Alexander Kulikov Massimo Narizzano Jean-Luc Guerin Oliver Kullman Sergey Nikolenko Keijo Heljanko Theodor Lettmann Nishant Ninha Jinbo Huang Lengning Liu Thomas Schiex Dmitry Itsyson Ines Lynce Armando Tacchella Matti Ja¨rvisalo Yogesh Mahajan Muralidhar Talupur Tommi Junttila Marco Maratea Daijue Tang Bernard Jurkowiak Victor Marek Yinlei Yu Zurab Khasidashvili Bertrand Mazure Arist Kojevnikov Maher N. Mneimneh Ioannis Koutis Alexander Nadel Table of Contents Preface Solving Over-Constrained Problems with SAT Technology Josep Argelich, Felip Manya`..................................... 1 A Symbolic Search Based Approach for Quantified Boolean Formulas Gilles Audemard, Lakhdar Sa¨ıs .................................. 16 Substitutional Definition of Satisfiability in Classical Propositional Logic Anton Belov, Zbigniew Stachniak ................................ 31 A Clause-Based Heuristic for SAT Solvers Nachum Dershowitz, Ziyad Hanna, Alexander Nadel ............... 46 Effective Preprocessing in SAT Through Variable and Clause Elimination Niklas E´en, Armin Biere........................................ 61 Resolution and Pebbling Games Nicola Galesi, Neil Thapen...................................... 76 Local and Global Complete Solution Learning Methods for QBF Ian P. Gent, Andrew G.D. Rowley ............................... 91 Equivalence Checking of Circuits with Parameterized Specifications Eugene Goldberg ............................................... 107 Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming Marijn Heule, Hans van Maaren ................................. 122 Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution Edward A. Hirsch, Sergey I. Nikolenko ........................... 135 Resolution Tunnels for Improved SAT Solver Performance Michal Kouril, John Franco ..................................... 143 Diversification and Determinism in Local Search for Satisfiability Chu Min Li, Wen Qi Huang .................................... 158 X Table of contents On Finding All Minimally Unsatisfiable Subformulas Mark H. Liffiton, Karem A. Sakallah ............................. 173 Optimizations for Compiling Declarative Models into Boolean Formulas Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, Lintao Zhang, Martin Rinard................................................. 187 Random Walk with Continuously Smoothed Variable Weights Steven Prestwich............................................... 203 Derandomization of PPSZ for Unique-k-SAT Daniel Rolf ................................................... 216 Heuristics for Fast Exact Model Counting Tian Sang, Paul Beame, Henry Kautz ............................ 226 A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic Hossein M. Sheini, Karem A. Sakallah ........................... 241 DPvis - A Tool to Visualize the Structure of SAT Instances Carsten Sinz, Edda-Maria Dieringer ............................. 257 Constraint Metrics for Local Search Finnegan Southey .............................................. 269 Input Distance and Lower Bounds for Propositional Resolution Proof Length Allen Van Gelder .............................................. 282 Sums of Squares, Satisfiability and Maximum Satisfiability Hans van Maaren, Linda van Norden............................. 294 Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable Magnus Wahlstro¨m ............................................ 309 A New Approach to Model Counting Wei Wei, Bart Selman ......................................... 324 Benchmarking SAT Solvers for Bounded Model Checking Emmanuel Zarpas ............................................. 340 Model-Equivalent Reductions Xishun Zhao, Hans Kleine Bu¨ning ............................... 355 Table of Contents XI Improved Exact Solvers for Weighted Max-SAT Teresa Alsinet, Felip Manya`, Jordi Planes ........................ 371 Quantifier Trees for QBFs Marco Benedetti ............................................... 378 Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas Uwe Bubeck, Hans Kleine Bu¨ning, Xishun Zhao ................... 386 A Branching Heuristics for Quantified Renamable Horn Formulas Sylvie Coste-Marquis, Daniel Le Berre, Florian Letombe ............ 393 An Improved Upper Bound for SAT Evgeny Dantsin, Alexander Wolpert .............................. 400 Bounded Model Checking with QBF Nachum Dershowitz, Ziyad Hanna, Jacob Katz .................... 408 Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies Vijay Durairaj, Priyank Kalla ................................... 415 Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas Roman Gershman, Ofer Strichman............................... 423 Automated Generation of Simplification Rules for SAT and MAXSAT Alexander S. Kulikov ........................................... 430 Speedup Techniques Utilized in Modern SAT Solvers Matthew D.T. Lewis, Tobias Schubert, Bernd W. Becker ............ 437 FPGA Logic Synthesis Using Quantified Boolean Satisfiability Andrew Ling, Deshanand P. Singh, Stephen D. Brown .............. 444 On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization Vasco Manquinho, Jo˜ao Marques-Silva............................ 451 A New Set of Algebraic Benchmark Problems for SAT Solvers Andreas Meier, Volker Sorge .................................... 459 A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas Maher Mneimneh, Inˆes Lynce, Zaher Andraus, Jo˜ao Marques-Silva, Karem Sakallah................................................ 467