A flexible proof format for SAT solver-elaborator communication

DOI10.1007/978-3-030-72016-2_4zbMath1467.68159arXiv2109.09665OpenAlexW3138848921MaRDI QIDQ2044190

Yanyan Li

Publication date: 4 August 2021

Full work available at URL: https://arxiv.org/abs/2109.09665

zbMATH Keywords

satisfiabilityproof formatDRATFRATLRAT

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)

Related Items (2)

Unnamed Item ⋮ Clause redundancy and preprocessing in maximum satisfiability

Uses Software

• FRAT

Cites Work

• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• The intractability of resolution
• Efficient certified RAT verification
• SMT proof checking using a logical framework
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• versat: A Verified Modern SAT Solver
• Inprocessing Rules
• Verifying Refutations with Extended Resolution
• The Mechanical Verification of a DPLL-Based Satisfiability Solver
• Mechanical Verification of SAT Refutations with Extended Resolution
• Scalable fine-grained proofs for formula processing
• Efficient verified (UN)SAT certificate checking

This page was built for publication: A flexible proof format for SAT solver-elaborator communication