Theory and applications of satisfiability testing -- SAT 2020 : 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings /: 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings. (2020)

• Record Type: Book
• Other Titles: SAT 2020
• Further Information: Note: Edited by Luca Pulina, Martina Seidl.
• Other Names: Pulina, Luca; Seidl, Martina; SAT (Conference), 23rd
• 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
• Publisher Details: Cham : Springer
• Publication Date: 2020
• Extent: 1 online resource (549 p.)
• Subjects: 005.1; Computer algorithms -- Congresses; Computer software -- Verification -- Congresses; Computer science; Computers -- Computer Science; Computer algorithms; Computer software -- Verification; Electronic books; Electronic books; Conference papers and proceedings
• Languages: English
• ISBNs: 9783030518257; 3030518256
• Related ISBNs: 9783030518240
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.