pith. sign in

arxiv: 1610.06229 · v1 · pith:AQIPLIHPnew · submitted 2016-10-19 · 💻 cs.LO

The DRAT format and DRAT-trim checker

Marijn J. H. Heule This is my paper
classification 💻 cs.LO
keywords checkerdratdrat-trimformatclausaldescribesdocumentproof
0
0 comments X
read the original abstract

This document describes the DRAT format for clausal proofs and the DRAT-trim proof checker.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. A Resolution-Based Interactive Proof System for UNSAT

    cs.LO 2024-01 unverdicted novelty 8.0

    First interactive protocol for Davis-Putnam resolution that is competitive with BDD methods for certifying UNSAT.