An expressive model for instance decomposition based parallel SAT solvers

DOI10.1007/978-3-319-24246-0_7zbMATH Open1471.68315OpenAlexW2293411300MaRDI QIDQ2964456FDOQ2964456

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

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

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)

Cites Work

• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Theory and Applications of Satisfiability Testing
• Title not available (Why is that?)
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• A machine program for theorem-proving
• Inprocessing rules
• Formalization and implementation of modern SAT solvers
• Blocked clause elimination
• Improving resource-unaware SAT solvers
• Partitioning SAT instances for distributed solving
• Efficient CNF simplification based on binary implication graphs
• Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
• On freezing and reactivating learnt clauses
• An overview of parallel SAT solving
• versat: A Verified Modern SAT Solver
• Mechanical verification of SAT refutations with extended resolution
• Soundness of inprocessing in clause sharing SAT solvers
• Incorporating Learning in Grid-Based Randomized SAT Solving

Cited In (6)

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

Uses Software

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

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)