Ebook: Theory and Applications of Satisfiability Testing – SAT 2012: 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings

This book constitutes the refereed proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT 2012, held in Trento, Italy, in June 2012. The 29 revised full papers, 7 tool papers, and 16 poster papers presented together with 2 invited talks were carefully reviewed and selected from 112 submissions (88 full, 10 tool and 14 poster papers). The papers are organized in topical sections on stochastic local search, theory, quantified Boolean formulae, applications, parallel and portfolio approaches, CDCL SAT solving, MAX-SAT, cores interpolants, complexity analysis, and circuits and encodings.

---

This book constitutes the refereed proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT 2012, held in Trento, Italy, in June 2012. The 29 revised full papers, 7 tool papers, and 16 poster papers presented together with 2 invited talks were carefully reviewed and selected from 112 submissions (88 full, 10 tool and 14 poster papers). The papers are organized in topical sections on stochastic local search, theory, quantified Boolean formulae, applications, parallel and portfolio approaches, CDCL SAT solving, MAX-SAT, cores interpolants, complexity analysis, and circuits and encodings.

---

This book constitutes the refereed proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT 2012, held in Trento, Italy, in June 2012. The 29 revised full papers, 7 tool papers, and 16 poster papers presented together with 2 invited talks were carefully reviewed and selected from 112 submissions (88 full, 10 tool and 14 poster papers). The papers are organized in topical sections on stochastic local search, theory, quantified Boolean formulae, applications, parallel and portfolio approaches, CDCL SAT solving, MAX-SAT, cores interpolants, complexity analysis, and circuits and encodings.
Content:
Front Matter....Pages -
Understanding IC3....Pages 1-14
Satisfiability and The Art of Computer Programming....Pages 15-15
Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break....Pages 16-29
Off the Trail: Re-examining the CDCL Algorithm....Pages 30-43
An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning....Pages 44-57
Computing Resolution-Path Dependencies in Linear Time ,....Pages 58-71
Strong Backdoors to Nested Satisfiability....Pages 72-85
Extended Failed-Literal Preprocessing for Quantified Boolean Formulas....Pages 86-99
On Sequent Systems and Resolution for QBFs....Pages 100-113
Solving QBF with Counterexample Guided Refinement....Pages 114-128
Henkin Quantifiers and Boolean Formulae....Pages 129-142
Lynx: A Programmatic SAT Solver for the RNA-Folding Problem....Pages 143-156
Generalized Property Directed Reachability....Pages 157-171
SMT-Aided Combinatorial Materials Discovery....Pages 172-185
Faulty Interaction Identification via Constraint Solving and Optimization....Pages 186-199
Revisiting Clause Exchange in Parallel SAT Solving....Pages 200-213
Designing Scalable Parallel SAT Solvers....Pages 214-227
Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors....Pages 228-241
Efficient SAT Solving under Assumptions....Pages 242-255
Preprocessing in Incremental SAT....Pages 256-269
On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets....Pages 270-283
Improvements to Core-Guided Binary Search for MaxSAT....Pages 284-297
On Efficient Computation of Variable MUSes....Pages 298-311
Interpolant Strength Revisited....Pages 312-326
Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas....Pages 327-340
Parameterized Complexity of Weighted Satisfiability Problems....Pages 341-354
Fixed-Parameter Tractability of Satisfying beyond the Number of Variables....Pages 355-368
Finding Efficient Circuits for Ensemble Computation....Pages 369-382
Conflict-Driven XOR-Clause Learning....Pages 383-396
Perfect Hashing and CNF Encodings of Cardinality Constraints....Pages 397-409
The Community Structure of SAT Formulas....Pages 410-423
Resolution-Based Certificate Extraction for QBF....Pages 424-429
Coprocessor 2.0 – A Flexible CNF Simplifier....Pages 430-435
SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox....Pages 436-441
CoPAn: Exploring Recurring Patterns in Conflict Analysis of CDCL SAT Solvers....Pages 442-448
Azucar: A SAT-Based CSP Solver Using Compact Order Encoding....Pages 449-455
SatX10: A Scalable Plug&Play Parallel SAT Framework....Pages 456-462
Improved Single Pass Algorithms for Resolution Proof Reduction....Pages 463-468
Creating Industrial-Like SAT Instances by Clustering and Reconstruction....Pages 469-470
Incremental QBF Preprocessing for Partial Design Verification....Pages 471-472
Concurrent Cube-and-Conquer....Pages 473-474
Satisfying versus Falsifying in Local Search for Satisfiability....Pages 475-476
Exploiting Historical Relationships of Clauses and Variables in Local Search for Satisfiability....Pages 477-478
Towards Massively Parallel Local Search for SAT....Pages 479-480
Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod....Pages 481-482
A Cardinality Solver: More Expressive Constraints for Free....Pages 483-484
Single-Solver Algorithms for 2QBF....Pages 485-486
An Efficient Method for Solving UNSAT 3-SAT and Similar Instances via Static Decomposition....Pages 487-488
Intensification Search in Modern SAT Solvers....Pages 489-490
Using Term Rewriting to Solve Bit-Vector Arithmetic Problems....Pages 491-492
Learning Polynomials over GF(2) in a SAT Solver....Pages 493-495
Learning Back-Clauses in SAT....Pages 496-497
Augmenting Clause Learning with Implied Literals....Pages 498-499
Back Matter....Pages 500-501
....Pages -