Section: User Commands (1) Updated: February 5, 2010 Local index
picosat - SAT solver with proof and core support
This manual page documents briefly the
picosat is a SAT solver with proof and core capabilities. Use the
picosat.trace binary to actually use these capabilities (these incur some
Show summary of options.
print version and exit
print build configuration and exit
enable verbose output
ignore invalid header
do not print satisfying assignment
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
picosat was written by Armin Biere <email@example.com>.
This manual page was written by Michael Tautschnig <firstname.lastname@example.org>,
for the Debian project (but may be used by others).
This document was created by
using the manual pages.
Time: 21:24:48 GMT, April 16, 2011