picosat.trace

Langue: en

Version: February 5, 2010 (ubuntu - 24/10/10)

Section: 1 (Commandes utilisateur)

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