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

Next Section: Attributes