Rechercher une page de manuel

Chercher une autre page de manuel:


Langue: en

Version: 371053 (fedora - 01/12/10)

Section: 1 (Commandes utilisateur)


picosat - Satisfiability (SAT) solver for boolean variables


picosat [OPTION]... [FILE]


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.


print this command line option summary and exit
print version and exit
print build configuration and exit
enable verbose output
ignore invalid header
do not print satisfying assignment
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
-T <trace>
generate extended proof trace file
-r <trace>
generate reverse unit propagation proof file
-c <core>
generate clausal core file in DIMACS format
-V <core>
generate file listing core variables
-U <core>
generate file listing used variables

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


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:


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.


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.


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


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.



[article symposté dans "fr.rec.divers", "fr.sci.cogni.incognito",
"" et ""; suivi-à dirigé sur
-+- GOF in: Guide du Cabaliste Usenet - La Cabale s'étale -+-