Theory and Applications of Satisfiability Testing – SAT 2021

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