Theory and Applications of Satisfiability Testing – SAT 2020: 23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings (Lecture Notes in Computer Science (12178))

Preface
Organization
Contents
Sorting Parity Encodings by Reusing Variables
	1 Introduction
	2 Preliminaries
	3 A parity contradiction based on random orderings
	4 Evaluation
	5 Conclusion
	References
Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving
	1 Introduction
	2 Preliminaries
		2.1 Boolean Satisfiability Problem
		2.2 Literal Block Distance
		2.3 Community
	3 Measures and Intuition
		3.1 Sequential SAT Solving, Learnt Clauses and LBD
		3.2 A First Parallel Sharing Strategy
	4 Combining LBD and Community for Parallel SAT Solving
		4.1 LBD Versus Communities
		4.2 Composing LBD and Communities
		4.3 Community Based Filtering
	5 Derived Parallel Strategy and Experimental Results
		5.1 Solvers and Evaluation Protocol
		5.2 Results and Discussion
	6 Related Works
	7 Conclusion and Future Works
	References
Clause Size Reduction with all-UIP Learning
	1 Introduction
	2 Clause Learning Framework
		2.1 Some Alternate Clause Learning Schemes
		2.2 Asserting Clauses and LBD—Reasons to Prefer 1-UIP Clauses
	3 Using all-UIP Clause Learning
		3.1 Variants of stable-alluip
	4 Implementation and Experiments
	5 Conclusion
	References
Trail Saving on Backtrack
	1 Introduction
	2 Background
	3 Chronological Backtracking Effects on Search
	4 Trail Saving
		4.1 Correctness
		4.2 Enhancements
	5 Experiments and Results
	6 Conclusion
	References
Four Flavors of Entailment
	1 Introduction
	2 Preliminaries
	3 Early Pruning for Projected Model Enumeration
	4 Testing Entailment
	5 Formalization
	6 Conclusion
	References
Designing New Phase Selection Heuristics
	1 Introduction
	2 Background
		2.1 CDCL Solver
		2.2 Experimental Setup
	3 Motivation
	4 Decaying Polarity Score for Phase Selection
		4.1 Experimental Results
	5 LSIDS: A VSIDS Like Heuristic for Phase Selection
		5.1 Implementation Details
		5.2 Experimental Results
		5.3 Case Study on Cryptographic Benchmarks
	6 Conclusion
	References
On the Effect of Learned Clauses on Stochastic Local Search
	1 Introduction
	2 Preliminaries
	3 The Quality of Learned Clauses
	4 Training Experiments
	5 Experimental Evaluation
	6 Conclusion and Outlook
	References
SAT Heritage: A Community-Driven Effort for Archiving, Building and Running More Than Thousand SAT Solvers
	1 Introduction
	2 History of SAT Solvers Releases and Publications
	3 SAT Heritage Docker Images
		3.1 Architecture
		3.2 Running Solvers
		3.3 Building and Adding New Solvers
	4 Ensuring Reproducibility
	5 Conclusion
	References
Distributed Cube and Conquer with Paracooba
	1 Introduction
	2 Preliminaries and Related Work
	3 Architecture
		3.1 Static Organization
		3.2 Solving
		3.3 System Management
	4 Experiments
	5 Conclusion
	References
Reproducible Efficient Parallel SAT Solving
	1 Introduction
	2 Non-deterministic Behavior in Parallel SAT Solvers
	3 A Deterministic Parallel SAT Solver
	4 Delayed Clause Exchange
	5 Refining Periods
		5.1 Refinement Based on Literal Accesses
		5.2 Refinement Based on Block Executions
	6 Experimental Results
	7 Conclusion
	References
Improving Implementation of SAT Competitions 2017–2019 Winners
	1 Introduction
	2 Background
	3 Improving Implementation of MapleLCMDistChronoBT
		3.1 On Switching Between Branching Heuristics
		3.2 On the Importance of Separate Branching Strategies
		3.3 Improving the Handling of Core and Tier2 Learnts
	4 Experimental Evaluation
	References
On CDCL-Based Proof Systems with the Ordered Decision Strategy
	1 Introduction
	2 Preliminaries
	3 CDCL(DECISION-L, -D)=p-Ordered Resolution
	4 CDCL(FIRST-L, -D)=p General Resolution
	5 Conclusion
	References
Equivalence Between Systems Stronger Than Resolution
	1 Introduction
	2 Preliminaries
		2.1 Circular Proofs
		2.2 Weighted Proofs
		2.3 Weighted Dual-Rail Proofs
	3 Basic Facts
	4 Equivalence of Circular Resolution and MaxSAT Resolution with Extension
	5 Systems that Simulate Dual-Rail MaxSAT
	6 Conclusions
	References
Simplified and Improved Separations Between Regular and General Resolution by Lifting
	1 Introduction
	2 Preliminaries
	3 Lower Bound for Stone Formulas as a Lifting Theorem
	4 Lower Bound for Sparsely Lifted Formulas
	5 Experiments
	6 Concluding Remarks
	References
Mycielski Graphs and PR Proofs
	1 Introduction
	2 Preliminaries
	3 PR proof system
		3.1 Expressiveness of PR
	4 Proofs of Mycielski graph formulas
		4.1 Mycielski graphs
		4.2 PR proofs
	5 Experimental results
		5.1 Proof verification
		5.2 Effect of redundant clauses on CDCL performance
		5.3 Difficult extended Mycielski graph formulas
	6 Conclusion
	References
Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
	1 Introduction
	2 SAT Preliminaries
	3 MaxSAT Preliminaries
	4 Pigeon Hole Problem and Variations
	5 MaxSAT Proof Systems
		5.1 Resolution
		5.2 Split
		5.3 Virtual
	6 MaxSAT Circular Proofs
		6.1 SAT Circular Proofs
		6.2 ResSV and MaxSAT Circular Proofs
	7 Conclusions
	References
Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers
	1 Introduction
		1.1 Contributions
	2 Definitions and Preliminaries
	3 Notation for Solver Configurations Considered
		3.1 Variable Selection Schemes
		3.2 Value Selection Schemes
		3.3 Backtracking and Backjumping Schemes
	4 Separation for Drunk CDCL with and Without Restarts
		4.1 Upper Bound on Ladder Formulas via Restarts
		4.2 Lower Bound on Ladder Formulas Without Restarts
	5 CDCL+VSIDS Solvers with and Without Restarts
	6 Minor Equivalences and Separations for CDCL/DPLL Solvers with and Without Restarts
		6.1 Equivalence Between CDCL Solvers with Static Configurations with and Without Restarts
		6.2 Equivalence Between DPLL Solvers with ND Variable Selection on UNSAT Formulas
		6.3 Separation Result for Drunk DPLL Solvers
		6.4 Separation Result for CDCL Solvers with WDLS
	7 Related Work
	8 Conclusions
	References
On the Sparsity of XORs in Approximate Model Counting
	1 Background and Introduction
	2 Preliminaries and Notations
		2.1 Related Work
	3 Weakness of Guarantees Offered by Sparse XORs
	4 SparseCount2: An Efficient Algorithm for Sparse XORs
		4.1 Analysis of Correctness of SparseCount2
	5 Empirical Studies
		5.1 SparseCount vis-a-vis SparseCount2
		5.2 ApproxMC3 vis-a-vis SparseCount2
	6 Conclusion
	References
A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
	1 Introduction
	2 Preliminaries
	3 Faster Model Counting for Incidence Treewidth
	4 Discussion
	References
Abstract Cores in Implicit Hitting Set MaxSat Solving
	1 Introduction
	2 Preliminaries
	3 Implicit Hitting Set Based MaxSat Solving
	4 Abstract Cores
	5 Abstract Cores in IHS MaxSat Solving
	6 Experimental Evaluation
	7 Conclusion
	References
MaxSAT Resolution and Subcube Sums
	1 Introduction
	2 Defining the Proof Systems
	3 MaxRes, MaxResW, and TreeRes
	4 The SubCubeSums Proof System
		4.1 Res Does Not Simulate SubCubeSums
		4.2 A Lower Bound for SubCubeSums
		4.3 Lifting Degree Lower Bounds to Size
	5 Discussion
	References
A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
	1 Introduction
	2 Preliminaries
	3 Restriction to Threshold Models of PB-Constraints
	4 Reduction to Covering Maximal Matchings of Kn,n
	5 Proof of Theorem 1
	References
On Weakening Strategies for PB Solvers
	1 Introduction
	2 Pseudo-Boolean Solving
		2.1 Generalized Resolution Based Solvers
		2.2 Division Based Solvers
	3 Weakening Strategies
		3.1 Weakening Ineffective Literals for Shorter Constraints
		3.2 Partial Weakening for Stronger Constraints
		3.3 Towards a Tradeoff
	4 Experimental Results
	5 Conclusion
	References
Reasoning About Strong Inconsistency in ASP
	1 Introduction
	2 Preliminaries
	3 Reasoning About Strongly Inconsistent ASP Programs
		3.1 Strong Inconsistency and MSMP
		3.2 Computing Minimal Explanations and Corrections
	4 Preliminary Results
	5 Conclusions
	References
Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology
	1 Introduction
	2 Background
	3 Towards Nested Dynamic Programming
		3.1 Essentials for Nested Dynamic Programming
		3.2 Hybrid Solving Based on Nested DP
		3.3 Generalizing Nested DP to Other Formalisms
	4 Implementation and Preliminary Results
	5 Conclusion
	References
Reducing Bit-Vector Polynomials to SAT Using Gröbner Bases
	1 Introduction
	2 Bit-Sequence Propagation in a Nutshell
		2.1 Solving Using 0/1 Truth Values
		2.2 Solving Using Symbolic Truth Values
		2.3 Solving Using SAT
	3 Theoretical Underpinnings
		3.1 Modulo Integers
		3.2 Polynomials and Ideals
		3.3 Leading Terms
		3.4 Reduction
		3.5 Gröbner Bases
		3.6 Buchberger's Algorithm
		3.7 Modified Buchberger's Algorithm
		3.8 Encoding Pseudo-Boolean Constraints
	4 Experimental Results
	5 Related Work
	6 Concluding Discussion
	References
Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions
	1 Introduction
	2 Preliminaries
	3 Formula Reduction and Model Extension
		3.1 Reduction of Bit-Widths in Formulas
		3.2 Extending Bit-Widths of Symbolic Models
	4 Algorithm
		4.1 Checking Satisfiability Using Reductions and Extensions
		4.2 Dual Algorithm
		4.3 Combined Algorithm
	5 Implementation
		5.1 Model-Generating Solver
		5.2 Portfolio Solver
	6 Experimental Evaluation
		6.1 Boolector
		6.2 CVC4 and Q3B
	7 Conclusions
	References
Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths
	1 Introduction
	2 Preliminaries
	3 DQBF Dependency Schemes and Full Exhibition
	4 Parametrising DQBF Calculi by Dependency Schemes
	5 The Tautology-Free Dependency Scheme
	6 Proof Complexity of Exp+Res(D)
	7 Tautology-Free Dependencies for QBF
	8 Conclusions
	References
Short Q-Resolution Proofs with Homomorphisms
	1 Introduction
	2 Preliminaries
	3 Dependency Schemes and Q(D)-Resolution
	4 Homomorphisms
	5 The Homomorphism Rule
	6 Lifting Lower Bounds from Q(Drrs)-Resolution to LH(Drrs)
	7 Separating LH(Drrs) from LH
	8 Concluding Remarks
	References
Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness
	1 Introduction
	2 Preliminaries
	3 Strategies
	4 Local Soundness
		4.1 Combine
	5 Implementing Strategies Using Circuits
		5.1 Circuit Construction
		5.2 Correctness and Running Time
	6 Circuit Extraction for QParity
	7 Related Work
	8 Conclusion
	References
Positional Games and QBF: The Corrective Encoding
	1 Introduction
	2 Preliminaries on QBF and Positional Games
	3 The Corrective Encoding
		3.1 Description
		3.2 Size of the COR Encoding
	4 Instances
		4.1 Harary's Tic-Tac-Toe and GTTT(p, q)
		4.2 Hex
		4.3 Challenges
	5 Analysis
		5.1 Setup of Experiments
		5.2 Experimental Comparison of Our New Encoding to the DYS
		5.3 Solving Increasingly Realistic Games
	6 Comparison to Related Encodings
	7 Conclusion and Future Work
	References
Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles
	1 Introduction
	2 Preliminaries
	3 Verifying Strong USPs
		3.1 Brute Force
		3.2 Strong USP Verification to 3D Matching
		3.3 3D Matching to Satisfiability
		3.4 3D Matching to Integer Programming
		3.5 Heuristics
		3.6 Hybrid Algorithm
	4 Searching for Strong USPs
	5 Experimental Results
		5.1 New Bounds on the Size of Strong USPs
		5.2 Algorithm Performance
	6 Conclusions
	References
Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits
	1 Introduction
	2 Designing Approximate Circuits
	3 SAT-based Circuit Approximation
		3.1 A Monolithic Approach
		3.2 Sub-circuit Approximation
		3.3 Evolutionary Approximation with StS-Based Optimisation
	4 Experimental Results
		4.1 Performance on Small Circuits
		4.2 Performance on Complex Circuits
	References
SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing
	1 Introduction
	2 Encoding Fragmented Hamiltonian Path Constraints for WAAM
	3 Solver and Simulator Engineering
	4 Experiments
	5 Related Work
	6 Conclusion and Outlook
	References
SAT-Based Encodings for Optimal Decision Trees with Explicit Paths
	1 Introduction
	2 Preliminaries
		2.1 Training Data
	3 SAT-Based Optimization of Decision Trees
		3.1 Path-Based Encoding
		3.2 Path Encoding Optimizations
	4 Search-Space Splitting by Topologies
		4.1 Topology Enumeration
	5 Experimental Evaluation
	6 Related Work
	7 Conclusions and Future Work
	References
Incremental Encoding of Pseudo-Boolean Goal Functions Based on Comparator Networks
	1 Introduction
		1.1 Related Work
		1.2 Our Contribution
		1.3 Structure of the Paper
	2 Background
		2.1 4-Way Merge Selection Network
		2.2 Mixed Radix Base Technique
	3 The Incremental Algorithm
	4 Experimental Evaluation
	5 Conclusions
	References
Author Index