-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathcertificates.html
231 lines (191 loc) · 7.96 KB
/
certificates.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>SAT Race 2019</title>
<link rel="stylesheet" href="main.css" type="text/css">
<link rel="icon" type="image/x-icon" href="doge2.ico">
<script src="https://www.w3schools.com/lib/w3.js"></script>
<style>a#certificates { color:#c20114; }</style>
</head>
<body>
<div class="main">
<div class="navigation" w3-include-html="navigation.html"></div>
<script>w3.includeHTML();</script>
<div class="content">
<h1>SAT Race 2019</h1>
<h2>Certified UNSAT</h2>
<p>
Certificates of unsatisfiability have been required for the UNSAT tracks since
SAT Competition 2013. This year we will require certificates of unsatisfiablity
for all participants.
</p>
<p>
Although resolution proof formats have been supported in the past,
SAT Race 2019 will only support clausal proofs. The main reason
for this restriction is that no participant in recent years showed any
interest in providing resolution proofs as such proofs as too complicated to
produce and they cost too much space to store.<br>
</p>
<p>
The proof format of SAT Race 2019 is the same as in 2018, i.e.,
<a href="http://www.cs.utexas.edu/~marijn/drat-trim/" target="_blank">DRAT</a>
(Delete Resolution Asymmetric Tautologies) which is backwards compatible
with both RUP (Reverse Unit Propagation) and
<a href="http://www.cs.utexas.edu/~marijn/drup/" target="_blank">DRUP</a>.
During SAT Competition 2014, a few runs produced proofs of over 100GB,
the local storage limit. In order to avoid this issue in 2019, we will
also support a <b>binary DRAT format</b>. Details and the checker will be made
available on the <a href="http://www.cs.utexas.edu/~marijn/drat-trim/">DRAT website</a>.
</p>
<p>
<b>The proof should be written into a (text/binary) file called "proof.out", which is then passed to the verifier.</b> <br>
The output of the solver though, should conform to the following rules:
<ul>
<li> Comment lines are to be prepended by <b>"c "</b></li>
<li> In case of UNSAT a proof in the DRAT format should be written into "proof.out"</li>
<li> Solution line <b>"s SATISFIABLE"</b> or <b>"s UNSATISFIABLE"</b></li>
</ul>
The solution line can appear anywhere in the output of the solver, though
the solution "v ..." in case of SAT should appear after the solution line
"s SATISFIABLE" as it is the case in the original specification.<br>
<h3>Certified UNSAT solver output example</h3>
<pre>
c this is a solver output example
c computing ....
c statistics ...
s UNSATISFIABLE
</pre>
<h3>Format</h3>
Below is a brief description of the proof format based on an example formula.
The new proof format DRAT is backwards compatible with both the DRUP and RUP formats.
More details about DRUP can be found <a href="http://cs.utexas.edu/~marijn/drup/" target="_blank">here</a>.
The spacing in the examples is to improve readability. Consider the following
formula in the DIMACS format.
<br><br>
<pre>
p cnf 4 8
1 2 -3 0
-1 -2 3 0
2 3 -4 0
-2 -3 4 0
1 3 4 0
-1 -3 -4 0
-1 2 4 0
1 -2 -4 0
</pre>
<br>
A proof of the above formula in the RUP (and thus DRAT) format is:
<br><br>
<pre>
1 2 0
1 0
2 0
0
</pre>
<br>
A RUP proof is a sequence of clauses that are redundant with respect to the input formula.
To check that a clause C is redundant, all literals l in C are assigned to false followed
by unit propagation. In order to verify redundancy, unit propagation should result in
a conflict. The redundant clause is added to the formula in case the check is successful.
The conflict clauses produced by conflict-driven clause learning (CDCL) solvers have the RUP property.
Therefore, a sequence of all conflict clauses (in the order of
learning) is a RUP proof for unsatisfiable formulas.
<br><br>
One important disadvantage of checking RUP proofs is the cost of verifying a proof.
The DRUP format (Delete Reverse Unit
Propagation) was developed to counter this disadvantage.
The DRUP format extends the RUP format by allowing it to express
clause elimination information within the proof format.
<br><br>
<pre>
1 2 0
d 1 2 -3 0
1 0
d 1 2 0
d 1 3 4 0
d 1 -2 -4 0
2 0
0
</pre>
<br>
Apart from the redundant RUP clauses, a DRUP proof may contain lines with a 'd'
prefix. These lines refer to clauses (original or learned) that can be deleted
without influencing the proof checking. In the above example, all the deleted
clauses are subsumed by the added RUP clauses. In practice, however, the clauses
that one wants to include in a DRUP proof are the clauses that are removed
while reducing the (learned) clause database.<br><br>
Some state-of-the-art SAT solvers use techniques, such as extended resolution,
that cannot be validated using RUP.
The DRAT format (Delete Resolution Asymmetric Tautologies) was developed to
deal with this.
<br><br>
<pre>
1 0
d 1 2 -3 0
d 1 2 0
d 1 3 4 0
d 1 -2 -4 0
2 0
0
</pre>
<br>
The syntax of DRAT proofs is identical to DRUP proofs. Lines contain either
a 'd' expression which denotes deletion, or have no prefix expression which stands for clause addition.
<h3>Binary Format</h3>
<h5>Mapping DIMACS Literals to Unsigned Integers</h5>
The first step of the binary encoding is mapping literals in
the DIMACS format to unsigned integers. The following mapping function is used:
map(l) := (l > 0)? 2*l : -2*l + 1. The mapping for some DIMACS literals are shown below.<BR><BR>
<pre> DIMACS literals unsigned integers
-63 127
129 258
-8191 16383
-8193 16387
</pre><BR>
<h5>Variable-Byte Encoding of Unsigned Integers</h5>
Assume that 'w0, ..., wi' are 7-bit words, 'w1' to 'wi' all non zero and
the unsigned number 'x' can be represented as<BR><BR>
<pre> x = w0 + 2^7*w1 + 2^14*w2 + ... + 2^(7*i)*wi</pre><BR>
The variable-byte encoding of DRAT (also used in <A href="http://fmv.jku.at/aiger/">AIGER</A>) is the sequence of
i bytes b0, ... bi:<BR><BR>
<pre> 1w0, 1w1, 1w2, ..., 0wi </pre><BR>
/Users/mbassms6/Desktop/satcomp/downloads.html
The MSB of a byte in this sequence signals whether this byte is the last
byte in the sequence, or whether there are still more bytes to follow.
Here are some examples:<BR><BR>
<pre> unsigned integer byte sequence of encoding (in hexadecimal)
x b0 b1 b2 b3 b4
0 00
1 01
2^7-1 = 127 7f
2^7 = 128 80 01
2^8 + 2 = 258 82 02
2^14 - 1 = 16383 ff 7f
2^14 + 3 = 16387 83 80 01
2^28 - 1 ff ff ff 7f
2^28 + 7 87 80 80 80 01
</pre><br>
<h5>Bringing it together</h5>
In the binary DRAT format, each clause consists of at least two bytes. The
first byte expresses whether the lemma is added (character 'a' or 61 in
hexadecimal) or deleted (character 'd' or 64 in hexadecimal). The last byte
of each lemma is the zero byte (00 in hexadecimal). In between these two
bytes, the literals of the lemma are shown as unsigned integers in the
variable-byte encoding.<BR><BR>
In the example below, the plain DRAT format requires 26 bytes (including the
new line characters and excluding the redundant spaces in the second lemma),
while the binary DRAT format of the same proof requires only 12 bytes. Emiting
proofs in the binary format reduces the size on disk by approximatedly a
factor of three compared to the conventional (plain) DRAT format.<BR><BR>
<pre> plain DRAT binary DRAT (in hexadecimal)
d -63 -8193 0 64 7f 83 80 01 00 61 82 02 ff 7f 00
129 -8191 0
</pre>
<h5>Demo</h5>
A <a href="downloads/glucose-3.0D.zip">modified Glucose 3.0</a> which outputs the proof in a binary format is available. Run it using the command
<pre>./glucose unsat-benchmark.cnf -vbyte -certified -certified-output=proof.out</pre> to produce a binary proof.
</div>
</div>
</body>
</html>