Theory and Applications of Satisfiability Testing - SAT 2017

Name: Theory and Applications of Satisfiability Testing - SAT 2017 | 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings

Serge Gaspers Toby Walsh(Herausgeber*in)

Springer (Verlag)

Erschienen am 14. August 2017

XIII, 476 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-66263-3 (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

Intro
Preface
Organization
Contents
Algorithms, Complexity, and Lower Bounds
Probabilistic Model Counting with Short XORs
1 Introduction
2 Lower Bounds are Easy
2.1 Searching for a Lower Bound
2.2 Choice of Constants
2.3 Dealing with Timeouts
3 What Does it Take to Get a Good Lower Bound?
4 Accurate Counting Without Pairwise Independence
5 Nested Sample Sets
6 Proof of Theorem 3
6.1 Proof for Monotone Sequences of Sample Sets
7 Low Density Parity Check Codes
8 Tractable Distributions
8.1 The Lumpiness of LDPC Codes
9 Experiments
References
Backdoor Treewidth for SAT
1 Introduction
2 Preliminaries
3 Backdoor Treewidth
4 Acyclic Backdoors to Scattered Classes for SAT
5 Conclusions
References
New Width Parameters for Model Counting
1 Introduction
1.1 Contribution
2 Preliminaries
2.1 SAT and #SAT
2.2 Parameterized Complexity
2.3 Treewidth
3 Consensus Treewidth
4 Conflict Treewidth
5 Concluding Remarks
References
Hard Satisfiable Formulas for Splittings by Linear Combinations
1 Introduction
2 DPLL() and Parity Decision Trees
3 Lower Bound
References
Clause Learning and Symmetry Handling
On the Community Structure of Bounded Model Checking SAT Problems
1 Introduction
2 Preliminaries
3 Communities and Unrolling Depth in SAT Encodings
3.1 Communities are Stronger When Spreading over Time Steps
4 Unrolling Depth of Decisions, Resolutions and Learnt Clauses
4.1 Relation Between Solver Progress and Unrolling Depths
4.2 Unrolling Depth and Literal Block Distance
4.3 On the Relation Between Decisions, Resolutions and Learning During Solver Search
4.4 On the Relation Between Variable Unrolling Depths and Variable Eliminations
5 Discussions About Improving SAT Solvers
5.1 Shifting Variables Scores
5.2 Scoring Clauses w.r.t. Max-Min of Unrolling Iterations
5.3 Forcing Variable Elimination According to Their Unrolling Iterations
5.4 Further Possible Ways of Improvements
6 Conclusions
References
Symmetric Explanation Learning: Effective Dynamic Symmetry Handling for SAT
1 Introduction
2 Preliminaries
2.1 Conflict Driven Clause Learning SAT Solvers
3 Symmetric Explanation Learning
3.1 Complexity of SEL
4 Related Work
4.1 SEL and SLS
4.2 SEL and SP
4.3 Compatibility of Symmetrical Learning and Preprocessing Techniques
4.4 Symmetrical Learning Does Not Break Symmetry
5 Experiments
5.1 Row Interchangeability
5.2 Evaluation of SEL
6 Conclusion
References
An Adaptive Prefix-Assignment Technique for Symmetry Reduction
1 Introduction
2 Preliminaries on Group Actions and Symmetry
3 McKay's Canonical Extension Method
4 Generation of Partial Assignments
5 Representation Using Vertex-Colored Graphs
6 Preliminary Experimental Evaluation
References
An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate
1 Introduction
1.1 Contributions
2 Background
3 GLR Maximization as a Branching Heuristic Objective
3.1 GLR vs Solving Time
4 Greedy Maximization of GLR
4.1 Experimental Results
5 Stochastic Gradient Descent Branching Heuristic
5.1 Experimental Results
6 Threats to Validity
7 Related Work
8 Conclusion and Future Work
References
Coverage-Based Clause Reduction Heuristics for CDCL Solvers
1 Introduction
2 Clause Reduction Heuristics
3 Experimental Evaluation of LBD
4 Issues of Glucose Reduction Strategy
5 Coverage-Based Reduction Strategy
6 Experimental Results
7 Conclusion
References
Maximum Satisfiability and Minimal Correction Sets
(I Can Get) Satisfaction: Preference-Based Scheduling for Concert-Goers at Multi-venue Music Festivals
1 Introduction
2 Problem Definition
2.1 Parameters
2.2 Preference Learning Subproblem
2.3 Scheduling Subproblem
3 System Architecture
4 MaxSAT Model
4.1 A Boolean Formulation
4.2 Weighted Partial MaxSAT Encoding
5 Constraint Programming Model
6 Learning User Preferences
7 Empirical Evaluation
7.1 Preference Learning Evaluation
7.2 Schedule Evaluation
8 Related Work
9 Conclusions and Future Work
References
On Tackling the Limits of Resolution in SAT Solving
1 Introduction
2 Preliminaries
2.1 Propositional Encodings of the Pigeonhole Principle
2.2 MaxSAT, MaxSAT Resolution and MaxSAT Algorithms
2.3 Related Work
3 Reducing SAT to HornMaxSAT
4 Short MaxSAT Proofs for PHP
4.1 A Polynomial Bound on Core-Guided MaxSAT Algorithms
4.2 A Polynomial Bound on MaxSAT Resolution
4.3 Integration in SAT Solvers
5 Experimental Evaluation
5.1 Experimental Setup
5.2 Experimental Results
6 Conclusions and Research Directions
References
Improving MCS Enumeration via Caching
1 Introduction
2 Preliminaries
3 MCS Extraction and Enumeration
4 Caching for MCS Enumeration
5 Experimental Results
6 Conclusions
References
Introducing Pareto Minimal Correction Subsets
1 Introduction
2 Preliminaries
2.1 Weighted Boolean Optimization
2.2 Minimal Correction Subsets
2.3 Multi-Objective Combinatorial Optimization
3 Pareto Minimal Correction Subsets
3.1 Multi-Objective Weighted Boolean Optimization
3.2 Multi and Pareto Minimal Correction Subsets
3.3 Properties of Multi and Pareto Minimal Correction Subsets
4 Virtual Machine Consolidation
5 Experimental Results
5.1 Pareto-MCSs vs GIA
5.2 Pareto-MCSs vs Evolutionary Algorithms
6 Conclusion and Future Work
References
Parallel SAT Solving
A Distributed Version of SYRUP
1 Introduction
2 Preliminaries
3 SYRUP: A Portfolio Approach
4 Parallel SAT in Distributed Architecture
4.1 Pure Message-Passing Programming Model
4.2 Partially Hybrid Programming Model
5 Fully Hybrid Programming Model
6 Experiments
6.1 Comparison of the Different Programming Models
6.2 Evaluation on SAT'16 Benchmarks
7 Conclusion and Future Work
References
PaInleSS: A Framework for Parallel SAT Solving
1 Introduction
2 About Sequential SAT Solving
3 About Parallel SAT Solving
3.1 Parallelization Strategies
3.2 Clauses Sharing
4 Architecture of the Framework
5 Implementing and Combining Existing Strategies
6 Numerical Results
7 Conclusion
References
A Propagation Rate Based Splitting Heuristic for Divide-and-Conquer Solvers
1 Introduction
2 Background on Divide-and-Conquer Solvers
3 Propagation Rate-Based Splitting Heuristic
3.1 The AMPHAROS Solver
3.2 Propagation Rate Splitting Heuristic
3.3 Worker Diversification
4 Experimental Results
4.1 Experimental Setup
4.2 Case Study 1: SAT 2016 Application Benchmark
4.3 Case Study 2: Cryptographic Hash Instances
5 Related Work
6 Conclusion
References
Quantified Boolean Formulas
Shortening QBF Proofs with Dependency Schemes
1 Introduction
2 Preliminaries
3 Static Dependency Awareness in Q-Resolution
3.1 Overview of Dependency Schemes
3.2 Dependency Schemes in Q-Resolution
4 Exponential Separation of Q(Dstd)-Res and Q(Drrs)-Res
5 Modelling Dynamic Dependency Awareness
5.1 Dynamic Dependencies in Q-Resolution
5.2 Soundness of dyn-Q(D)-Res
5.3 Motivations for dyn-Q(D)-Res
6 Static vs Dynamic Dependency Awareness in Q(D)-Res
7 Conclusions
References
A Little Blocked Literal Goes a Long Way
1 Introduction
2 Preliminaries
2.1 Resolution-Based Calculi
2.2 The QRAT Proof System Light
3 Illustration of the Simulation
4 Simulation
4.1 QRAT Derivation of the Formula '
4.2 Modification of the Long-Distance-Resolution Proof
4.3 Correctness of the Simulation
4.4 Clashes of Several Universal Literals
5 Complexity of the Simulation
6 Evaluation
7 QRAT in the Complexity Landscape
8 Conclusion
References
Dependency Learning for QBF
1 Introduction
2 Preliminaries
3 QCDCL and Q-Resolution
4 QCDCL with Dependency Learning
4.1 Examples
4.2 Soundness and Termination
5 Experiments
5.1 Solved Instances for QBF Evaluation 2016 Benchmark Sets
5.2 Learned Dependencies Compared to Dependency Relations
5.3 Dependency Learning on Hard Instances for QCDCL
6 Discussion
References
A Resolution-Style Proof System for DQBF
1 Introduction
2 Dependency Quantified Boolean Formulas
3 On Quantification over Functions
4 The Fork-Resolution Proof System
5 Example
6 Proofs of Soundness and Completeness
7 Separation from Other Proof Systems
8 Related Work
9 Conclusion
References
From DQBF to QBF by Dependency Elimination
1 Introduction
2 Foundations
3 Dependency Elimination
3.1 Selecting Dependencies to Eliminate
3.2 Symmetry Reduction
3.3 An Optimization Approach
3.4 Don't-Care Dependencies
4 Experimental Evaluation
5 Conclusion
References
Satisfiability Modulo Theories
Theory Refinement for Program Verification
1 Introduction
2 Preliminaries
3 Combination of Theories in Theory Refinement
3.1 Bit Vectors for Programs
3.2 Uninterpreted Functions for Programs
3.3 Combination of UFP and BVP
4 Counterexample-Guided Theory Refinement
5 Implementation of Theory Refinement Algorithm
5.1 The Solver for UFP
5.2 The Solver for BVP
5.3 Theory Refinement in Model Checking
6 Experimental Results
6.1 Experiments on Refinement Heuristic
7 Conclusions and Future Work
References
On Simplification of Formulas with Unconstrained Variables and Quantifiers
1 Introduction
1.1 Contribution and Structure of the Paper
2 Preliminaries
3 Unconstrained Terms in Quantifier-Free Formulas
4 Partially Constrained Terms in Quantifier-Free Formulas
5 Unconstrained Terms in Quantified Formulas
6 Partially Constrained Terms in Quantified Formulas
7 Experimental Evaluation
8 Conclusion
References
A Benders Decomposition Approach to Deciding Modular Linear Integer Arithmetic
1 Introduction
2 Preliminaries
2.1 Benders Decomposition
3 From MLIA to Equivalent LIA Constraints
3.1 Encoding Simplification
3.2 Challenges in Solving LIA Formula Directly
4 Solving MLIA Constraints
4.1 Solving Algorithms
5 Implementation and Experiments
6 Related Work
7 Conclusion
References
SAT Encodings
SAT-Based Local Improvement for Finding Tree Decompositions of Small Width
1 Introduction
2 Preliminaries
3 Local Improvement of Tree Decompositions
3.1 Local Tree Decompositions
3.2 SAT Encodings for Tree Decompositions
3.3 The Local Improvement Loop
4 Experimental Results
5 Concluding Remarks
References
A Lower Bound on CNF Encodings of the At-Most-One Constraint
1 Introduction
2 Preliminaries
2.1 Formulas in CNF
2.2 Unit Resolution
2.3 Encodings of Boolean Functions
2.4 Identification of Variables in a Unit Resolution Proof
2.5 At-Most-One and Related Functions
2.6 Basic Size Estimates
3 Reducing to Regular Form
4 A Lower Bound for General Encodings
5 A Lower Bound for 2-CNF Encodings
6 Conclusion and Further Research
References
SAT-Encodings for Special Treewidth and Pathwidth
1 Introduction
2 Preliminaries
2.1 Satisfiability and SAT-Encodings
2.2 Graphs
2.3 Special Treewidth
2.4 Weak Partitions
3 Partition-Based Approach for Special Treewidth
3.1 Characterization: Special Derivations
3.2 SAT-Encoding of a Special Derivation
4 Ordering-Based Approach for Special Treewidth
4.1 Characterization: Special Elimination Orderings
4.2 SAT-Encoding for Special Elimination Orderings
5 SAT-Encodings for Pathwidth
5.1 Partition-Based Encoding for Pathwidth
5.2 Ordering-Based Encoding for Pathwidth
6 Experiments
6.1 Results
6.2 Discussion
7 Conclusion
References
Tool Papers
MaxPre: An Extended MaxSAT Preprocessor
1 Introduction
2 Supported Techniques
2.1 Cardinality Constraints
2.2 Preprocessing
2.3 Options and Usage
2.4 API
3 Experiments
4 Conclusions
References
The GRAT Tool Chain
1 Introduction
2 The GRAT Toolchain
2.1 DRAT Certificates
2.2 GRAT Certificates
2.3 Generating GRAT Certificates
2.4 Checking GRAT Certificates
2.5 Novel Optimizations
3 Benchmarks
4 Conclusion
References
CNFgen: A Generator of Crafted Benchmarks
1 Introduction
2 Some Formula Families in CNFgen
3 Further Tools for CNF Generation and Manipulation
4 Concluding Remarks
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken