picosat (1) - Linux Manuals

picosat: Satisfiability (SAT) solver with proof and core support

NAME

picosat - Satisfiability (SAT) solver with proof and core support

SYNOPSIS

picosat [OPTION]... [FILE]

DESCRIPTION

PicoSAT is a satisfiability (SAT) solver for boolean variables in boolean expressions. A SAT solver can determine if it is possible to find assignments to boolean variables that would make a given set of expressions true. If it's satisfiable, it can also show a set of assignments that make the expression true. Many problems can be broken down into a large SAT problem (perhaps with thousands of variables), so SAT solvers have a variety of uses.

The picosat binary is built with options that provide for the greatest speed. A second binary, picosat.trace, is built with proof and core capabilities, which incur some overhead.

OPTIONS

-h

print this command line option summary and exit

--version

print version and exit

--config

print build configuration and exit

-v

enable verbose output

-f

ignore invalid header

-n

do not print satisfying assignment

-p

print formula in DIMACS format and exit

-a <lit>

start with an assumption

-l <limit>

set decision limit (no limit per default)

-i <0|1>

force FALSE respectively TRUE as default phase

-s <seed>

set random number generator seed (default 0)

-o <output>

set output file (<stdout> per default)

-t <trace>

generate compact proof trace file (use picosat.trace; see above)

-T <trace>

generate extended proof trace file (use picosat.trace; see above)

-r <trace>

generate reverse unit propagation proof file (use picosat.trace; see above)

-c <core>

generate clausal core file in DIMACS format (use picosat.trace; see above)

-V <core>

generate file listing core variables

-U <core>

generate file listing used variables

If no input filename is given, standard input is used.

CONFORMING TO

This program uses DIMACS CNF format as input.

Like many SAT solvers, this program requires that its input be in conjunctive normal form (CNF or cnf) in DIMACS CNF format. CNF is built from these building blocks:

*

R term : A term is either a boolean variable (e.g., x4) or a negated boolean variable (NOT x4, written here as -x4).

*

R clause : A clause is a set of one or more terms, connected with OR (written here as |); boolean variables may not repeat inside a clause.

*

R expression : An expression is a set of one or more clauses, each connected by AND (written here as &).

Any boolean expression can be converted into CNF.

DIMACS CNF format is a simple text format for CNF. Every line beginning "c" is a comment. The first non-comment line must be of the form:

 p cnf NUMBER_OF_VARIABLES NUMBER_OF_CLAUSES

Each of the non-comment lines afterwards defines a clause. Each of these lines is a space-separated list of variables; a positive value means that corresponding variable (so 4 means x4), and a negative value means the negation of that variable (so -5 means -x5). Each line must end in a space and the number 0.

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

If it is satisfiable, the output line beginning with "v" declares a set of variable settings that satisfy all formulas. For example:

  v 1 -2 -3 -4 5 0

Shows that there is a solution with variable 1 true, variables 2, 3, and 4 false, and variable 5 true.

EXAMPLE

An example of CNF is:

  (x1 | -x5 | x4) &
  (-x1 | x5 | x3 | x4) &
  (-x3 | x4).

The DIMACS CNF format for the above set of expressions could be:

 c Here is a comment.
 p cnf 5 3
 1 -5 4 0
 -1 5 3 4 0
 -3 -4 0

The "p cnf" line above means that this is SAT problem in CNF format with 5 variables and 3 clauses. The first line after it is the first clause, meaning x1 | -x5 | x4.

CNFs with conflicting requirements are not satisfiable. For example, the following DIMACS CNF formatted data is not satisfiable, because it requires that variable 1 always be true and also always be false:

 c This is not satisfiable.
 p cnf 2 2
 -1 0
 1 0

AUTHORS

picosat was written by Armin Biere <biere [at] jku.at>

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