Unsatisfiability proofs for distributed clause-sharing SAT solvers

DOI10.1007/978-3-031-30823-9_18zbMATH Open1543.68256MaRDI QIDQ6535367FDOQ6535367

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

Publication date: 13 December 2023

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

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)

Cites Work

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

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)