scientific article; zbMATH DE number 7566059

MaRDI QIDQ5094131

No author found.

Publication date: 2 August 2022

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

satisfiabilityproof formatDRATLRATFRA

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items

FRAT

Uses Software

• versat
• CakeML
• DRAT-trim
• GRAT
• cake_lpr

Cites Work

• Unnamed Item
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• The intractability of resolution
• A verified SAT solver framework with learn, forget, restart, and incrementality
• A flexible proof format for SAT solver-elaborator communication
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• Short proofs without new variables
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• versat: A Verified Modern SAT Solver
• Inprocessing Rules
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• 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