picosat.trace1

Usage

Overview

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