| Name: | drat-trim |
|---|---|
| Version: | 0 |
| Release: | 0.25.20240427giteffa1dc.el9 |
| Architecture: | aarch64 |
| Group: | Unspecified |
| Size: | 69912 |
| License: | MIT |
| RPM: | drat-trim-0-0.25.20240427giteffa1dc.el9.aarch64.rpm |
| Source RPM: | drat-trim-0-0.25.20240427giteffa1dc.el9.src.rpm |
| Build Date: | Wed Jan 07 2026 |
| Build Host: | build-ol9-aarch64.oracle.com |
| Vendor: | Oracle America |
| URL: | https://github.com/marijnheule/drat-trim |
| Summary: | Proof checker for DIMACS proofs |
| Description: | The proof checker DRAT-trim can be used to check whether a propositional formula in the DIMACS format is unsatisfiable. Given a propositional formula and a clausal proof, DRAT-trim validates that the proof is a certificate of unsatisfiability of the formula. Clausal proofs should be in the DRAT format which is used to validate the results of the SAT competitions. |