Theory and Applications of Satisfiability Testing - SAT 2018

Name: Theory and Applications of Satisfiability Testing - SAT 2018 | 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings

Olaf Beyersdorff Christoph M. Wintersteiger(Herausgeber*in)

Springer (Verlag)

Erschienen am 27. Juni 2018

XIX, 452 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-94144-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

Intro
Preface
Organization
Invited Talks
Computable Short Proofs??
Modelling SAT
Contents
Invited Talk
Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
1 Introduction
2 Notions and Problem Definition
3 Overview of Solution Methods
3.1 Incomplete Approximations
3.2 Search-Based Solution
3.3 Abstraction-Based Solution
3.4 Fork Resolution
3.5 Basic Approach Using Universal Expansion
3.6 Transformation into QBF
3.7 The Role of Preprocessing
3.8 Computing Skolem Functions
4 Applications
4.1 Partial Equivalence Checking for Combinational Circuits
4.2 Controller Synthesis
4.3 Realizability Checking for Sequential Circuits
5 Conclusion and Future Challenges
References
Maximum Satisfiability
Approximately Propagation Complete and Conflict Propagating Constraint Encodings
1 Introduction
1.1 Related Work
2 Preliminaries
3 Approximate Propagation Completeness and Conflict Propagation
4 Computing Minimal Approximately Optimal Encodings
4.1 Ensuring Encoding Correctness
4.2 Encoding Approximate Propagation Completeness
4.3 Encoding Approximate Conflict Propagation
4.4 MaxSAT Solving
5 Experiments
5.1 Case Study: Integer Factoring
6 Conclusion
References
Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
1 Introduction
2 Related Work
3 Preliminaries
3.1 MaxSAT
3.2 Totalizer Network
3.3 Polynomial Watchdog Encoding Scheme
4 Dynamic PW Encoding and GPW Algorithm
4.1 Dynamic PW Encoding
4.2 Dynamic GPW Algorithm
5 PW Encoding Optimizations
5.1 Caching of Adder
5.2 Cone-of-Influence Encoding
5.3 Exact Bound Encoding
6 Experimental Results
7 Conclusions
References
Solving MaxSAT with Bit-Vector Optimization
1 Introduction
2 Preliminaries
2.1 SAT Solving
2.2 State-of-the-Art Unweighted MaxSAT Solvers
2.3 Totalizer Encoding
3 Responsiveness and Incrementality
3.1 Responsiveness
3.2 Incrementality
4 Optimization Modulo Bit-Vectors (OBV) Algorithms
5 Mrs. Beaver: An Unweighted MaxSAT Algorithm
5.1 Mrs. Beaver and Linear Search
5.2 Mrs. Beaver-Inc: The Incomplete Preprocessor
5.3 Responsiveness
5.4 Incrementality
6 Applying Mrs. Beaver to Solve BMO
7 Experimental Results
7.1 Unweighted MaxSAT: MaxSAT Evaluation 2017
7.2 Industrial Instances
8 Conclusion
References
Conflict Driven Clause Learning
Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
1 Introduction
1.1 Our Investigations and Conclusions
1.2 Organization of this Paper
2 Experimental Set-up
3 Description of Benchmarks
4 Experimental Evaluation
4.1 Pseudo-Boolean Solvers and Boolean Reasoning
4.2 Pseudo-Boolean Solvers and Linear Programming
4.3 Pseudo-Boolean Solvers Versus CDCL and MIP
5 Concluding Remarks
References
Machine Learning-Based Restart Policy for CDCL SAT Solvers
1 Introduction
2 Background
3 Prior Hypotheses on ``The Power of Restarts''
4 ``Restarts Enable Learning Better Clauses'' Hypothesis
4.1 Confirming the ``Compacting the Assignment Stack'' Claim
4.2 Learning Better Clauses
4.3 Solving Instances Faster
4.4 Clause Length
4.5 Low LBD in Core Proof
4.6 New Restart Policy
5 A Machine Learning-Based Restart Policy
5.1 LBD Percentile
5.2 LBD of Next Clause
6 Experimental Evaluation
7 Related Work
8 Conclusion
References
Chronological Backtracking
1 Introduction
2 Chronological Backtracking
2.1 Algorithm
2.2 Combining CB and NCB
3 Experimental Results
3.1 SAT Competition
3.2 MaxSAT Evaluation
4 Conclusion
References
Centrality-Based Improvements to CDCL Heuristics
1 Introduction
2 Centrality Computation
3 Modified Decision and Deletion Heuristics
4 Performance Evaluation
5 Performance Details
6 Discussion
References
Model Counting
Fast Sampling of Perfectly Uniform Satisfying Assignments
1 Introduction
1.1 Model Counting
2 Related Work
3 Caching and Component Decomposition
4 How to Get One Uniform Sample
5 How to Get Many Uniform Samples at Once
6 Reservoir Sampling
6.1 Reservoir Sampling in the Context of Model Caching
7 A Complete Algorithm
8 Evaluation and Experiments
8.1 Uniformity Verification
8.2 Running Time
8.3 Comparison
References
Fast and Flexible Probabilistic Model Counting
1 Introduction
2 Previous Work
2.1 Independent Support Sets
3 Our Results
4 First a Lower Bound
5 Then an Upper Bound
6 Finally a (1)|S| Approximation
7 Homogeneous Distributions
8 Low Density Parity Check Codes
9 Bounding B in Practice
10 Experiments
11 Conclusions
References
Exploiting Treewidth for Projected Model Counting and Its Limits
1 Introduction
2 Preliminaries
3 Dynamic Programming on TDs for SAT
4 Counting Projected Models by Dynamic Programming
5 Runtime (Upper and Lower Bounds)
6 Correctness of the Algorithm
7 Conclusions
References
Quantified Boolean Formulae
Circuit-Based Search Space Pruning in QBF
1 Introduction
2 Preliminaries
3 CQESTO Algorithm
3.1 Projection (proj)
3.2 SAT Calls
3.3 Backtracking
3.4 Discussion
3.5 Correctness and Termination
4 Experimental Evaluation
5 Summary and Future Work
References
Symmetries of Quantified Boolean Formulas
1 Introduction
2 Quantified Boolean Formulas
3 Groups and Group Actions
4 Syntactic Symmetries
5 Semantic Symmetries
6 Existential Symmetry Breakers
7 Universal Symmetry Breakers
8 Construction of Symmetry Breakers
References
Local Soundness for QBF Calculi
1 Introduction
2 Preliminaries
3 Policies and Strategies
4 Operations on Strategies
5 Local Soundness of Expansion-Derived Calculi
5.1 Local Soundness for IR-calc
5.2 What Needs to Be Done Differently for IRM-calc?
6 Local Soundness for CDCL-Derived Calculi
7 Winning Strategies Are Worst-Case Exponential for IRM-calc Proofs
8 Conclusion and Future Work
References
QBF as an Alternative to Courcelle's Theorem
1 Introduction
2 Preliminaries
2.1 Treewidth
2.2 CNF Formulas
2.3 From Primal to Incidence Treewidth
3 2-QBF
4 Abstract Argumentation
5 Abduction
5.1 Adding -Preferences
6 Circumscription
7 Minimal Unsatisfiable Subsets
8 Conclusion
References
Polynomial-Time Validation of QCDCL Certificates
1 Introduction
2 Preliminaries
3 Validation of Certificates
4 RUP Proofs from Ordinary Q-Resolution
5 RUP Proofs from Long-Distance Q-Resolution
6 True Formulas
7 Experiments
8 Concluding Remarks
References
Theory
Sharpness of the Satisfiability Threshold for Non-uniform Random k-SAT
1 Introduction
2 Preliminaries
3 Sharpness of the Threshold
3.1 Non-uniform Sharpness
3.2 Influence and Bourgain's Sharp Threshold Theorem
3.3 Proof of Sharpness for Non-uniform Random k-SAT
3.4 Relation to the Clause-Drawing Model
3.5 Example Application of the Theorem
4 Discussion of the Results
References
In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
1 Introduction
2 Proof Systems for Pseudo-Boolean SAT Solving
3 Relations Between Subsystems of Cutting Planes
4 Tricky Formulas Based on Easy NP Instances
5 Concluding Remarks
References
Cops-Robber Games and the Resolution of Tseitin Formulas
1 Introduction
2 Preliminaries
2.1 Tseitin Formulas
3 A Game Characterization of Resolution Variable Space
4 Cops and Robber Games
4.1 The Cops-Robber Game Characterizes Width on Tseitin Formulas
4.2 An Invisible Robber Characterizes Variable Space on Tseitin Formulas
4.3 A Game Characterization of Depth on Tseitin Formulas
5 Regular Resolution and Monotone Games
5.1 The Visible Robber
5.2 The Invisible Robber
6 New Relations Between Complexity Measures for Tseitin Formulas
7 Conclusions and Open Problems
References
Minimally Unsatisfiable Sets
Minimal Unsatisfiability and Minimal Strongly Connected Digraphs
1 Introduction
2 Preliminaries
3 Review on Minimal Unsatisfiability (MU)
4 MU with Full Monotone Clauses (FM)
5 FM with Binary Clauses (DFM)
6 Deficiency 2 Revisited
7 MU for 2-CNF
8 Conclusion
References
Finding All Minimal Safe Inductive Sets
1 Introduction
2 Preliminaries
2.1 Basic Definitions
2.2 MUSes, MCSes and Hitting Set Duality
2.3 Safe Inductive Invariants and MSIS
2.4 Monotonicity and MSMP
3 Problem Formulation: AllMSIS and SMSIS
4 MSIS Enumeration Using Hitting Set Duality
4.1 Inductive Support and Collapse Sets
4.2 CAMUS for MSIS Extraction
4.3 The CAMSIS Algorithm
5 MARCO and MSIS Extraction
5.1 MARCO Algorithm for MSMP
5.2 A Monotone Version of MSIS Enumeration
6 Complexity of MSIS and MUS
7 Experimental Results
8 Conclusion and Future Work
References
Satisfiability Modulo Theories
Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition
1 Introduction
2 Background: Automatic Generation of Simulation Proof
3 Running Example
4 Invariant Sketches and the Use of Counter-Examples
5 Efficient Discharge of Proof Obligations
6 Experiments
7 Related Work and Conclusions
References
Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
1 Introduction
2 Background
3 Implementing Incremental Linearization in a Lazy SMT Solver
4 Experimental Analysis
5 Conclusions
References
Tools and Applications
XOR-Satisfiability Set Membership Filters
1 Introduction
2 XORSAT Filters
2.1 XORSAT
2.2 XORSAT Filter Construction
2.3 False Positive Rate, Query Time, and Storing Multiple Solutions
2.4 Dictionaries
2.5 Blocked XORSAT Filters
3 Filter Efficiency
4 XORSAT Filter Parameters
5 Detailed Example
5.1 Building the Filter
5.2 Querying the Filter
6 Experimental Results
7 Conclusions and Future Work
References
ALIAS: A Modular Tool for Finding Backdoors for SAT
1 Introduction
2 On Backdoors to SAT
3 The ALIAS tool
4 Experimental Results
5 Conclusion
References
PySAT: A Python Toolkit for Prototyping with SAT Oracles
1 Introduction
2 Preliminaries
3 PySAT Toolkit Description
3.1 PySAT Design
3.2 Provided Interface
3.3 Installation
4 Usage Example
5 Experimenting with MaxSAT
6 Related Work
7 Conclusions
References
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
1 Introduction
2 Problem Description
3 The Generative Neural Network Approach
4 The Constraint-Based Approach
4.1 Approximation of a PDE Solver
4.2 Geometric and Process Constraints
5 Experiments
6 Related Work
7 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken