picomus(1)

1PICOMUS(1)                       User Commands                      PICOMUS(1)
2
3
4

NAME

6       picomus - Minimal Unsatisfiable Core (MUS) generator
7

SYNOPSIS

9       picomus [OPTION]... [INPUT [OUTPUT]]
10

DESCRIPTION

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

OPTIONS

17       -h     print this command line option summary and exit
18
19
20       -v     enable verbose output
21
22
23       If no input filename is given, or the input filename is "-", then stan‐
24       dard  input is used.  If the output filename is "-", then standard out‐
25       put is used.  If no output filename is given, then the MUS is  computed
26       but not printed.
27
28

CONFORMING TO

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

EXIT STATUS

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

AUTHORS

44       picomus was written by Armin Biere <biere@jku.at>
45
46       This man page was written by Jerry James.  It is released to the public
47       domain; you may use it in any way you wish.
48
49