Updated 14 May 2002 (final)

SAT 2002

Fifth  International Symposium on the
Theory and Applications of Satisfiability Testing

May 6-9, 2002
Cincinnati, Ohio, USA

Keynote Speakers

Edmund Clarke, Computer Science, Carnegie Mellon University, USA,

SAT based Abstraction Refinement in Temporal Logic Model Checking
We describe new techniques for model checking in the counterexample guided abstraction / refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" counterexamples, i.e., traces that can not be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a SAT checker. We then use a combination of Integer Linear Programming (ILP) and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques. This is joint work with Anubhav Gupta, James Kukula, and Ofer Strichman.
Presentation (postscript)

João Marques-Silva, Instituto Superior Técnico, Universidade Técnica de Lisboa, Portugal

Hypothetical Reasoning in Propositional Satisfiability
In this talk we describe the utilization of hypothetical reasoning in Propositional Satisfiability (SAT). Hypothetical reasoning (HR) consists of formulating hypothetical scenarios regarding the propositional formula, and establishing consequences from those scenarios. Different utilizations of HR can be envisioned, including the identification of necessary assignments (i.e. backbones) and the inference of new clauses. HR can also be utilized as a complete SAT algorithm, that entails other well-known proof procedures for SAT. Moreover, we analyze preliminary experimental results of applying HR to real-world problem instances of SAT.
Presentation (powerpoint)

Uwe Schöning, Informatik, Universität Ulm, Germany,

New Worst Case Bounds on k-SAT
We consider a series of very similar (deterministic and probabilistic) algorithms based on a simple local search paradigm. These algorithms have the advantage that rigorous worst-case complexity analyses are possible. Indeed, these analyses lead to the best known upper bounds for the complexity of k-SAT, especially for 3-SAT. The latest version of a 3-SAT algorithm chooses the initial assignments which are the starting points for the random local search in a random way where the probability distribution depends on the input fomula.
Presentation (postscript)

Main Conference Speakers (no particular order)

Alan Frieze, Mathematical Sciences, Carnegie Mellon University, USA (with Nicolas Wormald),
    k-SAT: A tight threshold for moderately growing k   (1-6)

Fahiem Bacchus, Computer Science, University of Toronto, Canada
    Exploring the computational tradeoff of more reasoning and less searching   (7-16)

Nadia Creignou, LIF, Université de la Méditerranée, Marseille, France (with Hervé Daudé)
    Random generalized Satisfiability problems   (17-26)

Inna Davydova, Mathematics and Mechanics, St. Petersburg State University, Russia (with Gennady Davydov),
    CNF application in discrete optimization   (27-34)

Edward A. Hirsch, Russian Academy of Sciences, Steklov Institute of Mathematics at St. Petersburg, Russia (with Arist Kojevnikov),
    UnitWalk: A new SAT solver that uses local search guided by unit clause elimination   (35-42)

Allen Van Gelder, Computer Science, University of California at Santa Cruz, USA,
    Toward leaner binary-clause reasoning in a Satisfiability solver   (43-53)

Eugene Goldberg, Cadence Berkeley Labs, USA,
    Testing satisfiability of CNF formulas by computing a stable set of points   (54-69)   pdf version

Yoichi Takenaka, Computer Science, Osaka University, Japan (with Akihiro Hashimoto),
    An analog algorithm for the Satisfiability problem   (70-77)

Remi Monasson, CNRS-Laboratoire de Physique Théorique de l'ENS, France (with Simona Cocco),
    Restart method and exponential acceleration of random 3-SAT instances resolutions:
    a large deviation analysis of the Davis-Putnam-Loveland-Logemann algorithm   (78-88)

Stefan Woltran, Computer Science, Technische Universität, Austria (with Uwe Egly and Reinhard Pichler),
    On deciding subsumption problems   (89-97)   updated 28 March 02

Fadi A. Aloul, Electrical Engineering and Computer Science, University of Michigan, USA (with Brian Sierawski and Karem Sakallah),
    A tool for measuring progress of backtrack-search solvers   (98-105)

Andrea Roli, DEIS, Università degli Studi di Bologna, Italy,
    Impact of structure on parallel local search for SAT   (106-113)   updated 4 April 02

Daniele Pretolani, Matematica e Informatica, Università di Camerino, Italy,
    Probabilistic logic: the PSAT and CPA models   (114-121)

Lyndon Drake, Computer Science, University of York, United Kingdom (with Alan Frisch and Toby Walsh),
    Adding resolution to the DPLL procedure for Satisfiability   (122-129)

Olivier Dubois, LIP6, CNRS, Université Paris 6, France (with Gilles Dequen),
    Renormalization as a function of clause lengths for solving random k-SAT formulae   (130-132)

Ian Gent, Computer Science, University of St. Andrews, Scotland (with Patrick Prosser),
    SAT encodings of the stable marriage problem with ties and incomplete lists   (133-140)

Holger Hoos, Computer Science, University of British Columbia, Canada,
    SLS algorithms for SAT: irregular instances, search stagnation, and mixture models   (141-148)

Chu Min Li, LaRIA, University of Picardie Jules Verne, France (with Bernard Jurkowiak and Paul Walton Purdom),
    Integrating symmetry breaking into a DLL procedure   (149-155)

Felip Manya, Departament d'Informatica i E. Industrial, Universitat de Lleida, Spain (with Carlos Ansótegui, Ramón Béjar, Alba Cabiscol, and Chu Min Li),
    Resolution methods for many-valued CNF formulas   (156-163)   updated 21 April 02

Hans Kleine Büning, Informatik, Universität Paderborn, Germany (with Daoyun Xu),
    The complexity of homomorphisms and renamings of minimal unsatisfiable formulas   (164-181)

Akihiro Matsuura, Informatics, Kyoto University, Japan (with Kazuo Iwama),
    Inclusion-exclusion for k-CNF formulas   (182-189)   updated 5 April 02

Oliver Kullmann, Computer Science, University of Wales Swansea, United Kingdom,
    Towards an adaptive density based branching rule for SAT solvers, using a database for
    mixed random conjunctive normal forms built upon the Advanced Encryption Standard (AES)   (190-200)

Chu Min Li, LaRIA, University of Picardie Jules Verne, France (with Hachemi Bennaceur),

An empirical measure for characterizing 3-SAT   (201-205)

DoRon Motter, Electrical Engineering and Computer Science, University of Michigan, USA (with Igor Markov),
    On proof systems behind efficient SAT solvers   (206-213)   updated 19 April 02

João Marques-Silva, Instituto Superior Técnico, Universidade Técnica de Lisboa, Portugal (with Inês Lynce),
    Complete unrestricted backtracking algorithms for Satisfiability   (214-221)

Oded Maler, Verimag, France (with Moez Mahfoudh, Peter Niebert, and Eugene Asarin),
    A Satisfiability checker for difference logic   (222-230)

Stefan Porschen, Institut für Informatik, Universität zu Köln, Germany (with Bert Randerath and Ewald Speckenmeyer),
    X3SAT is decidable in time O(2n/5)   (231-235)

Sean Forman, Computer Science, St. Joseph's University, USA (with Alberto M. Segre),
    NAGSAT: A randomized, complete, parallel solver for 3-SAT   (236-243)

Leonardo de Moura, Computer Science Lab, SRI International, USA (with Harald Ruess),
    Lemmas on demand for Satisfiability solvers   (244-251)

Steven Prestwich, Cork Constraint Computation Center, Ireland (with Stéphane Bressan),
    A SAT approach to query optimization in mediator systems   (252-259)

Xishun Zhao, Institute of Logic and Cognition, Zhongshan University, P.R. China (with Hans Kleine Büning),
    Extension and equivalence problems for clause minimal formulas   (260-272)

John Slaney, Computer Science, Australian National University, Australia (with Toby Walsh),
    Phase transition behavior: from decision to optimization   (273-280)

Hantao Zhang, Computer Science, University of Iowa, USA,
    Generating college conference basketball schedules by a SAT solver   (281-291)

Stefan Szeider, Institute of Discrete Mathematics, Austrian Academy of Sciences, Austria,
    Generalizations of matched CNF formulas   (292-307)

Inês Lynce, Information Systems and Computer Science, Technical University of Lisbon, Portugal (with João Marques-Silva),
    Efficient data structures for backtrack search SAT solvers   (308-315)

Zbigniew Stachniak, Computer Science, York University, Canada,
    Going non-clausal   (316-322, revised 22 March, 2002)

Gábor Kusper, Research Institute for Symbolic Computation, Linz, Austria,
    Solving the resolution-free SAT problem by hyper-unit propagation in linear time   (323-332)

Renato Bruni, Dipartimento di Informatica e Sistemistica, Università di Roma "La Sapienza", Italy,
    Exact selection of minimal unsatisfiable subformulae for special classes of propositional formulae   (333-337)

Fadi A. Aloul, Electrical Engineering and Computer Science, University of Michigan, USA (with Arathi Ramani, Igor Markov, and Karem Sakallah),
    Solving difficult SAT instances in the presence of symmetry   (338-345)

Fadi A. Aloul, Electrical Engineering and Computer Science, University of Michigan, USA (with Arathi Ramani, Igor Markov, and Karem Sakallah),
    PBS: a backtrack-search psuedo-boolean solver and optimizer   (346-353)

Franc Brglez, Computer Science, North Carolina State University, USA (with Xiao Yu Li and Matthias F. Stallmann),
    The role of a skeptic agent in testing and benchmarking of SAT algorithms   (354-361) updated 5 May

Alexis C. Kaporis, University of Patras, Greece (with Lefteris M. Kirousis and Efthimios G. Lalas),
    The probabilistic analysis of a greedy satisfiability algorithm   (362-376)   updated 25 April 02


QBF Mini-Workshop Speakers (speaking order)

Dan Pehoushek
   Introduction to Q space  (1-16)

Andrew G.D. Rowley, St. Andrews University, Scotland (with Ian Gent)
   Solving 2-CNF quantified boolean formulae using variable assignment and propagation   (17-25)

Anja Remshagen, State University of West Georgia, USA (with Klaus Truemper)
   Algorithms for logic-based abduction   (26-31)

Subramanyan Siva, U. Cincinnati, USA (with R. Vemuri, W.M. Vanfleet, J. Schlipf and J. Franco
   Reconfigurable interconnect synthesis via quantified Boolean satisfiability   (32-40)

Enrico Giunchiglia, Università di Genova, Italia (with Massimo Narizzano and Armando Tacchella)
   Assessing the impact of learning techniques in quantified Boolean logic satisfiability   (41-47)

Stefan Woltran, Technische Universität, Austria (with H. Tompits and Uwe Egly)
   On quantifier shifting for quantified Boolean formulas   (48-61)

Hans Kleine Büning, Universität Paderborn (with Xishun Zhao)
   Minimal falsity for QBF with deficiency 1   (62-69)


SAT Solver Speakers (Short explanations of some solvers)

        Speaking Author                                                 Solver Name                                        
Oliver Kullmannoksolver
Allen Van Geldermodoc
Allen Van Gelderrb2cl
John Kolenpartsat
Richard Ostrowskilsat (with Bertrand Mazure, Lakhdar Sais)
(presented by Daniel Le Berre)
Marijn Heulemarch (with Hans van Maaren, Mark Dufour, Joris van Zwieten)
Eugene Goldbergberkmin (with Yakov Novikov)
Armando Tacchellasimo (with Enrico Giunchiglia, Massimo Maratea)
João Marques-Silvajquest (with Inês Lynce)