Linked e-resources
Details
Table of Contents
Intro; Foreword; Preface; Contents; List of Contributors; Part I Theory and Algorithms; 1 Parallel Satisfiability; 1.1 Introduction; 1.2 Preliminaries; 1.2.1 Satisfiability (SAT); 1.2.2 Local Search Algorithms for SAT; 1.2.3 The DPLL Algorithm; 1.2.4 Resolution Refutation; 1.2.5 The CDCL Algorithm; 1.2.6 Parallel Computing Architectures; 1.2.7 Measuring Speedups; 1.3 Divide-and-Conquer Approaches; 1.3.1 Problem Decomposition and Load Balancing; 1.3.2 Implementations of Search-Space-Splitting Solvers; 1.3.3 Search Space Splitting in CDCL; 1.3.4 Cube and Conquer
1.4 Parallel Portfolios
Diversify and Conquer!1.4.1 Virtual Best Solver; 1.4.2 Pure Portfolio Solvers and Diversification; 1.4.3 Clause-Sharing Portfolios; 1.4.4 Impact of Diversification and Clause Sharing; 1.4.5 Examples of Parallel Portfolio Solvers; 1.5 Parallel Local Search; 1.5.1 Multiple Flips; 1.5.2 Portfolios; 1.6 Future Challenges; Acknowledgements; References; 2 Cube-and-Conquer for Satisfiability; 2.1 Introduction; 2.2 Preliminaries; 2.3 Combining CDCL and Lookahead; 2.4 Creating Cubes: The Basic Method; 2.5 Creating Cubes: a General Methodology; 2.5.1 General Framework
2.5.2 Cutoff Heuristic2.5.3 Heuristics for Splitting; 2.6 Solving Cubes; 2.6.1 Sequential Solving; 2.6.2 Solving Cubes in Parallel; 2.7 Interleaving the Cube and Conquer Phases; 2.7.1 Ineffective Lookahead Heuristics; 2.7.2 Concurrent Cube-and-Conquer; 2.7.3 Cubes on Demand; 2.8 Proofs of Unsatisfiability; 2.9 Experimental Evaluation; 2.9.1 Application Benchmarks; 2.9.2 The Boolean Pythagorean Triples Problem; 2.10 Conclusions; Acknowledgements; References; 3 Parallel Maximum Satisfiability; 3.1 Introduction; 3.2 Maximum Satisfiability; 3.2.1 Sequential MaxSAT Algorithms
3.2.1.1 Linear Search Algorithms3.2.1.2 Unsatisfiability-Based Algorithms; 3.2.1.3 Other Algorithmic Solutions and Implementation Issues; 3.3 Parallel MaxSAT; 3.3.1 Portfolio Approaches; 3.3.1.1 Parallel Unsatisfiability-Based Algorithms; 3.3.1.2 Parallel Linear Search Algorithms; 3.3.1.3 Implementation Issues; 3.3.2 Search Space Splitting; 3.3.2.1 Interval Splitting; 3.3.2.2 Guiding Paths; 3.3.2.3 Other Splitting Schemes and Implementation Issues; 3.3.3 Clause Sharing; 3.3.3.1 Conditions for Safe Clause Sharing; 3.3.3.2 Clause-Sharing Heuristics
3.3.3.3 Comparison Between Clause-Sharing Heuristics3.4 Deterministic Parallel MaxSAT; 3.4.1 Motivation; 3.4.2 Deterministic Solver; 3.4.2.1 Standard Synchronization; 3.4.2.2 Period Synchronization; 3.4.2.3 Dynamic Synchronization; 3.4.3 Comparison Between Non-deterministic and Deterministic Solvers; 3.5 Research Directions; 3.5.1 Scalability; 3.5.2 Clause Sharing; Acknowledgments; References; 4 Parallel Solving of Quantified Boolean Formulas; 4.1 Introduction; 4.2 Background; 4.3 Sequential Search-Based QBF Solving; 4.4 Parallel QBF Solving at a Glance; 4.5 Parallel QBF-Solving Approaches
1.4 Parallel Portfolios
Diversify and Conquer!1.4.1 Virtual Best Solver; 1.4.2 Pure Portfolio Solvers and Diversification; 1.4.3 Clause-Sharing Portfolios; 1.4.4 Impact of Diversification and Clause Sharing; 1.4.5 Examples of Parallel Portfolio Solvers; 1.5 Parallel Local Search; 1.5.1 Multiple Flips; 1.5.2 Portfolios; 1.6 Future Challenges; Acknowledgements; References; 2 Cube-and-Conquer for Satisfiability; 2.1 Introduction; 2.2 Preliminaries; 2.3 Combining CDCL and Lookahead; 2.4 Creating Cubes: The Basic Method; 2.5 Creating Cubes: a General Methodology; 2.5.1 General Framework
2.5.2 Cutoff Heuristic2.5.3 Heuristics for Splitting; 2.6 Solving Cubes; 2.6.1 Sequential Solving; 2.6.2 Solving Cubes in Parallel; 2.7 Interleaving the Cube and Conquer Phases; 2.7.1 Ineffective Lookahead Heuristics; 2.7.2 Concurrent Cube-and-Conquer; 2.7.3 Cubes on Demand; 2.8 Proofs of Unsatisfiability; 2.9 Experimental Evaluation; 2.9.1 Application Benchmarks; 2.9.2 The Boolean Pythagorean Triples Problem; 2.10 Conclusions; Acknowledgements; References; 3 Parallel Maximum Satisfiability; 3.1 Introduction; 3.2 Maximum Satisfiability; 3.2.1 Sequential MaxSAT Algorithms
3.2.1.1 Linear Search Algorithms3.2.1.2 Unsatisfiability-Based Algorithms; 3.2.1.3 Other Algorithmic Solutions and Implementation Issues; 3.3 Parallel MaxSAT; 3.3.1 Portfolio Approaches; 3.3.1.1 Parallel Unsatisfiability-Based Algorithms; 3.3.1.2 Parallel Linear Search Algorithms; 3.3.1.3 Implementation Issues; 3.3.2 Search Space Splitting; 3.3.2.1 Interval Splitting; 3.3.2.2 Guiding Paths; 3.3.2.3 Other Splitting Schemes and Implementation Issues; 3.3.3 Clause Sharing; 3.3.3.1 Conditions for Safe Clause Sharing; 3.3.3.2 Clause-Sharing Heuristics
3.3.3.3 Comparison Between Clause-Sharing Heuristics3.4 Deterministic Parallel MaxSAT; 3.4.1 Motivation; 3.4.2 Deterministic Solver; 3.4.2.1 Standard Synchronization; 3.4.2.2 Period Synchronization; 3.4.2.3 Dynamic Synchronization; 3.4.3 Comparison Between Non-deterministic and Deterministic Solvers; 3.5 Research Directions; 3.5.1 Scalability; 3.5.2 Clause Sharing; Acknowledgments; References; 4 Parallel Solving of Quantified Boolean Formulas; 4.1 Introduction; 4.2 Background; 4.3 Sequential Search-Based QBF Solving; 4.4 Parallel QBF Solving at a Glance; 4.5 Parallel QBF-Solving Approaches