Theory and Applications of Satisfiability Testing - SAT 2021

Name: Theory and Applications of Satisfiability Testing - SAT 2021 | 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings
Brand: Springer
Price: 106.99 EUR
Availability: OnlineOnly

24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings

Chu-Min Li Felip Manyà(Herausgeber*in)

Springer (Verlag)

Erschienen am 1. Juli 2021

XI, 564 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-030-80223-3 (ISBN)

106,99 €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
OptiLog: A Framework for SAT-based Systems
1 Introduction
2 OptiLog Framework Architecture
2.1 Formula Module
2.2 SAT Solver Module
2.3 PB Encoder Module
2.4 Automatic Configuration (AC) Module
2.5 Adding SAT Solvers to OptiLog Through iSAT Interface
3 Example: The Linear MaxSAT Algorithm with OptiLog
4 Conclusions and Future Work
References
PyDGGA: Distributed GGA for Automatic Configuration
1 Introduction
2 Preliminaries
3 PyDGGA
3.1 Distributed Architecture
3.2 Simulation
3.3 Scheduling and Canceling
3.4 Instance Selection
3.5 Elite Mini-Tournament
3.6 Other Tool Enhancements
4 Using PyDGGA
5 Experiments with SAT
6 Conclusions and Future Work
References
QBFFam: A Tool for Generating QBF Families from Proof Complexity
1 Introduction
2 Related Work
3 Formula Families
4 Case Study
5 Conclusion
References
Davis and Putnam Meet Henkin: Solving DQBF with Resolution
1 Introduction
2 Preliminaries
3 Davis-Putnam Resolution for H-Form DQBF
3.1 Strategy Operations
3.2 Definition of the Construction
3.3 Correctness and Completeness
3.4 Representing Strategies
4 NEXP-completeness of CNF H-Form DQBF
5 Conclusion
References
Lower Bounds for QCDCL via Formula Gauge
1 Introduction
2 Preliminaries
3 QCDCL as a Formal Proof System
4 Quasi Level-Ordered Proofs
5 A Lower Bound Technique via Gauge
6 Applications of the Lower Bound Technique
7 Conclusion
References
Deep Cooperation of CDCL and Local Search for SAT
1 Introduction
2 Preliminaries
2.1 Preliminary Definitions and Notations
2.2 CDCL Solvers
2.3 Local Search Solvers
2.4 Experiment Preliminaries
3 Exploring Promising Branches by Local Search
4 Phase Resetting with Local Search Assignments
5 Branching with Conflict Frequency in Local Search
6 Experiments
7 Related Works
8 Conclusions
References
Hash-Based Preprocessing and Inprocessing Techniques in SAT Solvers
1 Introduction
2 Preliminaries
3 Hash-Based Methods
4 Probabilistic Analysis
5 Evaluation
6 Conclusions
References
Hardness and Optimality in QBF Proof Systems Modulo NP
1 Introduction
1.1 Organisation
2 Preliminaries
2.1 Proof Complexity
2.2 Propositional Logic
2.3 Quantified Boolean Formulas
3 Simulations with Extension Variables
4 Extended Q-Res Modulo NP
5 Weaker QBF Systems
6 Conclusion
References
Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
1 Introduction
2 Preliminaries
3 Reduction from Unsatisfiable to Satisfiable Formulas
3.1 Well-Structured Branching Programs for SearchVertex(G,c)
3.2 Constructing DNNF from Well-Structured Branching Programs
4 Adversarial Rectangle Bounds
5 Splitting Parity Constraints
5.1 Rectangles Induce Sub-constraints for Tseitin-Formulas
5.2 Vertex Splitting and Sub-constraints for Tseitin-Formulas
5.3 Vertex Splitting in 3-Connected Graphs
6 DNNF Lower Bounds for Tseitin-Formulas
6.1 Reduction from Connected to 3-Connected Graphs
6.2 Proof of the DNNF Lower Bound and of the Main Result
7 Conclusion
References
Weighted Model Counting Without Parameter Variables
1 Introduction
2 Weighted Model Counting
2.1 Bayesian Network Encodings
3 Pseudo-Boolean Functions
4 Pseudo-Boolean Projection
4.1 From WMC to PBP
4.2 Correctness Proofs
5 Experimental Evaluation
5.1 Setup
5.2 Results
6 Conclusion
References
ProCount: Weighted Projected Model Counting with Graded Project-Join Trees
1 Introduction
2 Preliminaries
3 Using Project-Join Trees for Projected Model Counting
3.1 Project-Join Trees for Model Counting
3.2 Adaptations for Projected Model Counting
4 Building Graded Project-Join Trees
4.1 Reducing Free Project-Join Trees to Ungraded Project-Join Trees
4.2 Reducing Graded Project-Join Trees to Free Project-Join Trees
5 Experimental Evaluation
5.1 Experiment 1: Comparing Planners
5.2 Experiment 2: Comparing Execution Heuristics
5.3 Experiment 3: Comparing Weighted Projected Model Counters
6 Related Work
7 Discussion
References
Efficient All-UIP Learned Clause Minimization
1 Introduction
2 Minimization
3 Shrinking
4 Minimizing and Shrinking
5 Experiments
6 Conclusion
References
Solving Non-uniform Planted and Filtered Random SAT Formulas Greedily
1 Introduction
1.1 Planted k-SAT
2 Non-uniform Planted k-SAT
3 The Greedy Algorithm on Non-uniform Planted k-SAT
4 Relationship Between Planted and Filtered Instances
5 Experiments
6 Conclusions
References
MCP: Capturing Big Data by Satisfiability (Tool Description)
1 Introduction and Related Work
2 Preliminaries
3 Core of the MCP System
3.1 Strategies for Computing the Closure
3.2 Minimal Section
3.3 Effective Learning of Formulas
3.4 First Postprocessing: Redundancy Elimination
3.5 Second Postprocessing: Set Cover
3.6 Input Format and Action Possibilities
3.7 Parallelization
3.8 Invocation
4 Prequel and Sequel Modules
4.1 Data Binarization
4.2 Formula Evaluation
5 System Distribution and Examples
6 Concluding Remarks
References
Chinese Remainder Encoding for Hamiltonian Cycles
1 Introduction
2 Preliminaries
3 Encodings
3.1 Degree Constraint
3.2 Binary Adder
3.3 Linear-Feedback Shift Register
4 Chinese Remainder Encoding
5 Results
6 Conclusions
References
Efficient SAT-Based Minimal Model Generation Methods for Modal Logic S5
1 Introduction
2 Preliminaries
2.1 Syntax and Semantics
2.2 Satisfiability
2.3 The Number of Possible Worlds
2.4 S5-NF
2.5 Complexity Analysis
3 Methodology
3.1 Querying SAT Iteratively
3.2 Partial MaxSAT Model
4 Improved Methods
4.1 SIF Strategy
4.2 Improved S5-K-SAT Model
4.3 Improved PMS Model
4.4 The Benefit of SIF
5 Comparison
6 Experimental Evaluation
6.1 Benchmarks
6.2 Environment
6.3 Experimental Results
7 Why Is a Minimal Model Small?
8 Conclusion
References
DiMo - Discrete Modelling Using Propositional Logic
1 Propositional Logic in Formal Modelling
2 The DiMo Language and Tool
3 Conclusion
References
SAT-Based Rigorous Explanations for Decision Lists
1 Introduction
2 Preliminaries
2.1 Propositional Satisfiability
2.2 Classification Problems, Decision Lists, and Explanations
3 Explaining Decision Lists
3.1 DL Explainability
3.2 Explaining Arbitrary DLs with SAT
4 Experimental Results
5 Conclusions
References
Investigating the Existence of Costas Latin Squares via Satisfiability Testing
1 Introduction
2 Preliminaries
3 Modeling
4 Improvements in Modeling
5 New Results and Experimental Evaluation
5.1 New Results
5.2 Experimental Evaluation
6 Conclusion
References
Assessing Progress in SAT Solvers Through the Lens of Incremental SAT
1 Introduction
2 Preliminaries
3 Motivation
4 Setup and Its Rationale
4.1 SAT Competition Main Track Benchmarks
4.2 SAT Competition Incremental Track Benchmarks
5 Experimental Evidence
5.1 RC2 MaxSAT and Mostly Unsatisfiable Calls
5.2 LSU MaxSAT and Mostly Satisfiable Calls
5.3 MUS Extraction and Mixed Oracle Calls
5.4 Final Remarks
6 Conclusions
References
Projection Heuristics for Binary Branchings Between Sum and Product
1 Introduction
2 Branching Tuples and Distances
2.1 Trees and Distances
2.2 The Tau-Function and Bounds on Tree Sizes
3 The Canonical Order of Branching Tuples
4 Analysis and Numerics of Binary Tau
5 On Binary Projections
5.1 On Means in General
5.2 Comparing the Various Means by Their Kernels
6 Summary and Outlook
References
On Dedicated CDCL Strategies for PB Solvers
1 Introduction
2 Preliminaries
3 Branching Heuristics
3.1 VSIDS in PB Solvers
3.2 Towards Better VSIDS for PB Solvers
4 Learned Constraint Deletion
4.1 Size-Based Measures
4.2 LBD-Based Measures
4.3 Deleting PB Constraints
5 Restarts
6 Experimental Results
6.1 Solver Configurations
6.2 Decision Problems
6.3 Optimization Problems
6.4 Discussion
7 Conclusion
References
Efficient Local Search for Pseudo Boolean Optimization
1 Introduction
2 Preliminaries
3 Main Ideas
3.1 Constraint Weighting
3.2 Scoring Function
4 A Local Search Algorithm for PBO
5 Experiments
5.1 Minimum-Width Confidence Band Problem
5.2 Wireless Sensor Network Optimization Problem
5.3 Seating Arrangements Problem
5.4 Results on Pseudo-Boolean Competition Benchmark
6 Conclusions and Future Work
References
Scheduling Reach Mahjong Tournaments Using Pseudoboolean Constraints
1 Problem Description
1.1 Constraints
2 Problem Encoding
2.1 Monolithic Constraint Encoding
2.2 Wind Balancing Constraint Encoding
3 Evaluation
4 Related Work and Conclusions
A Benchmarks for Large Instances
References
On the Hierarchical Community Structure of Practical Boolean Formulas
1 Introduction
2 Preliminaries
3 Research Methodology
4 Hierarchical Community Structure
5 Empirical Results
5.1 HCS-based Category Classification of Boolean Formulas
5.2 HCS-based Empirical Hardness Model
5.3 HCS Parameter Value Ranges for Industrial/Random Instances
5.4 Scaling Experiments with HCS Parameters
5.5 Discussion of Empirical Results
6 Theoretical Results
7 Related Work
8 Conclusions and Future Work
References
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving
1 Introduction
2 Design
2.1 Interface
2.2 Additional Features
3 Example
4 Related Work
5 Evaluation
6 Conclusion
References
The MergeSat Solver
1 Introduction
2 Recent SAT Competitions
2.1 Benchmark Selection
2.2 Winning Solvers and Top Solvers
2.3 SAT Solver Evolution
3 Development Model of MergeSat
3.1 Supported Features and Selected Techniques
3.2 Incorporating Patches
3.3 Provided Implementation Improvements
3.4 Development Environment
4 Tool Comparison
5 Conclusion and Future Work
References
Proof Complexity of Symbolic QBF Reasoning
1 Introduction
2 Preliminaries
2.1 Propositional Logic and Quantified Boolean Formulas
2.2 Graphs and Pathwidth of Formulas
2.3 OBDD
2.4 Combinatorial Rectangles
3 Symbolic QBF Proof Systems
4 Relation to Other Proof Systems
5 A Lower Bound on OBDD Refutations
5.1 From OBDD Proofs to Rectangle Decision Lists
5.2 From Rectangle Decision Lists to Communication Complexity
5.3 A Function with only Small Monochromatic Rectangles
5.4 Putting It All Together
6 Conclusion
References
XOR Local Search for Boolean Brent Equations
1 Introduction
2 XOR Constraints
3 Extracting XORs
4 Implementation
5 Experiments
6 Conclusion
References
A Fast Algorithm for SAT in Terms of Formula Length
1 Introduction
2 Preliminaries
3 Branch-and-Search and Measure-and-Conquer
4 The Algorithm
4.1 Reduction Rules
4.2 Branching Rules and the Algorithm
5 Framework of the Analysis
5.1 Some Lower Bounds
6 Step Analysis
6.1 Step 2
6.2 Step 3
6.3 Step 4
6.4 Step 5
6.5 Step 6
6.6 Step 7
6.7 Step 8
6.8 Step 9
6.9 Step 10
6.10 Step 11
7 The Final Result
8 Concluding Remarks
References
MedleySolver: Online SMT Algorithm Selection
1 Introduction and Motivation
2 Related Work
3 Problem Statement and Approach Overview
4 Dynamic Solver Selection
4.1 Thompson Sampling
4.2 Features for Contextual Approaches
4.3 k-Nearest-Neighbor
5 Runtime Prediction
6 Empirical Evaluation
6.1 RQ1: Comparison with Individual Solvers
6.2 RQ2: Comparison with State-of-the-Art
6.3 RQ3: Impact of Individual Components
6.4 Threats to Validity
7 Conclusions and Future Work
References
Leveraging GPUs for Effective Clause Sharing in Parallel SAT Solving
1 Introduction
2 Definitions
3 Related Work
4 GPUShareSat: GPU-Based Parallel SAT Solving
4.1 Usefulness of Clauses
4.2 Assignment Trigger Check
4.3 Pooling-Based Efficient Trigger Check
4.4 GPU Implementation
5 Evaluation
6 Conclusion
References
A Proof Builder for Max-SAT
1 Introduction
2 Preliminaries
2.1 Definitions and Notations
2.2 Resolution Refutations in SAT
2.3 Proofs for Max-SAT
3 Related Work
4 MS-Builder
5 MS-Checker
6 Experiments
7 Conclusion
References
Certified DQBF Solving by Definition Extraction
1 Introduction
2 Preliminaries
3 Solving DQBF by Definition Extraction
3.1 A Two-Phase Algorithm
3.2 Combining Definition Extraction with CEGIS
4 Experiments
4.1 Performance on Standard Benchmark Sets
4.2 Distribution of Defined Existential Variables
4.3 Solution Validation
5 Related Work
6 Conclusion
References
Scalable SAT Solving in the Cloud
1 Introduction
2 Related Work
3 Malleable Environment
4 The Mallob SAT Engine
4.1 Succinct Clause Exchange
4.2 Malleable Solver Backend
4.3 Performance Improvements
5 Evaluation
5.1 Selection of Benchmarks
5.2 Standalone SAT Solving Performance
5.3 Malleable Job Scheduling
6 Conclusion
References
DQBDD: An Efficient BDD-Based DQBF Solver
1 Introduction
2 Approach
3 Implementation and Usage
4 Experimental Comparison
5 Conclusion
References
Logical Cryptanalysis with WDSat
1 Introduction
2 Background
3 Implementation Details
3.1 Three Reasoning Modules
4 Applications in Cryptanalysis
5 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken