Theory and Applications of Satisfiability Testing -- SAT 2012

Name: Theory and Applications of Satisfiability Testing -- SAT 2012 | 15th International Conference, Trento, Italy, June 17-20, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

15th International Conference, Trento, Italy, June 17-20, 2012, Proceedings

Alessandro Cimatti Roberto Sebastiani(Herausgeber*in)

Springer (Verlag)

Erschienen am 18. Juni 2012

XIV, 500 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-31612-8 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken