Unsatisfiability proofs for distributed clause-sharing SAT solvers

DOI10.1007/978-3-031-30823-9_18MaRDI QIDQ6535367zbMATHFDO

Authors Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen

Publication date 13 December 2023

zbMATH Keywords

distributed computingSAT solving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Recommendations

• Partitioning SAT instances for distributed solving
• Compositional propositional proofs
• Soundness of inprocessing in clause sharing SAT solvers
• An expressive model for instance decomposition based parallel SAT solvers
• On the power of clause-learning SAT solvers as resolution engines

Cites work

• scientific article; zbMATH DE number 5620835 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Algorithm portfolios
• Decentralized Online Scheduling of Malleable NP-hard Jobs
• Efficient certified RAT verification
• Efficient verified (UN)SAT certificate checking
• Efficient, verified checking of propositional proofs
• HordeSat: a massively parallel portfolio SAT solver
• Inprocessing rules
• Lazy clause exchange policy for parallel SAT solvers
• ManySAT: a parallel SAT solver
• SAT competition 2020
• SATzilla: portfolio-based algorithm selection for SAT
• Scalable SAT solving in the cloud
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Space/time trade-offs in hash coding with allowable errors
• The resolution of Keller's conjecture
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Cited in

(1)

• On the (High) Undecidability of Distributed Synthesis Problems

This page was built for publication: Unsatisfiability proofs for distributed clause-sharing SAT solvers

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