Theory and Application of Satisfiability Testing
14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011, Proceedings
Published on 11. June 2011
XIII, 371 pages
978-3-642-21581-0 (ISBN)
Description
This book constitutes the refereed proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011, held in Ann Arbor, MI, USA in June 2011.The 25 revised full papers presented together with abstracts of 2 invited talks and 10 poster papers were carefully reviewed and selected from 57 submissions. The papers are organized in topical sections on complexity analysis, binary decision diagrams, theoretical analysis, extraction of minimal unsatisfiable subsets, SAT algorithms, quantified Boolean formulae, model enumeration and local search, and empirical evaluation.
More details
Other editions
Additional editions
Karem A. Sakallah | Laurent Simon
Theory and Application of Satisfiability Testing
14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011, Proceedings
Book
06/2011
Springer
€53.49
Shipment within 5-7 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Talks
- Connecting SAT Algorithms and Complexity Lower Bounds
- References
- Concolic Testing and Constraint Satisfaction
- References
- Technical Program
- Session 1: Complexity Analysis
- Parameterized Complexity of DPLL Search Procedures
- Introduction
- Preliminaries
- Parameterized Resolution and Parameterized DPLL
- Asymmetric Prover-Delayer Games for DPLL
- An Application of the Lower Bound Method
- DPLL and the Decision Tree Complexity of k-Clique
- References
- Satisfiability Certificates Verifiable in Subexponential Time
- Introduction
- Definitions
- Shortest Certificates for k-SAT
- Upper Bound on Certificate Length for k-SAT
- The Growth of Certificate Lengths for k-SAT
- Shortest Certificates for SAT?
- Shortest Certificates for CircuitSAT
- References
- On Variables with Few Occurrences in Conjunctive Normal Forms
- Introduction
- Preliminaries
- Non-mersenne Numbers
- Lean Clause-Sets and the Surplus
- The Special Case of Minimally Unsatisfiable Clause-Sets
- Proof of the General Case
- On Finding the Autarky
- On Strengthening the Bound
- Conclusion and Open Problems
- References
- Satisfiability of Acyclic and almost Acyclic CNF Formulas (II)
- Introduction
- Preliminaries
- Generalizing $\beta$-Acyclic Formulas
- An Example
- The NP-Completeness Result
- The Gadget and Its Properties
- The Reduction
- Intermediate Classes
- Grades of Tractability
- Comparisons
- Easy Classes
- Classes of Bounded Width
- Conclusion
- References
- Session 2: Binary Decision Diagrams
- BDDs for Pseudo-Boolean Constraints - Revisited
- Introduction
- Preliminaries
- Exponential BDDs for PB Constraints
- Intervals
- Some Families of PB Constraints and Their BDD Size
- Probably There Are No Small BDDs for All PB Constraints
- Avoiding Exponential BDDs
- Power-of-Two PB Constraints Do Have Polynomial-Size BDDs
- A Consistent Encoding for PB Constraints
- An Arc-Consistent Encoding for PB Constraints
- SAT Encodings of BDDs for Monotonic Functions
- Conclusions and Future Work
- References
- DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions
- Introduction
- Basic Mechanisms of DPLL+ROBDD Derivation
- Parallel DPLL+ROBDD Solver Sharing Arrays of Conflict Clauses in the ROBDD Form
- Experimental Results
- Conclusions and Future Work
- References
- $\pi$DD: A New Decision Diagram for Efficient Problem Solving in Permutation Space
- Introduction
- Preliminaries
- Sets of Permutations
- BDDs and ZDDs
- Data Structures
- Desired Properties for pDDs
- Decomposition of Permutations
- General Structure of pDDs
- Algorithms for Algebraic Operations
- Binary Set Operations
- Transposition
- Cartesian Product
- Cofactor
- Application Examples
- Design of Permutation Networks
- Analysis of Rubik's Cube
- Conclusion
- References
- Session 3: Theoretical Analysis
- How to Apply SAT-Solving for the Equivalence Test of Monotone Normal Forms
- Introduction
- Preliminaries
- Unit Propagation and Decision Strategies
- Solving Monet Using SAT-Solvers
- Experiments
- Conclusion
- References
- Enumerating All Solutions of a Boolean CSP by Non-decreasing Weight
- Introduction
- Material
- Constraint Languages and G-Formulae
- Enumeration
- Main Result
- Efficient Enumeration Algorithms
- Hardness Results
- Affine, 0-valid, not Horn
- Dual Horn, 0-valid, neither Affine nor Horn
- Conclusion
- References
- A Satisfiability-Based Approach for Embedding Generalized Tanglegrams on Level Graphs
- Introduction
- Preliminaries and Basic Notation
- Satisfiability Formulation of Crossing Minimization
- Conclusion and Open Problems
- References
- Session 4: Extraction of Minimal Unsatisfiable Subsets
- Minimally Unsatisfiable Boolean Circuits
- Introduction
- Preliminaries
- Definitions of Minimal Unsatisfiability
- Minimally Unsatisfiable Boolean Circuits
- Gate-Based Minimal Unsatisfiability
- Wire-Minimal Unsatisfiable Circuits
- Computing Circuit MUSes
- Empirical Study
- Conclusion
- References
- On Improving MUS Extraction Algorithms
- Introduction
- Preliminaries
- New Constructive Algorithm for MUS Extraction
- Hybrid MUS Extraction
- Analysis of Other Techniques
- Preprocessing and Interfacing SAT Solvers
- Results
- Related Work
- Conclusions
- References
- Faster Extraction of High-Level Minimal Unsatisfiable Cores
- Introduction
- Resolution-Based High-Level Core Minimization
- Optimizations
- Experimental Results
- Summary and Future Work
- References
- Session 5: SAT Algorithms
- On Freezing and Reactivating Learnt Clauses
- Introduction
- Definitions, Notations and Technical Background
- A New Measure for Identifying Relevant Learnt Clauses
- Freeze and Reactivate: A Dynamic Management Policy
- Empirical Evaluation
- Comparison with Different Quality Measures
- Comparison with State of the Art Solvers
- Conclusion
- References
- Efficient CNF Simplification Based on Binary Implication Graphs
- Introduction
- Preliminaries
- Known Simplification Techniques
- Hidden Literal Elimination
- Unhiding Redundancies Based on Time Stamping
- Basic Time Stamping
- Capturing Various Simplifications
- Hidden Literals
- Hidden Tautologies
- Adding Hyper Binary Resolution
- Some Limitations of Basic Stamping
- Advanced Stamping for Capturing Additional Simplifications
- Transitive Reduction
- Failed Literal Elimination over F2
- Equivalent Literal Substitution
- Experiments
- Conclusions
- References
- Between Restarts and Backjumps
- Introduction
- Conflict-Driven Clause Learning Solvers
- Heuristics
- Decision Levels and Backjumping
- Restart Strategies
- Motivation
- Partial Restart
- Restart Frequency
- Reducing Restart Costs
- Matching Trail
- Permuted Trail
- Discussion
- Experimental Results
- Matching Trail
- Permuted Trail
- Suggestions for Future Work
- Conclusion
- Session 6: Quantified Boolean Formulae
- Abstraction-Based Algorithm for 2QBF
- Introduction
- Preliminaries
- Counterexample Guided Abstraction Refinement (CEGAR)
- Problems
- Algorithm for the 2QBF problem
- Algorithm
- Properties
- Algorithm for the 2QCNF problem
- Heuristics
- Experimental Results
- Related Work
- Conclusions
- References
- Transformations into Normal Forms for Quantified Circuits
- Introduction
- Boolean Circuits and Propositional Formulas
- Quantified Boolean Formulas
- Nested Boolean Functions
- Quantified Circuits
- Normal Forms
- Quantified Circuits in Prenex Form
- Pure Quantified Circuits in Non-prenex Form
- Non-pure Quantified Circuits
- Conclusion
- References
- Failed Literal Detection for QBF
- Introduction
- Preliminaries
- SAT-Based FL
- Abstraction-Based FL
- QBCP-Guided Q-Resolution
- Comparing FL Approaches
- Experiments
- Conclusion
- References
- Session 7: Model Enumeration, Local Search
- Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One
- Introduction
- State-of-the-Art SAT Solvers
- Problem Definition
- Benchmarks
- Chaotic Behavior of SAT
- Trying a Local Search-Like Solution
- Our Barcelogic Approach
- Experimental Comparison with Cplex and Other Tools
- Factor Analysis of the Barcelogic Approach
- Related Work and Conclusions
- References
- Generating Diverse Solutions in SAT
- Introduction
- Related Work and Background
- Definitions
- Analizing Existing Algorithms
- Variable-Based Methods
- Local Variable-Based Methods for PGUIDE
- Local Variable-Based Methods for PBCPGUIDE
- Global Variable-Based Methods
- Conclusions and Future Work
- References
- Captain Jack: New Variable Selection Heuristics in Local Search for SAT
- Introduction
- Background
- SPARROW
- VE-SAMPLER and PARAMILS
- Design Considerations underlying CAPTAIN JACK
- CaptainJack
- Experimental Setup
- Results and Discussion
- Conclusions and Future Work
- References
- Session 8: Empirical Evaluation
- Careful Ranking of Multiple Solvers with Timeouts and Ties
- Introduction and Overview
- Related Work
- What Is a Tie?
- Pairwise Matches
- Competition Ranking
- Results on the SAT 2009 Competition
- Robustness of Ranking
- Differences in Ranking
- Tie-Break Illustration
- Conclusion
- References
- Generalized Conflict-Clause Strengthening for Satisfiability Solvers
- Introduction
- Terminology and Notation
- Implication Sequences
- DPLL and Implication Sequences
- CDCL and Implication Sequences
- Traditional Use of Implication Sequences
- Implication Sequences Are Horn Renamable
- Conflict-Clause Strengthening Problem
- Implication Sequences and Linear Input Regular Derivations
- The General Minimum Conflict Clause Problem Is NP-Complete
- Conclusion
- References
- Empirical Study of the Anatomy of Modern Sat Solvers
- Introduction
- Major Features of CDCL Solvers
- Conflict-Driven Clause Learning
- Random Restarts
- Boolean Constraint Propagation Using Lazy Data Structures
- Conflict-Based Adaptive Branching
- MiniSAT Configurations
- Benchmarks
- Experimental Evaluation
- Relative Contribution of Major CDCL Features
- The Impact of Additional Options in CDCL Solvers
- Conclusions
- References
- Extended Abstracts
- Translating Pseudo-Boolean Constraints into CNF
- Introduction
- ProposedMethod
- Performance of Unit Propagation
- Conclusion
- References
- Analyzing the Instances of the MaxSAT Evaluation
- Reference
- Model Counting Using the Inclusion-Exclusion Principle
- References
- Phase Transitions in Knowledge Compilation: An Experimental Study
- Introduction and Background
- Main Results
- References
- EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation
- References
- Non-Model-Based Algorithm Portfolios for SAT
- References
- The Order Encoding: From Tractable CSP to Tractable SAT
- References
- Applying UCT to Boolean Satisfiability
- References
- A Compact and Efficient SAT-Encoding of Finite Domain CSP
- Extended Abstract
- References
- Learning Polarity from Structure in SAT
- Introduction
- Polarity Prediction as Supervised Learning
- Classification for Assignment Initialization
- References
- Author Index
