picosat - SAT solver with proof and core support

       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)

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

       picosat - SAT solver with proof and core support

-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

picosat [options] input-file