picomus (1) - Linux Manuals

picomus: Minimal Unsatisfiable Core (MUS) generator

NAME

picomus - Minimal Unsatisfiable Core (MUS) generator

SYNOPSIS

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

DESCRIPTION

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

OPTIONS

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

CONFORMING TO

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

EXIT STATUS

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

AUTHORS

picomus was written by Armin Biere <biere [at] 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.