/usr/share/doc/prover9-doc/html/weight.html is in prover9-doc 0.0.200902a-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Weighting</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>Weighting</h1>
Prover9's weighting function maps clauses to integers, and
it is used primarily for two purposes:
<ul>
<li>selecting the given clause, and
<li>discarding inferred clauses (with the parameter <a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a>).
</ul>
<blockquote class="otter_diff">
Otter accepts two weighting functions, one for selecting the
given clause, and the other for discarding inferred clauses.
Prover9 always uses the same weighting function for both
purposes.
</blockquote>
<blockquote class="otter_diff">
In Otter's weighting rules, a variable matches any variable
and only variables. The role is similar to the anonymous variables "_"
in Prover9's weighting rules.
</blockquote>
<blockquote class="otter_diff">
Prover9 does not (yet) have anything analogous to Otter's <tt>$DOTS</tt> weighting feature.
</blockquote>
<h2>Default Weights</h2>
The default weight of a clause is its symbol count,
excluding commas, parentheses, negation symbols, and disjunction symbols.
That is,
<ul>
<li>the default weight of a constant or variable is 1,
<li>the default weight of a term or atomic formula is one more
than the sum of the weights of its arguments,
<li>the default weight of a literal is the weight of its atomic formula,
<li>the default weight of a clause is the sum of the weights of its literals.
</ul>
<h2>Weighting Rules</h2>
The weighting function can be modified by giving a list of rules
in the input file. The list must start with <tt>list(weights).</tt>
and end with <tt>end_of_list</tt>.
Here is an example.
<pre class="my_file">
list(weights).
weight(a) = 3. % the weight of the constant a is 3
weight(f(a,x)) = 5 * weight(x). % weight( f(a,<i>term</i>) ) = 5 * weight( <i>term</i> )
weight(f(a,_)) = -1. % _ matches any variable
weight(x | y) = 2 + (weight(x) + weight(y)). % add 2 for each "or" symbol
end_of_list.
</pre>
Here is a summary of the weighting language.
<ul>
<li>Each weighting rule is an equation.
The left-hand side of the rule must be <tt>weight(<i>pattern</i>)</tt>.
A rule applies to a term if its pattern matches the term in the ordinary sense of
demodulation or term rewriting. An exception is that the
symbol "_" matches any variable and only a variable.
<li>The right-hand side of a rule consists of an integer-arithmetic
expression applied to <tt>weight(...)</tt> terms.
When applying a rule, the substitution of the pattern match
is applied to the the <tt>weight(...)</tt> terms, which are
then weighed recursively, and then the integer expression is
evaluated to compute the weight of the term. The user is responsible
for making sure any recursion terminates.
<li>The accepted integer operations are
<ul>
<li>binary: {<tt>+, *, /, min, max</tt>}
<li>unary: {<tt>-, depth, vars</tt>}
</ul>
The <tt>depth</tt> operation gives the depth (height) of the term
(when viewed as a tree), and the <tt>vars</tt> operation gives the number of
(distinct) variables in the term.
<li>
The rules are parsed with the ordinary term-parsing code,
so (unless the user as included an <tt>op</tt> command
to change the parsing rules), the arithmetic expressions
must be fully parenthesized, e.g., <tt>a + (b + c)</tt>.
</ul>
Weighting rules are applied to a clause as follows.
<ul>
<li>The clause is weighed top-down. That is, a term is weighed
before its subterms are weighed.
<li>When weighing a term, the first rule that matches is applied.
<li>If no rule matches, the weight of the term is one more than
the sum of the weights of its arguments.
</ul>
<h2>Modifying the Default Weight</h2>
<!-- start option constant_weight -->
<a name="constant_weight">
<pre class="my_option">
assign(constant_weight, <i>n</i>). % default <i>n</i>=1, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter specifies the default weight of constants.
It can be overridden with weighting rules for individual constants.
</blockquote>
<!-- end option -->
<!-- start option constant_weight -->
<a name="sk_constant_weight">
<pre class="my_option">
assign(sk_constant_weight, <i>n</i>). % default <i>n</i>=1, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter specifies the default weight of <a href="glossary.html#skolemization">Skolem constant</a>s.
It takes precedence over <a href="weight.html#constant_weight"><tt><b>constant_weight</b></tt></a>.
</blockquote>
<!-- end option -->
<!-- start option variable_weight -->
<a name="variable_weight">
<pre class="my_option">
assign(variable_weight, <i>n</i>). % default <i>n</i>=1, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter specifies the default weight of variables.
</blockquote>
<!-- end option -->
<!-- start option not_weight -->
<a name="not_weight">
<pre class="my_option">
assign(not_weight, <i>n</i>). % default <i>n</i>=0, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
The negation symbols on literals
do not ordinarily contribute any weight to clauses.
This parameter says that each negation symbol has weight <i>n</i>.
</blockquote>
<!-- end option -->
<!-- start option or_weight -->
<a name="or_weight">
<pre class="my_option">
assign(or_weight, <i>n</i>). % default <i>n</i>=0, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
The disjunction symbols between literals
do not ordinarily contribute any weight to clauses.
This parameter says that each disjunction symbol has weight <i>n</i>.
</blockquote>
<!-- end option -->
<!-- start option prop_atom_weight -->
<a name="prop_atom_weight">
<pre class="my_option">
assign(prop_atom_weight, <i>n</i>). % default <i>n</i>=1, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter specifies the default weight for propositional atoms, that is,
predicate symbols of arity 0. They ordinarily have weight 1.
</blockquote>
<!-- end option -->
<!-- start option nest_penalty -->
<a name="nest_penalty">
<pre class="my_option">
assign(nest_penalty, <i>n</i>). % default <i>n</i>=0, range [0 .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter is used to penalize terms containing nested function symbols.
If no weighting rule applies to a term <i>t</i>, then for each argument
with the same function symbol as <i>t</i>, the value <i>n</i> is added to
the weight of <i>t</i>. If <i>n</i>=0, there is no penalty.
</blockquote>
<!-- end option -->
<!-- start option depth_penalty -->
<a name="depth_penalty">
<pre class="my_option">
assign(depth_penalty, <i>n</i>). % default <i>n</i>=0, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter is used to penalize (or prefer) clauses with deeper terms.
It is applied to the
entire clause after all of the literals and subterms have been weighed.
The weight of the clause <i>C</i> is increased by
<i>n * <a href="glossary.html#depth-C">depth(C)</a></i>.
Note that <i>n</i> may be negative, decreasing the weight of the clause.
</blockquote>
<!-- end option -->
<!-- start option var_penalty -->
<a name="var_penalty">
<pre class="my_option">
assign(var_penalty, <i>n</i>). % default <i>n</i>=0, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter is used to penalize (or prefer) clauses with more variables.
It is applied to the entire clause after all of the literals and
subterms have been weighed.
If <i>v</i> is the number of (distinct) variable in the clause,
the weight of the clause is increased by
<i>n * v</i>.
Note that <i>n</i> may be negative, decreasing the weight of the clause.
</blockquote>
<!-- end option -->
<h2>Adjustments to Clause Weight</h2>
The final weight of a clause is calculated in three steps.
First, the weighting rules are applied.
Second, if the weight is greater than
<a href="weight.html#default_weight"><tt><b>default_weight</b></tt></a>
and
less than
<a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a>,
the weight is reset to
<a href="weight.html#default_weight"><tt><b>default_weight</b></tt></a>.
<!-- start option default_weight -->
<a name="default_weight">
<pre class="my_option">
assign(default_weight, <i>n</i>). % default <i>n</i>=<tt>INT_MAX</tt>, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
That is, all clauses with weight from
<a href="weight.html#default_weight"><tt><b>default_weight</b></tt></a>
up to <a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a>
are treated equally.
</blockquote>
<!-- end option -->
Third, if the clause <a href="hints.html"</a> matches a hint</a>,
the weight may be adjusted by the flag <a href="hints.html#degrade_hints"><tt><b>degrade_hints</b></tt></a> and
by the hint attribute <tt>bsub_hint_wt</tt>.
<h2>Debugging Weighting Rules and Options</h2>
Here is an example of using Prover9 to test weighting rules and parameters.
<pre class="my_job">
prover9 -f <a href="../examples/weight_test.in">weight_test.in</a> | grep 'given #' > <a href="../examples/weight_test.out">weight_test.out</a>
</pre>
<hr>
Next Section:
<a href="attributes.html">Attributes</a>
</body>
</html>
|