An expressive model for instance decomposition based parallel SAT solvers

DOI10.1007/978-3-319-24246-0_7MaRDI QIDQ2964456zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Clause simplifications in search-space decomposition-based SAT solvers
• ManySAT: a parallel SAT solver
• Partitioning SAT instances for distributed solving
• Soundness of inprocessing in clause sharing SAT solvers
• Parallel SAT solving in bounded model checking

Cites work

• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• A machine program for theorem-proving
• An overview of parallel SAT solving
• Blocked clause elimination
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Efficient CNF simplification based on binary implication graphs
• 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
• Improving resource-unaware SAT solvers
• Incorporating Learning in Grid-Based Randomized SAT Solving
• Inprocessing rules
• Mechanical verification of SAT refutations with extended resolution
• On freezing and reactivating learnt clauses
• Partitioning SAT instances for distributed solving
• Soundness of inprocessing in clause sharing SAT solvers
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• versat: A Verified Modern SAT Solver

Cited in

(6)

• Clause simplifications in search-space decomposition-based SAT solvers
• Parallelizing SMT solving: lazy decomposition and conciliation
• Decomposing SAT Instances with Pseudo Backbones
• Soundness of inprocessing in clause sharing SAT solvers
• Unsatisfiability proofs for distributed clause-sharing SAT solvers
• Lazy clause exchange policy for parallel SAT solvers

Describes a project that uses

Uses Software

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

This page was built for publication: An expressive model for instance decomposition based parallel SAT solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2964456)