.TH "PICOMUS" "1" "Version 936" "PicoSAT" "User Commands"
.SH "NAME"
picomus \- Minimal Unsatisfiable Core (MUS) generator
.SH "SYNOPSIS"
.B picomus
[\fIOPTION\fR]... [\fIINPUT\fR [\fIOUTPUT\fR]]
.SH "DESCRIPTION"
.\" Add any additional description here
.PP
PicoMUS is a satisfiability (SAT) solver that generates a minimal unsatisfiable
core, using the PicoSAT library.

.SH "OPTIONS"
.TP
.BI \-h
print this command line option summary and exit

.TP
.BI \-v
enable verbose output

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

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

.SH "EXIT STATUS"
.PP
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).

.SH "AUTHORS"
picomus was written by Armin Biere <biere@jku.at>
.PP
This man page was written by Jerry James.
It is released to the public domain; you may use it in any way you wish.

.SH "SEE ALSO"
.PP
\fIpicosat\fP(1), \fIminisat2\fP(1).

.\" This documentation was written by Jerry James in 2011, and
.\" is released to the public domain.  Anyone can use it, in any way.