Prover9 Manual |  | Version 2009-02A

# 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 six components in selecting the given clause. The following six options are used.

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

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

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

    assign(true_part, n).    % default n=4, range [0 .. INT_MAX]

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

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

> These six parameters work together to specify a 6-way ratio for selection of the given clauses:
> - `age_part` refers to the clause with lowest ID (the oldest clause),
> - `weight_part` refers to the (oldest) clause with lowest weight,
> - `false_part` refers to the (oldest) lightest false clause,
> - `true_part` refers to the (oldest) lightest true clause,
> - `random_part` refers to a (pseudo-) random clause,
> - `hints_part` refers to the lightest clause that matches a hint.
> The false/true distinction is determined by a set of interpretations. The default interpretation is that negative clauses are false and 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.

> If a clause of required type is not available, that component of the ratio is simply skipped. For example, with ratio in the preceding paragraph, if no false clauses are available, the cycle has size four (one part age, 3 parts true clauses) until some false clauses become available.

> Note that the default value of `hints_part` is `INT_MAX`. This means that whenever the selection cycle gets to the `hints_part`, clauses that match hints will be selected as long as any are available.

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, `W`=weight, `F`=false, `T`=true, `H`=hints, `R`=random, and `I`=input (see flag `input_sos_first`).

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

## Other Options

    set(default_parts).      % default set
    clear(default_parts).

> If this flag is cleared, all of the selection parts, including hints, are set to 0. If it is set, the selection parts are reset to their defaults. This flag operates by making the following changes.

>       clear(default_parts) -> assign(hints_part, 0).
>       clear(default_parts) -> assign(weight_part, 0).
>       clear(default_parts) -> assign(age_part, 0).
>       clear(default_parts) -> assign(false_part, 0).
>       clear(default_parts) -> assign(true_part, 0).
>       clear(default_parts) -> assign(random_part, 0).

>       set(default_parts) -> assign(hints_part, INT_MAX).
>       set(default_parts) -> assign(weight_part, 0).
>       set(default_parts) -> assign(age_part, 1).
>       set(default_parts) -> assign(false_part, 4).
>       set(default_parts) -> assign(true_part, 4).
>       set(default_parts) -> assign(random_part, 0).

    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. (Note that this parameter does not alter `hints_part`, so that clauses matching hints may still be selected.)

>       assign(pick_given_ratio, n) -> assign(age_part, 1).
>       assign(pick_given_ratio, n) -> assign(weight_part, n).
>       assign(pick_given_ratio, n) -> assign(false_part, 0).
>       assign(pick_given_ratio, n) -> assign(true_part, 0).
>       assign(pick_given_ratio, n) -> assign(random_part, 0).

    set(lightest_first).
    clear(lightest_first).    % default clear

> If this flag is set, the given clauses are selected by weight, lightest first. This flag operates by making the following changes. (Note that this flag does not alter `hints_part`, so that clauses matching hints may still be selected.)

>       set(lightest_first) -> assign(weight_part, 1).
>       set(lightest_first) -> assign(age_part, 0).
>       set(lightest_first) -> assign(false_part, 0).
>       set(lightest_first) -> assign(true_part, 0).
>       set(lightest_first) -> assign(random_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 selected as the given clause. This flag operates by making the following changes. (Note that this flag does not alter `hints_part`, so that clauses matching hints may still be selected.)

>       set(breadth_first) -> assign(age_part, 1).
>       set(breadth_first) -> assign(weight_part, 0).
>       set(breadth_first) -> assign(false_part, 0).
>       set(breadth_first) -> assign(true_part, 0).
>       set(breadth_first) -> assign(random_part, 0).

    set(random_given).
    clear(random_given).    % default clear

> If this flag is set, a random clause is selected from the `sos` list. This flag operates by making the following changes. (Note that this flag does not alter `hints_part`, so that clauses matching hints may still be selected.)

>       set(random_given) -> assign(random_part, 1).
>       set(random_given) -> assign(age_part, 0).
>       set(random_given) -> assign(weight_part, 0).
>       set(random_given) -> assign(false_part, 0).
>       set(random_given) -> assign(true_part, 0).

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

> This parameter determines the seed for the (pseudo-) random number generator, which is used for the parameter `random_part` (and maybe also for other purposes). The system library functions `rand()` and `srand()` are used for random number generation.

> If n ≥ 0, it is used as the seed. If n = -1, Prover9 selects a seed, based on the value of the system clock; in this case, Prover9 jobs are not reproducibe.

    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 allows heavy input clauses to enter the search right away. After the initial clauses have been selected, the ordinary `selection ratio`, takes over.

Next Section: Inference Rules