Given Selection (Advanced)

This page describes a mechanism that allows the user to have more control over selection of given clauses than the ordinary parameters age_part, true_part, false_part, weight_part, hints_part, and random_part. (See the page Selecting the Given Clause for the basic mechanism.)

The user can input a list "given_selection" rules that specify how given clauses are to be selected. Each rule has the form

part( name, priority, order , property ) = n.

name is an identifier string chosen by the user; it is used when given clauses are printed to identify the rule that was used to select the given clause.
priority must be "high" or "low"; All high-priority rules are used before any low-priority rules are used.
order must be "age" (increasing clause ID), "weight" (increasing clause weight), or "random"; it is used to order the clauses that satisfy the property.
property is an expression in the Clause Properties language.
n is a positive integer; it specifies the number of given clauses that are selected according to the rule before moving to the next rule.

For example the default settings (see Selecting the Given Clause)

assign(hints_part, INT_MAX).
assign(age_part, 1).
assign(true_part, 4).
assign(false_part, 4).

are operationally similar to the following list of rules.

list(given_selection).
  part(H, high, weight,  hint) = 1.
  part(A,  low,    age,   all) = 1.
  part(T,  low, weight,  true) = 4.
  part(F,  low, weight, false) = 4.
end_of_list.

Selection by Ratio

Ignore high-priority rules for a moment and consider a list of low-priority rules. The positive integers (the parts) at the ends of the rules determine a ratio cycle. If there are three rules with parts 3,1,4, the cycle has size 8, with 3 clauses selected by the first rule, 1 clause by the second rule, 4 by the third rule, and so on. The ratio cycle is [3,1,4]. If no clauses of the required type are available, that part of the cycle is simply skipped. This much is essentially the same as the basic method described in Selecting the Given Clause.

Priority: High and Low

The given_selection rules are partitioned into "high" and "low" priority, and each partition determines a ratio cycle.

When Prover9 needs a new given clause, it first tries to find one by using the high-priority rules, picking up in the high-priority cycle where it left off. Consider the following rules.

list(given_selection).
  part(Hint_age,  high,    age,        hint) = 2.
  part(Hint_wt,   high, weight,        hint) = 3.

  part(Age,        low,    age,         all) = 1.
  part(Pos,        low, weight,    positive) = 2.
  part(Nonpos,     low, weight,   -positive) = 4.
end_of_list.

As long as clauses matching hints are available, they are selected in a cycle of size 5: 2 by age, then 3 by weight, and so on. When no more clauses matching hints are available, Prover9 reverts to the low-priority rules, selecting given clauses in a cycle of size 7. If any high-priority clauses become available, Prover9 immediately goes back to the high-priority cycle.

Covering All Clauses

We recommend that the list of rules cover all clauses that Prover9 keeps. (A rule with property "all" is sufficient, but not necessary.) If a kept clause does not match any of the rules, a warning message is printed. In this case, there can be sos clauses that will never be selectedas. (It is possible that such clauses can still be used by subsumption, back demodulation, or back unit deletion.)

The Ordinary Selection Parameters (`age_part`, etc.)

The ordinary parameters age_part, true_part, false_part, weight_part, hints_part, and random_part can be thought of as shorthand for given_selection rules. In fact, if the user does not input a list of given_selection rules, Prover9 constructs and uses an internal given_selection list by using those parameters.

However, if the user does input given_selection rules, those five parameters are ignored. In particular, if the user inputs given_selection rules, and if hints are being used, there probably should be (at least) a high_priority rule with property "hint" so that the hints will be used.

Input_sos_first

The flag input_sos_first (default set) says that all initial clauses (sos clauses that exist when the first given clause is selected) are to be selected as give clauses before any non-initial clauses. This flag is implemented with a high-priority rule.

Contrary to the hints case, if the user inputs given_selection rules, and if the flag input_sos_first, Prover9 will automatically insert the following rule as the first high-priority rule.

  part(I, high, age, initial) = INT_MAX.

If the user wishes to override this behavior, for example by having initial clauses selected immediately by weight instead of age, the flag input_sos_first can be cleared, and the following can be used as the first high-priority rule.