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
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
|
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Selecting the Given Clause</title>
<link rel="stylesheet" href="manual.css">
</head>
<body>
<hr>
<table width="100%">
<tr>
<colgroup>
<col width="33%">
<col width="34%">
<col width="33%">
</colgroup>
<td align="left"><i>Prover9 Manual</i>
<td align="center"><img src="prover9-5a-256t.gif">
<td align="right"><i>Version 2009-02A</i>
</table>
<hr>
<!-- Main content -->
<h1>Selecting the Given Clause</h1>
At each iteration of the <a href="loop.html">main loop</a>,
Prover9 selects a <i>given clause</i> from the <tt>sos</tt> list,
moves it to the <tt>usable</tt> list, and makes inferences
from it and other clauses in the <tt>usable</tt> list.
<p>
A basic way to select the given clause is to always select the
<a href="weight.html">lightest clause</a>
in <tt>sos</tt>.
Otter has the ability to mix two methods of selecting
the given clause in a ratio determined by a parameter ---
selecting the lightest clause and selecting the oldest
clause. This method adds a breadth-first component
to the search. See the
<a href="select.html#pick_given_ratio"><tt><b>pick_given_ratio</b></tt></a>
parameter below.
<p>
Prover9 uses six components in selecting the given clause.
The following six options are used.
<!-- start option age_part -->
<a name="age_part">
<pre class="my_option">
assign(age_part, <i>n</i>). % default <i>n</i>=1, range [0 .. <tt>INT_MAX</tt>]
</pre>
<!-- end option -->
<!-- start option weight_part -->
<a name="weight_part">
<pre class="my_option">
assign(weight_part, <i>n</i>). % default <i>n</i>=0, range [0 .. <tt>INT_MAX</tt>]
</pre>
<!-- end option -->
<!-- start option false_part -->
<a name="false_part">
<pre class="my_option">
assign(false_part, <i>n</i>). % default <i>n</i>=4, range [0 .. <tt>INT_MAX</tt>]
</pre>
<!-- end option -->
<!-- start option true_part -->
<a name="true_part">
<pre class="my_option">
assign(true_part, <i>n</i>). % default <i>n</i>=4, range [0 .. <tt>INT_MAX</tt>]
</pre>
<!-- end option -->
<!-- start option random_part -->
<a name="random_part">
<pre class="my_option">
assign(random_part, <i>n</i>). % default <i>n</i>=0, range [0 .. <tt>INT_MAX</tt>]
</pre>
<!-- end option -->
<!-- start option hints_part -->
<a name="hints_part">
<pre class="my_option">
assign(hints_part, <i>n</i>). % default <i>n</i>=<tt>INT_MAX</tt>, range [0 .. <tt>INT_MAX</tt>]
</pre>
<!-- end option -->
<blockquote>
These six parameters work together to specify a 6-way ratio for
selection of the given clauses:
<ul>
<li><a href="select.html#age_part"><tt><b>age_part</b></tt></a>
refers to the clause with lowest ID (the oldest clause),
<li><a href="select.html#weight_part"><tt><b>weight_part</b></tt></a>
refers to the (oldest) clause with
<a href="weight.html">lowest weight</a>,
<li><a href="select.html#false_part"><tt><b>false_part</b></tt></a>
refers to the (oldest) lightest <i>false</i> clause,
<li><a href="select.html#true_part"><tt><b>true_part</b></tt></a>
refers to the (oldest) lightest <i>true</i> clause,
<li><a href="select.html#random_part"><tt><b>random_part</b></tt></a>
refers to a (pseudo-) <i>random</i> clause,
<li><a href="select.html#hints_part"><tt><b>hints_part</b></tt></a>
refers to the lightest clause that
<a href="hints.html">matches a hint</a>.
</ul>
The <i>false/true</i> distinction is determined by a set of interpretations.
The default interpretation is that negative clauses are false
and non-negative clauses are true. To use explicit interpretations,
see the <a href="semantics.html">section on semantic guidance</a>.
<p>
Under the default interpretation, for example, if
<a href="select.html#age_part"><tt><b>age_part</b></tt></a> = 1,
<a href="select.html#false_part"><tt><b>false_part</b></tt></a> = 2, and
<a href="select.html#true_part"><tt><b>true_part</b></tt></a> = 3,
given clauses will be selected in a cycle of size six: one clause
by lowest ID, then two clauses because they are the lightest
negative (i.e., false) clauses, then three clauses because they are the
lightest non-negative (i.e., true) clauses. And so on.
<p>
If a clause of required type is not available, that component of
the ratio is simply skipped. For example, with ratio in the
preceding paragraph, if no false clauses are available, the
cycle has size four (one part age, 3 parts true clauses)
until some false clauses become available.
<p>
Note that the default value of
<a href="select.html#hints_part"><tt><b>hints_part</b></tt></a>
is <tt>INT_MAX</tt>. This means that whenever the selection cycle
gets to the
<a href="select.html#hints_part"><tt><b>hints_part</b></tt></a>,
<a href="hints.html">clauses that match hints</a>
will be selected as long as any are available.
</blockquote>
<!-- end option -->
<p>
When a given clause is printed, its sequence number, the reason
it was selected, its weight, and its ID are also shown as in the following
excerpt.
<pre class="my_file">
given #1 (I,wt=7): 9 x v y = y v x. [input].
<font color="red">...</font>
given #18 (T,wt=5): 28 x v x = x. [para(13(a,1),14(a,1,2))].
given #19 (A,wt=11): 18 x ^ (y ^ z) = y ^ (x ^ z). [para(11(a,1),12(a,1,1)),demod(12(2))].
given #20 (F,wt=21): 43 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),32(a,1,2,2))].
</pre>
The selection codes are
<tt>A</tt>=age, <tt>W</tt>=weight, <tt>F</tt>=false, <tt>T</tt>=true,
<tt>H</tt>=hints, <tt>R</tt>=random, and <tt>I</tt>=input (see flag
<a href="select.html#input_sos_first"><tt><b>input_sos_first</b></tt></a>).
<p>
More selection criteria will likely be added in future
versions of Prover9.
<h2>Other Options</h2>
<!-- start option default_parts -->
<a name="default_parts">
<pre class="my_option">
set(default_parts). % default set
clear(default_parts).
</pre>
<blockquote>
If this flag is cleared, all of the selection parts, <i>including hints</i>,
are set to 0.
If it is set, the selection parts are reset to their defaults.
This flag operates by making the following changes.
<pre>
clear(default_parts) -> assign(hints_part, 0).
clear(default_parts) -> assign(weight_part, 0).
clear(default_parts) -> assign(age_part, 0).
clear(default_parts) -> assign(false_part, 0).
clear(default_parts) -> assign(true_part, 0).
clear(default_parts) -> assign(random_part, 0).
</pre>
<pre>
set(default_parts) -> assign(hints_part, INT_MAX).
set(default_parts) -> assign(weight_part, 0).
set(default_parts) -> assign(age_part, 1).
set(default_parts) -> assign(false_part, 4).
set(default_parts) -> assign(true_part, 4).
set(default_parts) -> assign(random_part, 0).
</pre>
</blockquote>
<!-- end option -->
<!-- start option pick_given_ratio -->
<a name="pick_given_ratio">
<pre class="my_option">
assign(pick_given_ratio, <i>n</i>). % default <i>n</i>=0, range [0 .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
If <i>n</i>>0, the given clauses are chosen in the ratio
one part by age, and <i>n</i> parts by weight. The false/true
distinction is ignored.
This parameter works by making the following changes.
(Note that this parameter does not alter
<a href="select.html#hints_part"><tt><b>hints_part</b></tt></a>,
so that clauses matching hints may still be selected.)
<pre>
assign(pick_given_ratio, <i>n</i>) -> assign(age_part, 1).
assign(pick_given_ratio, <i>n</i>) -> assign(weight_part, <i>n</i>).
assign(pick_given_ratio, <i>n</i>) -> assign(false_part, 0).
assign(pick_given_ratio, <i>n</i>) -> assign(true_part, 0).
assign(pick_given_ratio, <i>n</i>) -> assign(random_part, 0).
</pre>
</blockquote>
<!-- end option -->
<!-- start option lightest_first -->
<a name="lightest_first">
<pre class="my_option">
set(lightest_first).
clear(lightest_first). % default clear
</pre>
<blockquote>
If this flag is set, the given clauses are selected by weight,
lightest first. This flag operates by making the following changes.
(Note that this flag does not alter
<a href="select.html#hints_part"><tt><b>hints_part</b></tt></a>,
so that clauses matching hints may still be selected.)
<pre>
set(lightest_first) -> assign(weight_part, 1).
set(lightest_first) -> assign(age_part, 0).
set(lightest_first) -> assign(false_part, 0).
set(lightest_first) -> assign(true_part, 0).
set(lightest_first) -> assign(random_part, 0).
</pre>
</blockquote>
<!-- end option -->
<!-- start option breadth_first -->
<a name="breadth_first">
<pre class="my_option">
set(breadth_first).
clear(breadth_first). % default clear
</pre>
<blockquote>
If this flag is set, the <tt>sos</tt> list operates as a queue,
giving a breadth-first search.
That is, the oldest clause is selected as the given clause.
This flag operates by making the following changes.
(Note that this flag does not alter
<a href="select.html#hints_part"><tt><b>hints_part</b></tt></a>,
so that clauses matching hints may still be selected.)
<pre>
set(breadth_first) -> assign(age_part, 1).
set(breadth_first) -> assign(weight_part, 0).
set(breadth_first) -> assign(false_part, 0).
set(breadth_first) -> assign(true_part, 0).
set(breadth_first) -> assign(random_part, 0).
</pre>
</blockquote>
<!-- end option -->
<!-- start option random_given -->
<a name="random_given">
<pre class="my_option">
set(random_given).
clear(random_given). % default clear
</pre>
<blockquote>
If this flag is set, a random clause is selected
from the <tt>sos</tt> list.
This flag operates by making the following changes.
(Note that this flag does not alter
<a href="select.html#hints_part"><tt><b>hints_part</b></tt></a>,
so that clauses matching hints may still be selected.)
<pre>
set(random_given) -> assign(random_part, 1).
set(random_given) -> assign(age_part, 0).
set(random_given) -> assign(weight_part, 0).
set(random_given) -> assign(false_part, 0).
set(random_given) -> assign(true_part, 0).
</pre>
</blockquote>
<!-- end option -->
<!-- start option random_seed -->
<a name="random_seed">
<pre class="my_option">
assign(random_seed, <i>n</i>). % default <i>n</i>=0, range [-1 .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter determines the seed for the (pseudo-) random number generator,
which is used for the parameter <a href="select.html#random_part"><tt><b>random_part</b></tt></a> (and maybe also for other purposes).
The system library functions <tt>rand()</tt> and <tt>srand()</tt>
are used for random number generation.
<p>
If <i>n ≥ 0</i>, it is used as the seed.
If <i>n = -1</i>, Prover9 selects a seed, based on the value of
the system clock; in this case, Prover9 jobs are not reproducibe.
</blockquote>
<!-- end option -->
<!-- start option input_sos_first -->
<a name="input_sos_first">
<pre class="my_option">
set(input_sos_first). % default set
clear(input_sos_first).
</pre>
<blockquote>
If this flag is set, the clauses in the initial <tt>sos</tt> list are selected
as given clauses (in the order in which they occur in the <tt>sos</tt> list)
before any derived clauses are selected. This flag allows heavy input clauses
to enter the search right away. After the initial clauses have been selected,
the ordinary
<a href="select.html#age_part"><tt><b>selection ratio</b></tt></a>,
takes over.
</blockquote>
<!-- end option -->
<hr>
Next Section:
<a href="inf-rules.html">Inference Rules</a>
</body>
</html>
|
