picosat(1)

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

NAME

6       picosat - Satisfiability (SAT) solver with proof and core support
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       The  picosat binary is built with options that provide for the greatest
21       speed.  A second binary, picosat.trace, is built with  proof  and  core
22       capabilities, which incur some overhead.
23
24

OPTIONS

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

CONFORMING TO

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

EXIT STATUS

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

EXAMPLE

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

AUTHORS

179       picosat was written by Armin Biere <biere@jku.at>
180
181       This man page was written by David A. Wheeler.  It is released  to  the
182       public domain; you may use it in any way you wish.
183
184