default search action
12th SAT 2009: Swansea, UK
- Oliver Kullmann:
Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings. Lecture Notes in Computer Science 5584, Springer 2009, ISBN 978-3-642-02776-5
Invited Talks
- Robert Nieuwenhuis:
SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. 1 - Moshe Y. Vardi:
Symbolic Techniques in Propositional Satisfiability Solving. 2-3
Applications of SAT
- Maria Luisa Bonet
, Katherine St. John:
Efficiently Calculating Evolutionary Tree Measures Using SAT. 4-17 - Yury Chebiryak, Thomas Wahl, Daniel Kroening
Finding Lean Induced Cycles in Binary Hypercubes. 18-31 - Arist Kojevnikov, Alexander S. Kulikov
Finding Efficient Circuits Using SAT-Solvers. 32-44 - Marko Samer, Helmut Veith:
Encoding Treewidth into SAT. 45-50
Complexity Theory
- Olaf Beyersdorff
The Complexity of Reasoning for Fragments of Default Logic. 51-64 - Olaf Beyersdorff
Does Advice Help to Prove Propositional Tautologies? 65-72
Structures for SAT
- Bistra Dilkina
Backdoors in the Context of Learning. 73-79 - Daniel Johannsen, Igor Razgon, Magnus Wahlström:
Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences. 80-85 - Stefan Porschen, Tatjana Schmidt, Ewald Speckenmeyer:
On Some Aspects of Mixed Horn Formulas. 86-100 - Patrick Traxler:
Variable Influences in Conjunctive Normal Forms. 101-113
Resolution and SAT
- Albert Atserias, Johannes Klaus Fichte, Marc Thurley:
Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution. 114-127 - Jan Johannsen:
An Exponential Lower Bound for Width-Restricted Clause Learning. 128-140 - Allen Van Gelder:
Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces. 141-146 - Eugene Goldberg:
Boundary Points and Resolution. 147-160
Translations to CNF
- Josep Argelich
Sequential Encodings from Max-CSP into Partial Max-SAT. 161-166 - Roberto Asín
Cardinality Networks and Their Applications. 167-180 - Olivier Bailleux, Yacine Boufkhad, Olivier Roussel:
New Encodings of Pseudo-Boolean Constraints into CNF. 181-194 - Hyondeuk Kim, Fabio Somenzi, HoonSang Jin:
Efficient Term-ITE Conversion for Satisfiability Modulo Theories. 195-208
Techniques for Conflict-Driven SAT Solvers
- HyoJung Han, Fabio Somenzi:
On-the-Fly Clause Improvement. 209-222 - Bas Schaafsma, Marijn Heule, Hans van Maaren:
Dynamic Symmetry Breaking by Simulating Zykov Contraction. 223-236 - Niklas Sörensson, Armin Biere
Minimizing Learned Clauses. 237-243 - Mate Soos, Karsten Nohl, Claude Castelluccia:
Extending SAT Solvers to Cryptographic Problems. 244-257
Solving SAT by Local Search
- Anton Belov, Zbigniew Stachniak:
Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability. 258-264 - Evgeny S. Skvortsov:
A Theoretical Analysis of Search in GSAT. 265-275 - Stefan Szeider
The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT. 276-283
Hybrid SAT Solvers
- Adrian Balint, Michael Henn, Oliver Gableske:
A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem. 284-297 - Jingchao Chen:
Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques. 298-311
Automatic Adaption of SAT Solvers
- Shai Haim, Toby Walsh:
Restart Strategy Selection Using Machine Learning Techniques. 312-325 - Mladen Nikolic, Filip Maric, Predrag Janicic
Instance-Based Selection of Policies for SAT Solvers. 326-340 - Knot Pipatsrisawat, Adnan Darwiche:
Width-Based Restart Policies for Clause-Learning Satisfiability Solvers. 341-355 - Carsten Sinz, Markus Iser:
Problem-Sensitive Restart Heuristics for the DPLL Procedure. 356-362
Stochastic Approaches to SAT Solving
- Nadia Creignou, Hervé Daudé, Uwe Egly, Raphaël Rossignol:
(1, 2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms. 363-376 - Eric I. Hsu, Sheila A. McIlraith:
VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search. 377-390
QBFs and Their Representations
- Hans Kleine Büning, Xishun Zhao, Uwe Bubeck:
Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits. 391-397 - Florian Lonsing
A Compact Representation for Syntactic Dependencies in QBFs. 398-411 - Alexandra Goultiaeva, Vicki Iverson, Fahiem Bacchus:
Beyond CNF: A Circuit-Based QBF Solver. 412-426
Optimisation Algorithms
- Carlos Ansótegui
Solving (Weighted) Partial MaxSAT through Satisfiability Testing. 427-440 - Timo Berthold, Stefan Heinz, Marc E. Pfetsch
Nonlinear Pseudo-Boolean Optimization: Relaxation or Propagation?. 441-446 - Lukas Kroc, Ashish Sabharwal, Bart Selman:
Relaxed DPLL Search for MaxSAT. 447-452 - Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras
Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. 453-466 - Chu Min Li, Felip Manyà
Exploiting Cycle Structures in Max-SAT. 467-480 - Mark H. Liffiton, Karem A. Sakallah:
Generalizing Core-Guided Max-SAT. 481-494 - Vasco Manquinho
Algorithms for Weighted Boolean Optimization. 495-508
Distributed and Parallel Solving
- Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano
PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing. 509-523 - Kei Ohmura, Kazunori Ueda:
c-sat: A Parallel SAT Solver for Clusters. 524-537
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-25 22:31 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: