https://bugzilla.redhat.com/show_bug.cgi?id=1718600
Bug ID: 1718600
Summary: Review Request: drat2er - Proof transformer for
propositional logic
Product: Fedora
Version: rawhide
Hardware: All
OS: Linux
Status: NEW
Component: Package Review
Severity: medium
Priority: medium
Assignee: [email protected]
Reporter: [email protected]
QA Contact: [email protected]
CC: [email protected]
Target Milestone: ---
Classification: Fedora
Spec URL: https://jjames.fedorapeople.org/drat2er/drat2er.spec
SRPM URL:
https://jjames.fedorapeople.org/drat2er/drat2er-0-0.1.20190307.521caf1.fc31.src.rpm
Fedora Account System Username: jjames
Description: 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.
--
You are receiving this mail because:
You are on the CC list for the bug.
You are always notified about changes to this product and component
_______________________________________________
package-review mailing list -- [email protected]
To unsubscribe send an email to [email protected]
Fedora Code of Conduct: https://getfedora.org/code-of-conduct.html
List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines
List Archives:
https://lists.fedoraproject.org/archives/list/[email protected]
