Prover9 Manual Version 2009-11A

Weighting

Prover9's weighting function maps clauses to integers, and it is used primarily for two purposes:
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,

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. Weighting rules are applied to a clause as follows.

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