An Expressive Model for Instance Decomposition Based Parallel SAT Solvers

DOI10.1007/978-3-319-24246-0_7zbMath1471.68315OpenAlexW2293411300MaRDI QIDQ2964456

Tobias Philipp

Publication date: 27 February 2017

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24246-0_7

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• MiniSat
• Chaff
• NiVER
• Plingeling
• PrecoSAT
• versat
• CryptoMiniSat
• DRAT-trim
• Coprocessor
• Lingeling
• BooleForce

Cites Work

• Unnamed Item
• An overview of parallel SAT solving
• Formalization and implementation of modern SAT solvers
• Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• versat: A Verified Modern SAT Solver
• Inprocessing Rules
• On Freezing and Reactivating Learnt Clauses
• Efficient CNF Simplification Based on Binary Implication Graphs
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Incorporating Learning in Grid-Based Randomized SAT Solving
• Blocked Clause Elimination
• Partitioning SAT Instances for Distributed Solving
• Improving Resource-Unaware SAT Solvers
• Theory and Applications of Satisfiability Testing
• Soundness of Inprocessing in Clause Sharing SAT Solvers
• Mechanical Verification of SAT Refutations with Extended Resolution
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

This page was built for publication: An Expressive Model for Instance Decomposition Based Parallel SAT Solvers