Certifying incremental SAT solving

DOI10.29007/PDCCMaRDI QIDQ7025181zbMATH OpenFDO

Authors Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/PDCC

zbMATH Keywords

certificationincremental SATproof checkingproofs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A flexible proof format for SAT solver-elaborator communication
• Automated testing and debugging of SAT and QBF solvers
• AVATAR: The Architecture for First-Order Theorem Provers
• Computer aided verification. 34th international conference, CAV 2022, Haifa, Israel, August 7--10, 2022. Proceedings. Part I
• Efficient certified RAT verification
• Faster LRAT checking than solving with CaDiCaL
• Handbook of satisfiability. In 2 parts
• scientific article; zbMATH DE number 7178357 (Why is no real title available?)
• scientific article; zbMATH DE number 2201583 (Why is no real title available?)
• Incremental inprocessing in SAT solving
• IPASIR-up: user propagators for CDCL
• Lazy satisfiability modulo theories
• Progress in certifying hardware model checking results
• SAT race 2015
• SAT-Based Model Checking
• Scalable fine-grained proofs for formula processing
• Temporal induction by incremental SAT solving
• Theory and Applications of Satisfiability Testing

Cited in

(1)

• Satisfiability modulo user propagators

This page was built for publication: Certifying incremental SAT solving

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