Prover9 Manual Version August-2006A

Selecting the Given Clause

At each iteration of the main loop, Prover9 selects a given clause from the sos list, moves it to the usable list, and makes inferences from it and other clauses in the usable list.

A basic way to select the given clause is to always select the lightest clause in sos. Otter has the ability to mix two methods of selecting the given clause in a ratio determined by a parameter --- selecting the lightest clause and selecting the oldest clause. This method adds a breadth-first component to the search. See the pick_given_ratio parameter below.

Prover9 uses three components, dividing the "lightest" component into two components based on semantics. The following options are used. 

assign(age_part, n).    % default n=1, range [0 .. INT_MAX]

assign(false_part, n).  % default n=2, range [0 .. INT_MAX]

assign(true_part, n).   % default n=2, range [0 .. INT_MAX]
These three parameters work together to specify a 3-way ratio for selection of the given clauses: The false/true distinction is determined by a set of interpretations. The default interpretation is that negative clauses are false non-negative clauses are true. To use explicit interpretations, see the section on semantic guidance.

Under the default interpretation, for example, if age_part = 1, false_part = 2, and true_part = 3, given clauses will be selected in a cycle of size six: one clause by lowest ID, then two clauses because they are the lightest negative (i.e., false) clauses, then three clauses because they are the lightest non-negative (i.e., true) clauses. And so on.

Anomalies:

  1. If one of false_part and true_part is 0 and the other is not, the false/true distinction disappears, and selection for that part is simply by weight.
  2. If it is time to select a false clause, and none is available, a true clause is selected instead (and vice versa). That is, we don't skip the selection of the false clause; we substitute a true one.

When a given clause is printed, its sequence number, the reason it was selected, its weight, and its ID are also shown as in the following excerpt. 

given #1  (I,wt=7): 9 x v y = y v x.  [input].
...
given #18 (T,wt=5): 28 x v x = x.  [para(13(a,1),14(a,1,2))].
given #19 (A,wt=11): 18 x ^ (y ^ z) = y ^ (x ^ z).  [para(11(a,1),12(a,1,1)),demod(12(2))].
given #20 (F,wt=21): 43 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y) # label(false).  [para(11(a,1),32(a,1,2,2))].
The selection codes are A=age, F=false, T=true, and I=input (see flag input_sos_first). Note that the selection code indicates the type of clause Prover9 attempted to select according to the ratio, and not the type of the clause that was actually selected (see the second anomaly above).

More selection criteria will likely be added in future versions of Prover9.

Other Options

assign(pick_given_ratio, n).  % default n=0, range [0 .. INT_MAX]
If n>0, the given clauses are chosen in the ratio one part by age, and n parts by weight. The false/true distinction is ignored. This parameter works by making the following changes. 
  assign(pick_given_ratio, n) -> assign(age_part, 1).
  assign(pick_given_ratio, n) -> assign(true_part, n).
  assign(pick_given_ratio, n) -> assign(false_part, 0).

set(breadth_first).
clear(breadth_first).    % default clear
If this flag is set, the sos list operates as a queue, giving a breadth-first search. That is, the oldest clause is always selected as the given clause. This flag operates by making the following changes. 
  set(breadth_first) -> assign(age_part, 1).
  set(breadth_first) -> assign(true_part, 0).
  set(breadth_first) -> assign(false_part, 0).

set(input_sos_first).    % default set
clear(input_sos_first).
If this flag is set, the clauses in the initial sos list are selected as given clauses (in the order in which they occur in the sos list) before any derived clauses are selected. This flag is useful if the input contains heavy clauses that should enter the search right away.