9. SAT 2006: Seattle, WA, USA

Armin Biere, Carla P. Gomes (Eds.): Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings. Lecture Notes in Computer Science 4121 Springer 2006, ISBN 3-540-37206-7 BibTeX

Invited Talks

Hossein M. Sheini, Karem A. Sakallah:
From Propositional Satisfiability to Satisfiability Modulo Theories. 1-9
Electronic Edition (link) BibTeX
Fahiem Bacchus:
CSPs: Adding Structure to SAT. 10-10
Electronic Edition (link) BibTeX

Proofs and Cores

Arist Kojevnikov, Alexander S. Kulikov:
Complexity of Semialgebraic Proofs with Restricted Degree of Falsity. 11-21
Electronic Edition (link) BibTeX
Oliver Kullmann, Inês Lynce, João Marques-Silva:
Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel. 22-35
Electronic Edition (link) BibTeX
Nachum Dershowitz, Ziyad Hanna, Alexander Nadel:
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. 36-41
Electronic Edition (link) BibTeX
Joshua Buresh-Oppenheim, David G. Mitchell:
Minimum Witnesses for Unsatisfiable 2CNFs. 42-47
Electronic Edition (link) BibTeX
Allen Van Gelder:
Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs. 48-53
Electronic Edition (link) BibTeX
Toni Jussila, Carsten Sinz, Armin Biere:
Extended Resolution Proofs for Symbolic SAT Solving with Quantification. 54-60
Electronic Edition (link) BibTeX

Heuristics and Algorithms

Mark Chavira, Adnan Darwiche:
Encoding CNFs to Empower Component Analysis. 61-74
Electronic Edition (link) BibTeX
Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke:
Satisfiability Checking of Non-clausal Formulas Using General Matings. 75-89
Electronic Edition (link) BibTeX
Eugene Goldberg:
Determinization of Resolution by an Algorithm Operating on Complete Assignments. 90-95
Electronic Edition (link) BibTeX
Hantao Zhang:
A Complete Random Jump Strategy with Guiding Paths. 96-101
Electronic Edition (link) BibTeX

Applications

Ilya Mironov, Lintao Zhang:
Applications of SAT Solvers to Cryptanalysis of Hash Functions. 102-115
Electronic Edition (link) BibTeX
Yuliya Zabiyaka, Adnan Darwiche:
Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies. 116-129
Electronic Edition (link) BibTeX
Roberto Sebastiani, Michele Vescovi:
Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC. 130-135
Electronic Edition (link) BibTeX
Inês Lynce, João Marques-Silva:
SAT in Bioinformatics: Making the Case with Haplotype Inference. 136-141
Electronic Edition (link) BibTeX

SMT

Yinlei Yu, Sharad Malik:
Lemma Learning in SMT on Linear Constraints. 142-155
Electronic Edition (link) BibTeX
Robert Nieuwenhuis, Albert Oliveras:
On SAT Modulo Theories and Optimization Problems. 156-169
Electronic Edition (link) BibTeX
Scott Cotton, Oded Maler:
Fast and Flexible Difference Constraint Propagation for DPLL(T). 170-183
Electronic Edition (link) BibTeX
Hossein M. Sheini, Karem A. Sakallah:
A Progressive Simplifier for Satisfiability Modulo Theories. 184-197
Electronic Edition (link) BibTeX

Structure

Uwe Bubeck, Hans Kleine Büning:
Dependency Quantified Horn Formulas: Models and Complexity. 198-211
Electronic Edition (link) BibTeX
Stefan Porschen, Ewald Speckenmeyer, Bert Randerath:
On Linear CNF Formulas. 212-225
Electronic Edition (link) BibTeX
Su Chen, Tomasz Imielinski, Karin Johnsgard, Donald Smith, Mario Szegedy:
A Dichotomy Theorem for Typed Constraint Satisfaction Problems. 226-239
Electronic Edition (link) BibTeX

MAX-SAT

Maria Luisa Bonet, Jordi Levy, Felip Manyà:
A Complete Calculus for Max-SAT. 240-251
Electronic Edition (link) BibTeX
Zhaohui Fu, Sharad Malik:
On Solving the Partial MAX-SAT Problem. 252-265
Electronic Edition (link) BibTeX
Evgeny Dantsin, Alexander Wolpert:
MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in O(s²) Time. 266-276
Electronic Edition (link) BibTeX
Osamu Watanabe, Masaki Yamamoto:
Average-Case Analysis for the MAX-2SAT Problem. 277-282
Electronic Edition (link) BibTeX

Local Search and Survey Propagation

Steven David Prestwich, Inês Lynce:
Local Search for Unsatisfiability. 283-296
Electronic Edition (link) BibTeX
Andrei A. Bulatov, Evgeny S. Skvortsov:
Efficiency of Local Search. 297-310
Electronic Edition (link) BibTeX
Panagiotis Manolios, Yimin Zhang:
Implementing Survey Propagation on Graphics Processing Units. 311-324
Electronic Edition (link) BibTeX
Eric I. Hsu, Sheila A. McIlraith:
Characterizing Propagation Methods for Boolean Satisfiability. 325-338
Electronic Edition (link) BibTeX

QBF

Hans Kleine Büning, Xishun Zhao:
Minimal False Quantified Boolean Formulas. 339-352
Electronic Edition (link) BibTeX
Horst Samulowitz, Fahiem Bacchus:
Binary Clause Reasoning in QBF. 353-367
Electronic Edition (link) BibTeX
Daijue Tang, Sharad Malik:
Solving Quantified Boolean Formulas with Circuit Observability Don't Cares. 368-381
Electronic Edition (link) BibTeX
Ashish Sabharwal, Carlos Ansótegui, Carla P. Gomes, Justin W. Hart, Bart Selman:
QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency. 382-395
Electronic Edition (link) BibTeX

Counting and Concurrency

Naomi Nishimura, Prabhakar Ragde, Stefan Szeider:
Solving #SAT Using Vertex Covers. 396-409
Electronic Edition (link) BibTeX
António Morgado, Paulo J. Matos, Vasco M. Manquinho, João P. Marques Silva:
Counting Models in Integer Domains. 410-423
Electronic Edition (link) BibTeX
Marc Thurley:
sharpSAT - Counting Models with Advanced Component Caching and Implicit BCP. 424-429
Electronic Edition (link) BibTeX
Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä:
A Distribution Method for Solving SAT in Grids. 430-435
Electronic Edition (link) BibTeX