PDRAT: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Tobias Philipp (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „PDRAT Checker =============“) |
Tobias Philipp (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 1: | Zeile 1: | ||
State-of-the-art SAT solvers are highly tuned systematic-search procedures augmented with formula simplification techniques. | |||
They emit unsatisfiability proofs in the DRAT format to guarantee correctness of their answers. | |||
However, the DRAT format is inadequate to model some parallel SAT solvers such as the award-winning system plingeling. | |||
The parallel DRAT format can be used to certify UNSAT answers from such parallel SAT solvers. | |||
Version vom 14. August 2016, 12:33 Uhr
State-of-the-art SAT solvers are highly tuned systematic-search procedures augmented with formula simplification techniques. They emit unsatisfiability proofs in the DRAT format to guarantee correctness of their answers. However, the DRAT format is inadequate to model some parallel SAT solvers such as the award-winning system plingeling. The parallel DRAT format can be used to certify UNSAT answers from such parallel SAT solvers.
