picosat(1)

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

NAME

6       picosat - Satisfiability (SAT) solver for boolean variables
7

SYNOPSIS

9       picosat [OPTION]... [FILE]
10

DESCRIPTION

12       PicoSAT is a satisfiability (SAT) solver for boolean variables in bool‐
13       ean expressions.  A SAT solver can determine if it is possible to  find
14       assignments to boolean variables that would make a given set of expres‐
15       sions true.  If it's satisfiable, it can also show a set of assignments
16       that make the expression true.  Many problems can be broken down into a
17       large SAT problem (perhaps with thousands of variables), so SAT solvers
18       have a variety of uses.
19
20

OPTIONS

22       -h     print this command line option summary and exit
23
24
25       --version
26              print version and exit
27
28
29       --config
30              print build configuration and exit
31
32
33       -v     enable verbose output
34
35
36       -f     ignore invalid header
37
38
39       -n     do not print satisfying assignment
40
41
42       -p     print formula in DIMACS format and exit
43
44
45       -a <lit>
46              start with an assumption
47
48
49       -l <limit>
50              set decision limit (no limit per default)
51
52
53       -i <0|1>
54              force FALSE respectively TRUE as default phase
55
56
57       -s <seed>
58              set random number generator seed (default 0)
59
60
61       -o <output>
62              set output file (<stdout> per default)
63
64
65       -t <trace>
66              generate compact proof trace file
67
68
69       -T <trace>
70              generate extended proof trace file
71
72
73       -r <trace>
74              generate reverse unit propagation proof file
75
76
77       -c <core>
78              generate clausal core file in DIMACS format
79
80
81       -V <core>
82              generate file listing core variables
83
84
85       -U <core>
86              generate file listing used variables
87
88
89       If no input filename is given, standard input is used.
90
91

CONFORMING TO

93       This program uses DIMACS CNF format as input.
94
95       Like  many SAT solvers, this program requires that its input be in con‐
96       junctive normal form (CNF or cnf) in DIMACS CNF format.  CNF  is  built
97       from these building blocks:
98
99       *  R term : A term is either a boolean variable (e.g., x4) or a negated
100          boolean variable (NOT x4, written here as -x4).
101
102       *  R clause : A clause is a set of one or more terms, connected with OR
103          (written  here  as  |);  boolean  variables may not repeat  inside a
104          clause.
105
106       *  R expression : An expression is a set of one or more  clauses,  each
107          connected by AND (written here as &).
108
109
110       Any boolean expression can be converted into CNF.
111
112
113       DIMACS  CNF  format is a simple text format for CNF.  Every line begin‐
114       ning "c" is a comment.  The first non-comment line must be of the form:
115
116        p cnf NUMBER_OF_VARIABLES NUMBER_OF_CLAUSES
117
118       Each of the non-comment lines afterwards defines  a  clause.   Each  of
119       these  lines  is  a space-separated list of variables; a positive value
120       means that corresponding variable (so 4 means x4), and a negative value
121       means  the negation of that variable (so -5 means -x5).  Each line must
122       end in a space and the number 0.
123
124

EXIT STATUS

126       The output is a number of lines.  Most of these  will  begin  with  "c"
127       (comment),  and  give  detailed technical information.  The output line
128       beginning with "s" declares whether or not it is satisfiable.  The line
129       "s  SATISFIABLE" is produced if it is satisfiable (exit status 10), and
130       "s UNSATISFIABLE" is produced if it is  not  satisfiable  (exit  status
131       20).
132
133       If it is satisfiable, the output line beginning with "v" declares a set
134       of variable settings that satisfy all formulas.  For example:
135
136         v 1 -2 -3 -4 5 0
137
138       Shows that there is a solution with variable 1 true,  variables  2,  3,
139       and 4 false, and variable 5 true.
140
141

EXAMPLE

143       An example of CNF is:
144
145         (x1 | -x5 | x4) &
146         (-x1 | x5 | x3 | x4) &
147         (-x3 | x4).
148
149       The DIMACS CNF format for the above set of expressions could be:
150
151        c Here is a comment.
152        p cnf 5 3
153        1 -5 4 0
154        -1 5 3 4 0
155        -3 -4 0
156
157       The  "p  cnf"  line  above means that this is SAT problem in CNF format
158       with 5 variables and 3 clauses.   The first line after it is the  first
159       clause, meaning x1 | -x5 | x4.
160
161       CNFs  with  conflicting requirements are not satisfiable.  For example,
162       the following DIMACS CNF formatted data is not satisfiable, because  it
163       requires that variable 1 always be true and also always be false:
164
165        c This is not satisfiable.
166        p cnf 2 2
167        -1 0
168        1 0
169
170

AUTHORS

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