Theory and Applications of Satisfiability Testing -- SAT 2012
15th International Conference, Trento, Italy, June 17-20, 2012, Proceedings
Published on 18. June 2012
XIV, 500 pages
978-3-642-31612-8 (ISBN)
Description
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.
More details
Other editions
Additional editions
Alessandro Cimatti | Roberto Sebastiani
Theory and Applications of Satisfiability Testing -- SAT 2012
15th International Conference, Trento, Italy, June 17-20, 2012, Proceedings
Book
06/2012
Springer
€53.49
Shipment within 7-9 days
Content
- Intro
- Title
- Preface
- Organization
- Table of Contents
- Invited Talks
- Understanding IC3
- Motivation
- Monolithic and Incremental Proof Methods
- Initial Attempts at Incremental, Inductive Algorithms
- Other SAT-Based Approaches
- IC3
- Perspective One: IC3 as a Prover
- Perspective Two: IC3 as a Bug Finder
- Beyond IC3: Incremental, Inductive Verification
- Challenges for SAT and SMT Solvers
- What's Next?
- References
- Satisfiability and The Art of Computer Programming
- Full Papers
- Stochastic Local Search
- Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break
- Introduction
- The New Algorithm Paradigm
- An Exponential Function
- A Polynomial Function
- Some Remarks
- Experimental Analysis of the Functions
- The Benchmark Formulae
- Good Parameter Setting for cb and cm
- Evaluations
- Soft- and Hardware
- The Competitors
- Results
- Comparison with WalkSAT
- Summary and Future Work
- References
- Off the Trail: Re-examining the CDCL Algorithm
- Introduction
- Examining the CDCL Algorithm
- Local Search
- Connection to CDCL
- Other Failed Implications
- Potential Extension to QBF Solving
- Experiments
- Conclusion
- References
- Theory
- An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
- Introduction
- Preliminaries and Main Results
- Proof of Main Theorems
- References
- Computing Resolution-Path Dependencies in Linear Time
- Introduction
- Preliminaries
- Quantified Boolean Formulas
- Q-Resolution
- Dependency Schemes
- Resolution-Path Dependencies
- Computing Resolution-Path Dependencies
- Minimal Dependency Schemes
- Conclusion
- References
- Strong Backdoors to Nested Satisfiability
- Introduction
- Preliminaries
- Detection of Strong Nested-Backdoor Sets
- Large Grid Minor
- Conclusion
- References
- Quantified Boolean Formulae
- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
- Introduction
- Preliminaries
- Pure Literals in QBF
- QBF Abstraction
- Experimental Results
- Complete Solutions with 1-Saturation
- Timed Runs with 1-Saturation and a Complete Solver
- Conclusion
- References
- On Sequent Systems and Resolution for QBFs
- Introduction
- Preliminaries
- Calculi for Quantified Boolean Formulas
- Sequent Calculi for Quantified Boolean Formulas
- The Q-resolution Calculus
- Comparing Different Quantifier Rules
- Using Eliminable Extensions to Simulate rf/lf by rv/lv
- Exponential Separation of Q-res and Gqve*
- The Construction of n
- Short Proofs of n in Gqve*
- Q-resolution Refutations of n
- Conclusion
- References
- Solving QBF with Counterexample Guided Refinement
- Introduction
- Preliminaries
- Game-Centric View
- Recursive CEGAR-Based Algorithm
- Improving Recursive CEGAR-Based Algorithm
- Properties of the Algorithms
- Implementation Details
- CEGAR as a Learning Technique in DPLL
- Implementation Details
- Experimental Results
- Related Work
- Conclusions and Future Work
- References
- Henkin Quantifiers and Boolean Formulae
- Introduction
- Preliminaries
- Quantified Boolean Formulae
- Dependency Quantified Boolean Formulae
- Properties of DQBF
- Negation vs. Complement
- Formula Expansion on Existential Variables
- Prenex and Non-prenex Conversion
- Applications
- Discussions
- Conclusions
- References
- Applications
- Lynx: A Programmatic SAT Solver for the RNA-Folding Problem
- Introduction
- Our Contributions
- Existing Approaches to Incremental and Adaptive Solving
- RNA-Folding with Lynx
- Incrementality in Lynx
- Biological Problem Overview
- Structure Prediction via SAT
- RNA Secondary Structure Prediction with Pseudoknots
- Encoding RNA Structure Prediction in SAT
- Experimental Results
- Description of Input Tests
- Experimental Methodology
- Results
- Discussion
- Related Work
- Conclusions
- References
- Generalized Property Directed Reachability
- Introduction
- From Safety Verification to Least Fixed-points
- Abstract Property Directed Reachability
- PDR as an Abstract Transition System
- Nonlinear PDR
- State
- Algorithm Specification
- Theories - The Case of Linear Real Arithmetic
- Conflicts
- Timed Push-Down Systems
- Decisions
- Implementation and Experiments
- Conclusions, Related and Future Work
- References
- SMT-Aided Combinatorial Materials Discovery
- Introduction
- Combinatorial Materials Discovery
- Phase Map Identification
- Prior Work
- SMT-Aided Phase Map Identification
- Model Parameters
- Variables
- Constraints
- Missing Peaks Bound.
- Phase Usage.
- Shift Continuity.
- Shift Monotonicity.
- Ternary Phases Shift.
- Connectivity Constraint.
- Symmetry Breaking.
- Experimental Results
- Synthetic Data.
- Running Time.
- Solving Strategy.
- Accuracy.
- Robustness.
- Conclusions
- References
- Faulty Interaction Identification via Constraint Solving and Optimization
- Introduction
- Definitions
- Formulation as a Constraint Satisfaction Problem
- Translation to Pseudo-Boolean Optimization Problem
- Encoding
- Tool Support
- Experiments
- Simulation Results
- Experiment on a Real System
- Related Works
- Concluding Remarks
- References
- Parallel and Portfolio Approaches
- Revisiting Clause Exchange in Parallel SAT Solving
- Introduction
- Technical Background
- Parallelism, Collaboration and Clause Exchange: A Premilinary Experimentation
- Selecting, Sharing and Activating Good Clauses
- Comparison with State of the Art Solvers
- Conclusion
- References
- Designing Scalable Parallel SAT Solvers
- Introduction
- Preliminaries
- Parallel Solving Approaches
- Plain Partitioning Can Increase Expected Run Time
- Multi-core Implementations
- The Iterative Partitioning Approach
- Clause Learning
- Results
- Experimental Setup
- Scalability of the Multi-core Implementation
- Selecting a Scalable Algorithm
- Conclusions and Future Work
- References
- Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors
- Introduction
- Improved Automated Construction of Portfolio-Based Algorithm Selectors: SATzilla 2011
- Measuring the Value of a Solver
- Experimental Setup
- Experimental Results
- Conclusions
- References
- CDCL SAT Solving
- Efficient SAT Solving under Assumptions
- Introduction
- Background
- Preprocessing under Assumptions
- Transforming Temporary Clauses to Pervasive Clauses
- Incremental SAT Solving under Assumptions with Step Look-Ahead
- Experimental Results
- Conclusion
- References
- Preprocessing in Incremental SAT
- Introduction
- Preliminaries
- Incremental Preprocessing
- Experimental Results
- Conclusion
- References
- MAX-SAT, Cores Interpolants
- On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets
- Introduction
- Preliminaries
- Singularity
- Confluence of Singular DP-Reduction
- Permutations of Sequences of DP-Reductions
- Iterated DP-Reduction
- Iterated sDP-Reduction via Singular Tuples
- Without 1-Singular Variables
- The Singularity Index
- Confluence Mod Isomorphism on Eventually SM U
- Conclusion and Open Problems
- References
- Improvements to Core-Guided Binary Search for MaxSAT
- Introduction
- Preliminaries
- Improving BCD
- Proof of Correctness
- Additional Techniques
- Hardening Rule
- Biased Search
- Experimental Evaluation
- Conclusions
- References
- On Efficient Computation of Variable MUSes
- Introduction
- Preliminaries
- Variable-MUS Computation Problem, and Generalizations
- VMUS
- Generalizations
- Algorithms for VMUS Computation
- Hybrid VMUS Computation
- Relaxation-Variables Approach
- Reduction to Group-MUS Computation
- Applications of VMUSes
- Experimental Study
- Conclusion
- References
- Interpolant Strength Revisited
- Introduction
- Background
- Formulae and Proofs
- Interpolation Systems and Labelling Functions
- Interpolation for Hyper-resolution
- Hyper-resolution and Resolution Chains
- Local Refutations and Hyper-resolution
- Related Work
- Consequences and Conclusion
- References
- Complexity Analysis
- Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas
- Introduction
- Background and Motivation
- Backtracking
- Proving Upper Bounds for Satisfiability Thresholds
- Applying the Interpolation Method to Random CNFs Formulas
- The Energetic Interpolation Method
- Energy Density Bounds for (2+p)-SAT
- Application to (2+p)-SAT
- References
- Parameterized Complexity of Weighted Satisfiability Problems
- Introduction
- Preliminaries
- Weighted Satisfiability Problems
- The Complexity of Weighted Satisfiability Problems
- Complexity of the Counting Problems
- Conclusion
- References
- Fixed-Parameter Tractability of Satisfying beyond the Number of Variables
- Introduction
- Additional Terminology, Notation and Preliminaries
- Preprocessing Rules
- Branching Rules and Reduction to (m-k)-Hitting Set
- Improved FPT Algorithm for (m-k)-Hitting Set
- Complete Algorithm, Correctness and Analysis
- Hardness of Kernelization
- Conclusion
- References
- Circuits and Encodings
- Finding Efficient Circuits for Ensemble Computation
- Introduction
- OR-Circuits, SUM-Circuits, and Rewriting
- Definitions
- Bounds for Separation
- Upper Bounds for Rewriting
- Subquadratic Rewriting Implies Faster CNF-SAT
- Finding Small Circuits Using SAT Solvers
- SAT Encoding
- Practical Considerations
- Experiments
- Instance Generation and Experimental Setup
- Optimal Circuits for All Small Ensembles
- Scaling on Structured Ensembles
- Conclusions
- References
- Conflict-Driven XOR-Clause Learning
- Introduction
- Preliminaries
- The DPLL(XOR) Framework
- The Xor-Reasoning Module ``UP''
- Parity Explanations
- Resolution Cannot Polynomially Simulate Parity Explanations
- Learning Parity Explanations
- General Xor-Derivations
- Experimental Results
- Conclusions
- References
- Perfect Hashing and CNF Encodings of Cardinality Constraints
- Introduction
- Efficient Encodings and Related Work
- Our Contribution
- Perfect Hashing
- Perfect Hashing - Constructions
- (n,2,2,"4264306 logn "5265307 ) PHF
- (n,3,3,"4264306 log32 n"5265307 ) PHF
- (n,,O"0365O(2 logn),2 logn) PHF
- New Encodings Based on PHFs
- Encoding the k(X1,.,Xn) Constraint
- Encoding the k(X1,.,Xn) Constraint
- Hybrid Encodings
- Experiments
- Setting
- Results - Conclusion
- Results - Details
- Concluding Remarks and Future Work
- References
- The Community Structure of SAT Formulas
- Introduction
- Preliminaries
- Modularity in Large-Scale Graphs
- Modularity of SAT Instances
- Modularity of the Learnt Clauses
- Modularity of Random Formulas
- Conclusions
- References
- Tool Presentations
- SATLab: X-Raying Random k-SAT (Tool Presentation)
- Introduction
- SATLab's Features
- Installing SATLab
- What SATLab Does
- SATLab's Universe
- Case Study: The Structure of the Solutions Space
- References
- Resolution-Based Certificate Extraction for QBF
- Introduction
- The Certification Framework at a Glance
- Experiments
- Discussion
- References
- Coprocessor 2.0 - A Flexible CNF Simplifier
- Introduction
- Preprocessing
- Limited Preprocessing
- Simplifying During Search
- Implementation Details
- Empirical Results
- Conclusion
- References
- SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox (Tool Presentation)
- Introduction
- Satisfiability Modulo Real Arithmetic
- Toolbox Design
- Experimental Results
- Conclusion and Future Work
- References
- CoPAn: Exploring Recurring Patterns in Conflict Analysis of CDCL SAT Solvers (Tool Presentation)
- Introduction and Motivation
- The Application
- Patterns in Clause Learning
- The CoPAn GUI
- User-Defined Analysis
- Theoretical and Algorithmic Background
- Summary
- References
- Azucar: A SAT-Based CSP Solver Using Compact Order Encoding (Tool Presentation)
- Introduction
- Compact Order Encoding
- Azucar Implementation
- Performance Evaluation
- Conclusion
- References
- SatX10: A Scalable Plug&Play Parallel SAT Framework (Tool Presentation)
- Introduction
- Background
- X10: A Parallelization Framework
- Building Parallel SAT Solvers with X10
- Empirical Demonstration
- References
- Poster Presentations
- Improved Single Pass Algorithms for Resolution Proof Reduction (Poster Presentation)
- References
- Creating Industrial-Like SAT Instances by Clustering and Reconstruction (Poster Presentation)
- Introduction
- Used Methodology
- Results
- References
- Incremental QBF Preprocessing for Partial Design Verification (Poster Presentation)
- References
- Concurrent Cube-and-Conquer (Poster Presentation)
- References
- Satisfying versus Falsifying in Local Search for Satisfiability (Poster Presentation)
- References
- Exploiting Historical Relationships of Clausesand Variables in Local Search for Satisfiability (Poster Presentation)
- References
- Towards Massively Parallel Local Search for SAT (Poster Presentation)
- References
- Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod (Poster Presentation)
- References
- A Cardinality Solver: More Expressive Constraints for Free (Poster Presentation)
- References
- Single-Solver Algorithms for 2QBF (Poster Presentation)
- References
- An Efficient Method for Solving UNSAT 3-SAT and Similar Instances via Static Decomposition (Poster Presentation)
- References
- Intensification Search in Modern SAT Solvers(Poster Presentation)
- References
- Using Term Rewriting to Solve Bit-Vector Arithmetic Problems (Poster Presentation)
- References
- Learning Polynomials over GF(2) in a SAT Solver (Poster Presentation)
- Introduction
- Structure of the Solver
- References
- Learning Back-Clauses in SAT (Poster Presentation)
- References
- Augmenting Clause Learning with Implied Literals (Poster Presentation)
- References
- Author Index
