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).