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

Front Matter....Pages -
Understanding IC3....Pages 1-14
Satisfiability and The Art of Computer Programming....Pages 15-15
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
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
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
Improved Single Pass Algorithms for Resolution Proof Reduction....Pages 469-470
Creating Industrial-Like SAT Instances by Clustering and Reconstruction....Pages 471-472
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
 SATLab : X-Raying Random k - SAT ....Pages 424-429
Resolution-Based Certificate Extraction for QBF....Pages 430-435
Coprocessor 2.0 – A Flexible CNF Simplifier....Pages 436-441
SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox....Pages 442-448
CoPAn: Exploring Recurring Patterns in Conflict Analysis of CDCL SAT Solvers....Pages 449-455
Azucar: A SAT-Based CSP Solver Using Compact Order Encoding....Pages 456-462
SatX10: A Scalable Plug&Play Parallel SAT Framework....Pages 463-468
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
Incremental QBF Preprocessing for Partial Design Verification....Pages 473-474
Concurrent Cube-and-Conquer....Pages 475-476
Satisfying versus Falsifying in Local Search for Satisfiability....Pages 477-478
Exploiting Historical Relationships of Clauses and Variables in Local Search for Satisfiability....Pages 479-480
Towards Massively Parallel Local Search for SAT....Pages 481-482
Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod....Pages 483-484
A Cardinality Solver: More Expressive Constraints for Free....Pages 485-486
Single-Solver Algorithms for 2QBF....Pages 487-488
An Efficient Method for Solving UNSAT 3-SAT and Similar Instances via Static Decomposition....Pages 489-490
Intensification Search in Modern SAT Solvers....Pages 491-492
Using Term Rewriting to Solve Bit-Vector Arithmetic Problems....Pages 493-495
Learning Polynomials over GF(2) in a SAT Solver....Pages 496-497
Learning Back-Clauses in SAT....Pages 498-499
Augmenting Clause Learning with Implied Literals....Pages 500-501
Back Matter....Pages -