---
name: "picosat"
section: "1"
platform: "linux"
package: "picosat"
version: "965-2"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/picosat"
---

# picosat(1)

SAT solver with proof and core support

## NAME

picosat - SAT solver with proof and core support

## SYNOPSIS

**picosat** \[*options*\] *input-file*

## DESCRIPTION

This manual page documents briefly the **picosat** command.

**picosat** is a SAT solver with proof and core capabilities. Use the **picosat.trace** binary to actually use these capabilities (these incur some overhead).

## OPTIONS

**-h** Show summary of options.

- **--version**

  print version and exit

- **--config**

  print build configuration and exit

- **-v**

  enable verbose output

- **-f**

  ignore invalid header

- **-n**

  do not print satisfying assignment

- **-p**

  print formula in DIMACS format and exit

- **-i \<0/1\>**

  force FALSE respectively TRUE as default phase

- **-a \<lit\>**

  start with an assumption

- **-l \<limit\>**

  set decision limit

- **-s \<seed\>**

  set random number generator seed

- **-o \<output\>**

  set output file

- **-t \<trace\>**

  generate compact proof trace file (use picosat.trace, see above).

- **-T \<trace\>**

  generate extended proof trace file (use picosat.trace, see above).

- **-r \<trace\>**

  generate reverse unit propagation proof file (use picosat.trace, see above).

- **-c \<core\>**

  generate clausal core file in DIMACS format (use picosat.trace, see above).

- **-V \<core\>**

  generate file listing core variables

- **-U \<core\>**

  generate file listing used variables

## AUTHOR

picosat was written by Armin Biere \<biere@jku.at\>.

This manual page was written by Michael Tautschnig \<mt@debian.org\>, for the Debian project (but may be used by others).