Weighting
Prover9's weighting function maps clauses to integers, and
it is used primarily for two purposes:
- selecting the given clause, and
- discarding inferred clauses (with the parameter max_weight).
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.
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.
Prover9 does not (yet) have anything analogous to Otter's $DOTS weighting feature.
Default Weights
The default weight of a clause is its symbol count,
excluding commas, parentheses, negation symbols, and disjunction symbols.
That is,
- the default weight of a constant or variable is 1,
- the default weight of a term or atomic formula is one more
than the sum of the weights of its arguments,
- the default weight of a literal is the weight of its atomic formula,
- the default weight of a clause is the sum of the weights of its literals.
Weighting Rules
The weighting function can be modified by giving a list of rules
in the input file. The list must start with
list(weights).
and end with
end_of_list.
Here is an example.
list(weights).
weight(a) = 3. % the weight of the constant a is 3
weight(f(a,x)) = 5 * weight(x). % weight( f(a,term) ) = 5 * weight( term )
weight(f(a,_)) = -1. % _ matches any variable
weight(x | y) = 2 + (weight(x) + weight(y)). % add 2 for each "or" symbol
end_of_list.
Here is a summary of the weighting language.
- Each weighting rule is an equation.
The left-hand side of the rule must be weight(pattern).
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.
- The right-hand side of a rule consists of an integer-arithmetic
expression applied to weight(...) terms.
When applying a rule, the substitution of the pattern match
is applied to the the weight(...) 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.
- The accepted integer operations are
- binary: {+, *, /, min, max}
- unary: {-, depth, vars}
The depth operation gives the depth (height) of the term
(when viewed as a tree), and the vars operation gives the number of
(distinct) variables in the term.
-
The rules are parsed with the ordinary term-parsing code,
so (unless the user as included an op command
to change the parsing rules), the arithmetic expressions
must be fully parenthesized, e.g., a + (b + c).
Weighting rules are applied to a clause as follows.
- The clause is weighed top-down. That is, a term is weighed
before its subterms are weighed.
- When weighing a term, the first rule that matches is applied.
- If no rule matches, the weight of the term is one more than
the sum of the weights of its arguments.
Modifying the Default Weight
assign(constant_weight, n). % default n=1, range [INT_MIN .. INT_MAX]
This parameter specifies the default weight of constants.
It can be overridden with weighting rules for individual constants.
assign(sk_constant_weight, n). % default n=1, range [INT_MIN .. INT_MAX]
This parameter specifies the default weight of Skolem constants.
It takes precedence over constant_weight.
assign(variable_weight, n). % default n=1, range [INT_MIN .. INT_MAX]
This parameter specifies the default weight of variables.
assign(not_weight, n). % default n=0, range [INT_MIN .. INT_MAX]
The negation symbols on literals
do not ordinarily contribute any weight to clauses.
This parameter says that each negation symbol has weight n.
assign(or_weight, n). % default n=0, range [INT_MIN .. INT_MAX]
The disjunction symbols between literals
do not ordinarily contribute any weight to clauses.
This parameter says that each disjunction symbol has weight n.
assign(prop_atom_weight, n). % default n=1, range [INT_MIN .. INT_MAX]
This parameter specifies the default weight for propositional atoms, that is,
predicate symbols of arity 0. They ordinarily have weight 1.
assign(nest_penalty, n). % default n=0, range [0 .. INT_MAX]
This parameter is used to penalize terms containing nested function symbols.
If no weighting rule applies to a term t, then for each argument
with the same function symbol as t, the value n is added to
the weight of t. If n=0, there is no penalty.
assign(depth_penalty, n). % default n=0, range [INT_MIN .. INT_MAX]
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 C is increased by
n * depth(C).
Note that n may be negative, decreasing the weight of the clause.
assign(var_penalty, n). % default n=0, range [INT_MIN .. INT_MAX]
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 v is the number of (distinct) variable in the clause,
the weight of the clause is increased by
n * v.
Note that n may be negative, decreasing the weight of the clause.
Adjustments to Clause Weight
The final weight of a clause is calculated in three steps.
First, the weighting rules are applied.
Second, if the weight is greater than
default_weight
and
less than
max_weight,
the weight is reset to
default_weight.
assign(default_weight, n). % default n=INT_MAX, range [INT_MIN .. INT_MAX]
That is, all clauses with weight from
default_weight
up to max_weight
are treated equally.
Third, if the clause matches a hint,
the weight may be adjusted by the flag
degrade_hints and
by the hint attribute
bsub_hint_wt.
Debugging Weighting Rules and Options
Here is an example of using Prover9 to test weighting rules and parameters.
prover9 -f weight_test.in | grep 'given #' > weight_test.out