---
name: "drat-trim"
section: "1"
platform: "linux"
package: "drat-trim"
version: "0.0~git20240428.effa1dc-2"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/drat-trim"
---

# drat-trim(1)

DRAT-trim Satisfiability Proof Checker

## NAME

drat-trim - DRAT-trim Satisfiability Proof Checker

## DESCRIPTION

usage: drat-trim \[INPUT\] \[\<PROOF\>\] \[\<option\> ...\]

where \<option\> is one of the following

- **-h**

  print this command line option summary

- **-c** CORE

  prints the unsatisfiable core to the file CORE (DIMACS format)

- **-a** ACTIVE

  prints the active clauses to the file ACTIVE (DIMACS format)

- **-l** LEMMAS

  prints the core lemmas to the file LEMMAS (DRAT format)

- **-L** LEMMAS

  prints the core lemmas to the file LEMMAS (LRAT format)

- **-r** TRACE

  resolution graph in the TRACE file (TRACECHECK format)

- **-t** \<lim\>

  time limit in seconds (default 40000)

- **-u**

  default unit propatation (i.e., no core-first)

- **-f**

  forward mode for UNSAT

- **-v**

  more verbose output

- **-b**

  show progress bar

- **-O**

  optimize proof till fixpoint by repeating verification

- **-C**

  compress core lemmas (emit binary proof)

- **-D**

  delete proof file after parsing

- **-I**

  force ASCII proof parse mode

- **-i**

  force binary proof parse mode

- **-w**

  suppress warning messages

- **-W**

  exit after first warning

- **-p**

  run in plain mode (i.e., ignore deletion information)

- **-R**

  turn off reduce mode

- **-S**

  run in SAT check mode (forward checking)

- **-U**

  only allow RUP additions

and input and proof are specified as follows

- INPUT

  input file in DIMACS format

- PROOF

  proof file in DRAT format (stdin if no argument)