Theory and Application of Satisfiability Testing

Name: Theory and Application of Satisfiability Testing | 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011, Proceedings

Karem A. Sakallah Laurent Simon(Herausgeber*in)

Springer (Verlag)

Erschienen am 11. Juni 2011

XIII, 371 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-21581-0 (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
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

Systemvoraussetzungen

Als PDF speichern Als Link merken