PICOSAT(1)						      General Commands Manual							PICOSAT(1)

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

								 February  5, 2010							PICOSAT(1)