A unified framework for DPLL(T) + certificates

DOI10.1155/2013/964682MaRDI QIDQ2375732zbMATH OpenOpenAlexWikidataFDO

Authors Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun

Publication date 14 June 2013

Published in Journal of Applied Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1155/2013/964682

zbMATH Keywords

certificate formatDPLL(T)satisfiability modulo theorySMT solvers

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)

Review text

Summary: Satisfiability modulo theories (SMT) techniques are widely used nowadays. SMT solvers are typically used as verification backends. When an SMT solver is invoked, it is quite important to ensure the correctness of its results. To address this problem, we propose a unified certificate framework based on DPLL(T), including a uniform certificate format, a unified certificate generation procedure, and a unified certificate checking procedure. The certificate format is shown to be simple, clean, and extensible to different background theories. The certificate generation procedure is well adapted to most DPLL(T)-based SMT solvers. The soundness and completeness for DPLL(T) + certificates were established. The certificate checking procedure is straightforward and efficient. Experimental results show that the overhead for certificates generation is only 10\%, which outperforms other methods, and the certificate checking procedure is quite time saving.

Recommendations

• Efficient verified (UN)SAT certificate checking
• Efficient verified (UN)SAT certificate checking
• SMT proof checking using a logical framework
• Rocket-Fast Proof Checking for SMT Solvers
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)

Cites work

• A machine program for theorem-proving
• A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
• An overview of backtrack search satisfiability algorithms
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 1179974 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Rocket-Fast Proof Checking for SMT Solvers
• SMT proof checking using a logical framework
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• The complexity of theorem-proving procedures
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(2)

• A framework for developing stand-alone certifiers
• Efficient verified (UN)SAT certificate checking

Describes a project that uses

Uses Software

• z3
• CLSAT
• Isabelle/HOL
• cvc3
• Chaff
• MiniSat
• SMT-LIB
• PicoSAT

This page was built for publication: A unified framework for DPLL(T) + certificates

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