You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
56 lines
1.6 KiB
56 lines
1.6 KiB
.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.
|