drat2er
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 | - |
Package Info
- Upstream: https://github.com/benjaminkiesl/drat2er
- License(s): MIT
- Maintainer: jjames
Related Packages
You can contact the maintainers of this package via email at
drat2er dash maintainers at fedoraproject dot org.
Sources on Pagure