Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers

DOI10.1007/S10817-025-09725-WMaRDI QIDQ6957142zbMATH OpenFDO

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

Publication date 16 July 2025

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-025-09725-W

zbMATH Keywords

cloud computingdistributed computingHPCSAT solving

Mathematics Subject Classification ID

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

Cites work

• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• Automated testing and debugging of SAT and QBF solvers
• Between SAT and UNSAT: the fundamental difference in CDCL SAT
• Bounded model checking using satisfiability solving
• Decentralized Online Scheduling of Malleable NP-hard Jobs
• Efficient certified RAT verification
• Efficient verified (UN)SAT certificate checking
• Efficient, verified checking of propositional proofs
• Fast priority queues for cached memory
• Faster LRAT checking than solving with CaDiCaL
• HordeSat: a massively parallel portfolio SAT solver
• ManySAT: a parallel SAT solver
• Parallel merge sort with load balancing
• SAT competition 2020
• 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 intractability of resolution
• The packing chromatic number of the infinite square grid is 15
• The resolution of Keller's conjecture
• Trusted scalable SAT solving with on-the-fly LRAT checking
• Unsatisfiability proofs for distributed clause-sharing SAT solvers

This page was built for publication: Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers

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