Theory and Applications of Satisfiability Testing -- SAT 2015

Name: Theory and Applications of Satisfiability Testing -- SAT 2015 | 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings
Brand: Springer
Price: 67.4 EUR
Availability: OnlineOnly

18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings

Marijn Heule Sean Weaver(Herausgeber*in)

Springer (Verlag)

Erschienen am 17. September 2015

XIX, 436 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-24318-4 (ISBN)

67,40 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Pragmatic Approach to Formal Verification
Applying Satisfiability to the Analysisof Cryptography
Random Formulas are Irrelevant, Right?
Contents
CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
1 Introduction
2 Solver Description
2.1 The CCA Heuristic and Swcca
2.2 The CCAnr Algorithm
2.3 Implementation Details
3 Experimental Results
References
PBLib -- A Library for Encoding Pseudo-Boolean Constraints into CNF
1 Introduction
2 Pseudo-Boolean Constraints and Encodings
3 Description of the PBLib
3.1 Components of the PBLib
3.2 Example
4 Included Tools
5 Empirical Evaluation and Related Work
6 Conclusion
References
Speeding up MUS Extraction with Preprocessing and Chunking
1 Introduction
2 Preliminaries
3 LMUS Extraction
4 Chunking
5 Experiments
5.1 Overall GMUS Evaluation
5.2 Parameter Impact
6 Conclusions
References
Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP
1 Introduction
1.1 Related Work
1.2 Organization of the Paper
2 Preliminaries
2.1 MAXSAT, MAX-k-SAT, MAX-k-CSP
2.2 Concentration Bounds
3 MAX-k-CSP
3.1 Known Algorithms for MAX-2-CSP
3.2 A Polynomial-space Algorithm for MAX-k-CSP
3.3 An Exponential-Space Algorithm for MAX-k-CSP
4 MAX-SAT and MAX-k-SAT
4.1 A Polynomial-Space Algorithm for MAX-SAT
4.2 An Exponential-Space Algorithm for MAX-SAT
5 Sparse Depth-2 Threshold Circuits
6 Open Questions
References
Laissez-Faire Caching for Parallel #SAT Solving
1 Introduction
2 Basic Notations
3 #SAT Solving
3.1 Conflict Learning
3.2 Sub-Formula Decomposition
3.3 Formula Caching
3.4 Incorrect Results in the Cache
4 Laissez-Faire Caching
4.1 Node Re-Computation
4.2 Memory Consumption and Cleanup
5 countAntom Solver Structure
5.1 Node Computation
5.2 Node Order
5.3 Caching
6 Experimental Results
6.1 Benchmarks
6.2 Parallel Performance
6.3 Impact of Laissez-Faire Caching
7 Conclusion
References
SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers
1 Introduction
2 How SATGraf Works
3 Results
3.1 Observation #1: VSIDS Chooses High-Centrality Bridge Variables
3.2 Observation #2: VSIDS Moves Infrequently Between Communities
3.3 Observation #3: Backtracking May Incur Unnecessary Overhead
4 Related Work
5 Conclusion
References
Hints Revealed
1 Introduction
2 Preliminaries
3 Hint Addition
4 Hint Creation Algorithms
4.1 Avoiding Failing Branches
4.2 Randomized Hints
5 Theoretical Basis
6 Experimental Results
6.1 AFB Results: SAT 2013
6.2 AFB Results: SAT 2014
6.3 RH Results: SAT 2013
7 Discussion
References
Mining Backbone Literals in Incremental SAT
1 Introduction
2 Mining Backbone Literals
2.1 Optimizations and Implementation Details
2.2 Constants can Increase the Number of Assumptions
3 A Case Study: Using MBL in the Context of MUC Extraction
3.1 How HaifaMUC Extracts Minimal Unsatisfiable Cores
3.2 Experiments
3.3 Mitigating the Side-Effect of Assumptions on MUC Search
4 Conclusions and Future Work
References
Constructing SAT Filters with a Quantum Annealer
1 Introduction
2 Filters, SAT Filters and Blocked SAT Filters
2.1 SAT Filters
2.2 Blocked SAT Filters
3 Solving CSPs in the Ising Model with a D-Wave Processor
3.1 Constraint Satisfaction Problems in the Ising Model
3.2 Graph Minors in the Ising Model
4 SAT Variants in the Ising Model
4.1 NAE3SAT
Monotone NAE3SAT.
4.2 MAX-CUT SAT Variants
4.3 Bipartite 4FLSAT
4.4 Threshold Analysis
4.5 Software Solvers
5 Case Study 1: A Blocked MNAE3SAT Filter
6 Case Study 2: Filter and Performance Scaling
6.1 Scaling of Solution Time
7 Conclusions
References
#SAT: Projected Model Counting
1 Introduction
2 Preliminaries
3 Model Counting
3.1 Solution Enumeration Using SAT Solvers
3.2 DPLL-style Model Counting
4 Projected Model Counting
4.1 Restricting Search to Priority Variables
4.2 Blocking Seen Solutions
4.3 Counting Models of Projected d-DNNF
5 Experiments
5.1 Uniform Random 3-SAT and Boolean Circuits
5.2 Planning
6 Related Work and Conclusion
References
Computing Maximal Autarkies with Few and Simple Oracle Queries
1 Introduction
2 Preliminaries
3 Oracles
4 The Basic Translation
4.1 Basic Usages
4.2 Adding Positive ``Steering'' Clauses
5 The New Algorithm
6 Conclusion and Outlook
References
HordeSat: A Massively Parallel Portfolio SAT Solver
1 Introduction
2 Preliminaries
3 Related Work
4 Design Decisions
5 Black Box for Portfolios
6 The Portfolio Algorithm
6.1 Diversification
6.2 Clause Sharing
7 Experimental Evaluation
7.1 Clause Sharing and Diversification
7.2 Scaling on Application Benchmarks
7.3 Comparison with Plingeling
8 Conclusion
8.1 Future Work
References
Preprocessing for DQBF
1 Introduction
2 Preliminaries
3 Incomplete, but Cheap Decision Procedures
4 Preprocessing Techniques for DQBF
4.1 Backbones, Monotonic and Equivalent Variables
4.2 Reduction of Dependency Sets
4.3 Universal Reduction, Resolution, and Universal Expansion
4.4 Blocked Clause Elimination
4.5 Structure Extraction
5 Experimental Results
6 Conclusion
References
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
1 Introduction
2 Implementing a Clause Group API
3 Computing Minimal Unsatisfiable Cores of QBFs
4 Conclusion
References
On Compiling CNFs into Structured Deterministic DNNFs
1 Introduction
2 Preliminaries
3 From Dynamic Programming to Structured d-DNNFs
3.1 Branch Decompositions, Projections, and PS-width
3.2 Records and Dynamic Programming
3.3 Constructing a Structured d-DNNF
4 Corollaries
5 A Lower Bound for Clique-Width
6 Conclusion
References
SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
1 Introduction
2 Algorithm Configuration and Analysis
3 SpySMAC's Framework
4 Spying on Lingeling and probSAT
5 Conclusion
References
Community Structure Inspired Algorithms for SAT and #SAT
1 Introduction
2 Preliminaries
2.1 SAT and #SAT
2.2 Parameterized Complexity
2.3 Hitting Formulas
2.4 Treewidth
3 h-Communities and h-Modularity
4 Finding h-Structures
5 Using h-Structures
6 Concluding Notes
References
Using Community Structure to Detect Relevant Learnt Clauses
1 Introduction
2 Preliminaries
3 Clause Learning Destroys the Community Structure
4 On the Relevance of Learnt Clauses
5 Detecting Relevant Learnt Clauses
6 Experimental Evaluation
7 Related Work
8 Conclusions and Future Work
References
Recognition of Nested Gates in CNF Formulas
1 Introduction
1.1 Related Work
1.2 Contributions
2 Theoretical Background
2.1 Gates and Monotonicity
2.2 And-Inverter Graphs (AIG)
2.3 Preprocessing
3 Recognition of Nested Gates
3.1 Iterative Root Selection
3.2 Recursive Gate Extraction
3.3 Equivalence Detection Methods
3.4 AIG Construction
4 Experimental Results
4.1 Equivalence Detection Methods
4.2 Preprocessing and Gate Recognition
4.3 Maximum Number of Recognition Tries
4.4 And-Inverter Graphs
5 Conclusion and Future Work
References
Exploiting Resolution-Based Representations for MaxSAT Solving
1 Introduction
2 Preliminaries
3 Graph Representations
4 New Partition-Based Algorithm for MaxSAT
4.1 Algorithm Description
4.2 Partition and Merge of Soft Clauses
4.3 Algorithm Analysis
5 Experimental Results
6 Conclusions and Future Work
References
SAT-Based Formula Simplification
1 Introduction
2 Preliminaries
3 Formula Simplification with SAT
3.1 Prime Implicant/Implicate Enumeration
3.2 Computing a Smallest Prime Cover
4 Preliminary Results
4.1 PLA Benchmarks
4.2 Bi-decomposition Interpolation Benchmarks
4.3 Quasigroup Classification Benchmarks
5 Conclusions
References
Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
1 Introduction
2 Volt: A Lazy Grounding Framework
3 Empirical Evaluation
4 Conclusion
References
Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
1 Introduction
2 Background
2.1 COMiniSatPS
2.2 VSIDS Branching Heuristic
2.3 Learned Clause Management
2.4 Restart Strategies
3 The SAT/UNSAT Difference of CDCL in Practice
3.1 Roles of Learned Clauses
3.2 Effects of Restarts
3.3 VSIDS and Variable Decay Factor
4 Refining the Hybrid Strategy
5 Conclusion
References
Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
1 Introduction
2 Preliminaries
3 MUS Enumeration in Horn Formulae
4 Algorithm for Group-MUS Enumeration in Horn Formulae
4.1 Organization
4.2 Computing Maximal Models
4.3 Adding Blocking Clauses
4.4 Deciding Satisfiability of Horn Formulae
4.5 MUS Extraction in Horn Formulae
5 Comparison with Existing Alternatives
5.1 EL+SAT
5.2 EL2MCS
5.3 SATPin
6 Experimental Results
6.1 Experimental Setup
6.2 COI Instances
6.3 x2 Instances
6.4 Assessment of Non SAT-Based Axiom Pinpointing Tools
7 Conclusions and Future Work
References
QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
1 Introduction
2 Preliminaries
3 Algorithmic Flow
4 Learning
4.1 Solution Learning by Levelized Blocking
4.2 Solution Learning in the Presence of Circuit Information
4.3 Conflict Learning
5 Related Work
6 Experimental Results
7 Conclusion and Future Work
References
SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
1 Introduction
2 System Architecture
2.1 Data Structures and Basic Procedures: CArL carl
2.2 Interfaces and Strategic Compositions of Procedures: SMT-RAT smtrathtml
3 Experimental Results and Future Work
References
Search-Space Partitioning for Parallelizing SMT Solvers
1 Introduction
2 Preliminaries
3 Parallelization Approaches for SMT
3.1 Search-Space Partitioning in SMT
3.2 Combining Search Space Partitioning and Portfolio
4 A Cloud-Based Parallel SMT Solver for QF_UF
4.1 Partitioning Heuristics
4.2 The Client-Server Architecture
5 Experimental Results
5.1 Comparing the Implementation to the Portfolio Approach
5.2 Comparing the Partitioning Heuristics
5.3 Comparison to Other SMT Solvers
6 Conclusions
References
A New Approach to Partial MUS Enumeration
1 Introduction
2 Preliminaries
3 Related Work and the MARCO Algorithm
3.1 The MARCO Algorithm
4 A First Extension: Determine MUS Members via Map
5 Using Blocks to Speed-Up Partial MUS Enumeration
5.1 Determine the Blocks
5.2 Proving the Block Property
5.3 Using Block Information During shrink-Method
5.4 Using Block Information to Find More MCSes
6 Practical Results
6.1 Workload Computation
7 Conclusion
References
Evaluating CDCL Variable Scoring Schemes
1 Introduction
2 Decision Heuristics
3 Implementation
3.1 Fast Queue for VMTF
3.2 Generic Queue for all Decision Heuristics
3.3 Rescore, Reuse-Trail and Complexity
4 Results
5 Conclusion
References
SAT-Based Horn Least Upper Bounds
1 Introduction
2 Preliminaries
3 SAT-Based Algorithms
3.1 HFLUBBER: An Iterative Refinement Approach
3.2 IP-HORN: Computing all Horn Prime Implicates
3.3 Discussion
4 Results
5 Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken