Theory and applications of satisfiability testing -- SAT 2020 : 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings / edited by Luca Pulina, Martina Seidl.

International conference proceedings.

Print version record.

"Originally planned to be held in Alghero, Italy, it was not possible to have an onsite event due to of COVID-19. Instead SAT went online and was organized as a virtual event."

Intro -- 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

Includes author index.

This book constitutes the proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing, SAT 2020, which was planned to take place in Alghero, Italy, during July 5-9, 2020. Due to the coronavirus COVID-19 pandemic, the conference was held virtually. The 25 full, 9 short, and 2 tool papers presented in this volume were carefully reviewed and selected from 69 submissions. They deal with SAT interpreted in a broad sense, including theoretical advances (such as exact algorithms, proof complexity, and other complexity issues), practical search algorithms, knowledge compilation, implementation-level details of SAT solvers and SAT-based systems, problem encodings and reformulations, applications (including both novel application domains and improvements to existing approaches), as well as case studies and reports on findings based on rigorous experimentation.