Theory and Applications of Satisfiability Testing - SAT 2009: 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings

Front Matter....Pages -
SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms....Pages 1-1
Symbolic Techniques in Propositional Satisfiability Solving....Pages 2-3
Efficiently Calculating Evolutionary Tree Measures Using SAT....Pages 4-17
Finding Lean Induced Cycles in Binary Hypercubes....Pages 18-31
Finding Efficient Circuits Using SAT-Solvers....Pages 32-44
Encoding Treewidth into SAT....Pages 45-50
The Complexity of Reasoning for Fragments of Default Logic....Pages 51-64
Does Advice Help to Prove Propositional Tautologies?....Pages 65-72
Backdoors in the Context of Learning....Pages 73-79
Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences....Pages 80-85
On Some Aspects of Mixed Horn Formulas....Pages 86-100
Variable Influences in Conjunctive Normal Forms....Pages 101-113
Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution....Pages 114-127
An Exponential Lower Bound for Width-Restricted Clause Learning....Pages 128-140
Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces....Pages 141-146
Boundary Points and Resolution....Pages 147-160
Sequential Encodings from Max-CSP into Partial Max-SAT....Pages 161-166
Cardinality Networks and Their Applications....Pages 167-180
New Encodings of Pseudo-Boolean Constraints into CNF....Pages 181-194
Efficient Term-ITE Conversion for Satisfiability Modulo Theories....Pages 195-208
On-the-Fly Clause Improvement....Pages 209-222
Dynamic Symmetry Breaking by Simulating Zykov Contraction....Pages 223-236
Minimizing Learned Clauses....Pages 237-243
Extending SAT Solvers to Cryptographic Problems....Pages 244-257
Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability....Pages 258-264
A Theoretical Analysis of Search in GSAT....Pages 265-275
The Parameterized Complexity of k -Flip Local Search for SAT and MAX SAT....Pages 276-283
A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem....Pages 284-297
Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques....Pages 298-311
Restart Strategy Selection Using Machine Learning Techniques....Pages 312-325
Instance-Based Selection of Policies for SAT Solvers....Pages 326-340
Width-Based Restart Policies for Clause-Learning Satisfiability Solvers....Pages 341-355
Problem-Sensitive Restart Heuristics for the DPLL Procedure....Pages 356-362
 (1,2)-QSAT : A Good Candidate for Understanding Phase Transitions Mechanisms....Pages 363-376
 VARSAT : Integrating Novel Probabilistic Inference Techniques with DPLL Search....Pages 377-390
Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits....Pages 391-397
A Compact Representation for Syntactic Dependencies in QBFs....Pages 398-411
Beyond CNF: A Circuit-Based QBF Solver....Pages 412-426
Solving (Weighted) Partial MaxSAT through Satisfiability Testing....Pages 427-440
Nonlinear Pseudo-Boolean Optimization: Relaxation or Propagation?....Pages 441-446
Relaxed DPLL Search for MaxSAT....Pages 447-452
Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates....Pages 453-466
Exploiting Cycle Structures in Max-SAT....Pages 467-480
Generalizing Core-Guided Max-SAT....Pages 481-494
Algorithms for Weighted Boolean Optimization....Pages 495-508
PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing....Pages 509-523
 c-sat : A Parallel SAT Solver for Clusters....Pages 524-537
Back Matter....Pages -