| Description |
1 online resource (549 pages) |
| Series |
Lecture Notes in Computer Science ; 12178 |
|
LNCS Sublibrary: SL 1, Theoretical computer science and general issues |
|
Lecture notes in computer science ; 12178.
|
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
|
| Contents |
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 |
| Summary |
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 |
| Notes |
International conference proceedings |
|
"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." |
|
Reproducible Efficient Parallel SAT Solving |
|
Includes author index |
|
Print version record |
| Subject |
Computer algorithms -- Congresses
|
|
Computer software -- Verification -- Congresses
|
|
Computer science.
|
|
Computers -- Computer Science.
|
|
Computer algorithms
|
|
Computer software -- Verification
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Pulina, Luca
|
|
Seidl, Martina.
|
| ISBN |
9783030518257 |
|
3030518256 |
|
