Fedora Packages


Proof transformer for propositional logic

Drat2er is a tool for transforming proofs that are usually produced by SAT solvers. It takes as input a propositional formula (specified in the DIMACS format) together with a DRAT proof (DRAT is the current standard format for proofs in SAT solving), and outputs an extended-resolution proof of the formula in either the TRACECHECK or the DRAT format. The details of this proof transformation are described in the paper "Extended Resolution Simulates DRAT" (IJCAR 2018). Note that if drat2er is given as input a DRUP proof, then it transforms this DRUP proof into an ordinary resolution proof.

Releases Overview

Release Stable Testing
Fedora Rawhide 0-0.15.20211228git6dfd668.fc41 -
Fedora 40 0-0.15.20211228git6dfd668.fc40 0-0.15.20211228git6dfd668.fc40
Fedora 39 0-0.12.20190307.521caf1.fc39 -
Fedora 38 0-0.11.20190307.521caf1.fc38 -
File a new bug report »
Package Info
Related Packages

You can contact the maintainers of this package via email at drat2er dash maintainers at fedoraproject dot org.

Sources on Pagure