drat-trim
DRAT-trim is a satisfiability proof checking and trimming utility designed to validate proofs for all known satisfiability solving and preprocessing techniques. DRAT-trim can also emit trimmed formulas, optimized proofs, and TraceCheck+ dependency graphs.
DRAT-trim has been used as part of the judging process in the annual SAT Competition in recent years, in order to check competing SAT solvers' work when they claim that a SAT instance is unsatisfiable.
This package also contains the related tool LRAT-check, which checks a proof format called LRAT which extends DRAT with hint statements to speed up the checking process.
- Name
- drat-trim
- Programs
drat-trimlrat-check
- Homepage
- Version
- 2023-05-22
- License
- Maintainers
- Platforms
- i686-cygwin
- x86_64-cygwin
- x86_64-darwin
- aarch64-darwin
- i686-freebsd
- x86_64-freebsd
- aarch64-freebsd
- aarch64-genode
- i686-genode
- x86_64-genode
- x86_64-solaris
- javascript-ghcjs
- aarch64-linux
- armv5tel-linux
- armv6l-linux
- armv7a-linux
- armv7l-linux
- i686-linux
- loongarch64-linux
- m68k-linux
- microblaze-linux
- microblazeel-linux
- mips-linux
- mips64-linux
- mips64el-linux
- mipsel-linux
- powerpc-linux
- powerpc64-linux
- powerpc64le-linux
- riscv32-linux
- riscv64-linux
- s390-linux
- s390x-linux
- x86_64-linux
- mmix-mmixware
- aarch64-netbsd
- armv6l-netbsd
- armv7a-netbsd
- armv7l-netbsd
- i686-netbsd
- m68k-netbsd
- mipsel-netbsd
- powerpc-netbsd
- riscv32-netbsd
- riscv64-netbsd
- x86_64-netbsd
- aarch64_be-none
- aarch64-none
- arm-none
- armv6l-none
- avr-none
- i686-none
- microblaze-none
- microblazeel-none
- mips-none
- mips64-none
- msp430-none
- or1k-none
- m68k-none
- powerpc-none
- powerpcle-none
- riscv32-none
- riscv64-none
- rx-none
- s390-none
- s390x-none
- vc4-none
- x86_64-none
- i686-openbsd
- x86_64-openbsd
- x86_64-redox
- wasm64-wasi
- wasm32-wasi
- aarch64-windows
- x86_64-windows
- i686-windows
- Defined
- Source