| Conference |
SAT (Conference) (23rd : 2020 : Online)
|
| 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.
|
| Subject |
Computer algorithms -- Congresses.
|
|
Computer software -- Verification -- Congresses.
|
| Alt Name |
Pulina, Luca.
|
|
Seidl, Martina.
|
| Add Title |
SAT 2020 |
| Description |
1 online resource (549 pages). |
| Note |
International conference proceedings. |
|
Description based upon print version of 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." |
|
Reproducible Efficient Parallel SAT Solving |
|
Includes author index. |
| 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 |
| ISBN |
9783030518257 (electronic bk.) |
|
3030518256 (electronic bk.) |
|
9783030518240 |
| OCLC # |
1164502217 |
| Additional Format |
Print version: Pulina, Luca Theory and Applications of Satisfiability Testing - SAT 2020 : 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings Cham : Springer International Publishing AG,c2020 9783030518240. |
|
Search 
Search 
Previous Item
Permanent Link
