Theory and Applications of Satisfiability Testing – SAT 2021

Description

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