PICOSAT
PICOSAT
Section: User Commands (1) Updated: February 5, 2010 Local index
Up
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).
Index
- NAME
-
- SYNOPSIS
-
- DESCRIPTION
-
- OPTIONS
-
- AUTHOR
-
This document was created by
man2html,
using the manual pages.
Time: 21:24:48 GMT, April 16, 2011