Trusted scalable SAT solving with on-the-fly LRAT checking

DOI10.4230/LIPICS.SAT.2024.25MaRDI QIDQ6864414zbMATH OpenFDO

Authors Dominik Schreiber

Publication date 3 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.SAT.2024.25

zbMATH Keywords

distributed algorithmsSAT solvingproofs

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07)

Cites work

• A verified SAT solver framework with learn, forget, restart, and incrementality
• Automated testing and debugging of SAT and QBF solvers
• Bounded model checking using satisfiability solving
• Codes Which Detect Deception
• Decentralized Online Scheduling of Malleable NP-hard Jobs
• Efficient certified RAT verification
• Efficient verified (UN)SAT certificate checking
• Efficient, verified checking of propositional proofs
• Extended resolution simulates \({\mathsf{DRAT}}\)
• Faster LRAT checking than solving with CaDiCaL
• Handbook of parallel constraint reasoning
• Lilotane: a lifted SAT-based approach to hierarchical planning
• MUS Extraction Using Clausal Proofs
• On tackling the limits of resolution in SAT solving
• PaSAT -- parallel SAT-checking with lemma exchange: Implementation and applications
• SAT competition 2020
• Scalable SAT solving in the cloud
• SipHash: a fast short-input PRF
• Solving huge instances with Intel SAT solver
• Soundness of inprocessing in clause sharing SAT solvers
• Unsatisfiability proofs for distributed clause-sharing SAT solvers

Cited in

(1)

• Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers

This page was built for publication: Trusted scalable SAT solving with on-the-fly LRAT checking

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