Image of Swansea Bay and
    University

SAT 2009 - Twelfth International Conference on
Theory and Applications of Satisfiability Testing

June 30 - July 3, 2009, Swansea, Wales, United Kingdom


Accepted papers SAT 2009

Roberto Asín Achá, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez Carbonell. Cardinality Networks and their Applications
Carlos Ansótegui, María Luisa Bonet and Jordi Levy. A Weighted Partial MaxSAT Solver Based on Satisfiability Testing
Josep Argelich, Alba Cabiscol, Inês Lynce and Felip Manyà. Sequential Encodings from Max-CSP into Partial Max-SAT
Albert Atserias, Johannes Fichte and Marc Thurley. Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
Olivier Bailleux, Yacine Boufkhad and Olivier Roussel. New Encodings of Pseudo-Boolean Constraints into CNF
Adrian Balint, Michael Henn and Oliver Gableske. A novel approach to combine a SLS- and a DPLL-solver for the satisfiability problem
Timo Berthold, Stefan Heinz and Marc E. Pfetsch. Nonlinear Pseudo-Boolean Optimization: Relaxation or Propagation?
Olaf Beyersdorff, Arne Meier, Michael Thomas and Heribert Vollmer. The Complexity of Reasoning for Fragments of Default Logic
Olaf Beyersdorff and Sebastian Müller. Does Advice Help to Prove Propositional Tautologies?
Maria Luísa Bonet and Katherine St. John. Efficiently Calculating Tree Measures Using SAT
Yury Chebiryak, Thomas Wahl, Daniel Kröning and Leopold Haller. Finding Lean Induced Cycles in Binary Hypercubes
Jingchao Chen. Building a Hybrid SAT Solver via Conflict-driven, Look-ahead and XOR Reasoning Techniques
Nadia Creignou, Hervé Daudé, Uwe Egly and Raphaël Rossignol. (1,2)-QSAT: a good candidate for understanding phase transition mechanisms
Eugene Goldberg. Boundary Points and Resolution
Bistra Dilkina, Carla Gomes and Ashish Sabharwal. Backdoors in the Context of Learning
Alexandra Goultiaeva, Vicki Iverson and Fahiem Bacchus. Beyond CNF: a Circuit-Based QBF Solver
Shai Haim and Toby Walsh. Restart Strategy Selection using Machine Learning Techniques
Hyojung Han and Fabio Somenzi. On-The-Fly Clause Improvement
Eric Hsu and Sheila McIlraith. VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search
Daniel Johannsen, Igor Razgon and Magnus Wahlström. Solving SAT for CNF formulas with a one-sided variable occurrence restriction
Jan Johannsen. An exponential lower bound for width-restricted clause learning
Hyondeuk Kim, Fabio Somenzi and HoonSang Jin. Efficient Term-ITE Conversion for Satisfiability Modulo Theories
Hans Kleine Büning, Xishun Zhao and Uwe Bubeck. Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
Arist Kojevnikov, Alexander Kulikov and Grigory Yaroslavtsev. Finding Efficient Circuits Using SAT-solvers
Lukas Kroc, Ashish Sabharwal and Bart Selman. Relaxed DPLL Search for MaxSAT
Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez Carbonell. Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker and Enrico Giunchiglia. PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing
Chu Min Li, Felip Manyà, Nouredine Ould Mohamedou and Jordi Planes. Exploiting Cycle Structures in Max-SAT
Mark Liffiton and Karem Sakallah. Generalizing Core-Guided Max-SAT
Florian Lonsing and Armin Biere. A Compact Representation for Syntactic Dependencies in QBFs
Vasco Manquinho, Joao Marques-Silva and Jordi Planes. Algorithms for Weighted Boolean Optimization
Mladen Nikolić, Filip Marić and Predrag Janičić. Instance-Based Selection of Policies for SAT Solvers
Kei Ohmura and Kazunori Ueda. c-sat: A Parallel SAT Solver for Clusters
Knot Pipatsrisawat and Adnan Darwiche. Width-Based Restart Policies for Clause-Learning Satisfiability Solvers
Stefan Porschen, Tatjana Schmidt and Ewald Speckenmeyer. On Some Aspects of Mixed Horn Formulas
Marko Samer and Helmut Veith. Encoding Treewidth into SAT
Bas Schaafsma, Marijn Heule and Hans van Maaren. Dynamic Symmetry Breaking by Simulating Zykov Contraction
Carsten Sinz and Markus Iser. Problem-Sensitive Restart Heuristics for the DPLL Procedure
Evgeny Skvortsov. A Theoretical Analysis of Search in GSAT
Niklas Sörensson and Armin Biere. Minimizing Learned Clauses
Mate Soos, Karsten Nohl and Claude Castelluccia. Extending SAT solvers to cryptographic problems
Zbigniew Stachniak and Anton Belov. Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability
Stefan Szeider. The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT
Patrick Traxler. Variable Influences in Conjunctive Normal Forms
Allen Van Gelder. Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces

Invited presentations


Valid XHTML 1.0 Strict Valid CSS level 2.1 Last modified: Thu Oct 1 18:24:25 BST 2009