A unified framework for DPLL(T) + certificates

DOI10.1155/2013/964682zbMath1267.68146OpenAlexW1517540595WikidataQ59007217 ScholiaQ59007217MaRDI QIDQ2375732

Bow-Yaw Wang, Min Zhou, Fei He, Jia-Guang Sun, Ming Gu

Publication date: 14 June 2013

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

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

zbMATH Keywords

SMT solverssatisfiability modulo theoryDPLL(T)certificate format

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)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An overview of backtrack search satisfiability algorithms
• SMT proof checking using a logical framework
• Solving SAT and SAT Modulo Theories
• A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
• Rocket-Fast Proof Checking for SMT Solvers
• A machine program for theorem-proving
• The complexity of theorem-proving procedures
• Tools and Algorithms for the Construction and Analysis of Systems

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