Faster LRAT checking than solving with CaDiCaL

DOI10.4230/LIPICS.SAT.2023.21MaRDI QIDQ6643101zbMATH OpenFDO

Authors Florian Pollitt, Mathias Fleury, Armin Biere

Publication date 26 November 2024

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

zbMATH Keywords

DRATFRATLRATproof checkingSAT solving

Mathematics Subject Classification ID

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

Cited in

(6)

• Trusted scalable SAT solving with on-the-fly LRAT checking
• Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers
• Certifying incremental SAT solving
• Fast and verified UNSAT certificate checking
• Improving the SMT proof reconstruction pipeline in Isabelle/HOL
• Hardware model checking certification with Certifaiger and Cerbtora

This page was built for publication: Faster LRAT checking than solving with CaDiCaL

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