picomus - Man Page

picomus [OPTION]... [INPUT [OUTPUT]]

PicoMUS is a satisfiability (SAT) solver that generates a minimal unsatisfiable core, using the PicoSAT library.

-h

print this command line option summary and exit

-v

enable verbose output

If no input filename is given, or the input filename is "-", then standard input is used.  If the output filename is "-", then standard output is used. If no output filename is given, then the MUS is computed but not printed.

This program uses DIMACS CNF format as input.  The output conforms to the standard SAT solver format used at SAT competitions.

The output is a number of lines. Most of these will begin with "c" (comment), and give detailed technical information. The output line beginning with "s" declares whether or not it is satisfiable. The line "s SATISFIABLE" is produced if it is satisfiable (exit status 10), and "s UNSATISFIABLE" is produced if it is not satisfiable (exit status 20).

picomus was written by Armin Biere <biere@jku.at>

This man page was written by Jerry James. It is released to the public domain; you may use it in any way you wish.

picosat(1), minisat2(1).

picosat(1).