Prover9 Manual		Version 2009-02A

Automatic Modes

Prover9's automatic mode is set by default. Otter's automatic mode must be explicitly set.

If you simply give Prover9 a set of clauses and/or formulas, Prover9 will look at the clauses and decide which inference rules and clause-processing operations to use. If you don't like the automatic decisions that Prover9 makes, you can clear the flag auto or any of the secondary auto flags that depend on it. Prover9 output files show in detail the effects of changing these flags.

set(auto).    % default set
clear(auto).

This is the basic automatic mode of Prover9. The only direct effect of this flag is that it changes four secondary auto flags as follows.

  set(auto) -> set(auto_inference).
  set(auto) -> set(auto_process).
  set(auto) -> set(auto_setup).
  set(auto) -> set(auto_limits).
  set(auto) -> set(auto_denials).

  clear(auto) -> clear(auto_inference).
  clear(auto) -> clear(auto_process).
  clear(auto) -> clear(auto_setup).
  clear(auto) -> clear(auto_limits).
  clear(auto) -> clear(auto_denials).

Any of the secondary flags, as well as the entire automatic mode can be cleared by the user.

set(auto_inference).    % default set
clear(auto_inference).

If this flag is set, the input clauses are checked for several syntactic properties such as the presence of equality and non-Horn clauses. Based on the results of the checks, Prover9 decides which inference rules to use.

Unlike ordinary option dependencies, the options that are changed by auto_inference cannot be undone by placing commands in the input file, because they depend on the structure of the clauses.

set(auto_process).    % default set
clear(auto_process).

This flag causes several other flags that affect clause processing to be altered based syntactic properties of the initial clauses.

If all clauses are Horn and there are negative nonunits, the flag back_unit_deletion is automatically set. If there are non-Horn clauses, the flags back_unit_deletion and factor are automatically set.

Unlike ordinary option dependencies, the options that are changed by auto_process cannot be undone by placing commands in the input file, because they depend on the structure of the clauses.

set(auto_setup).    % default set
clear(auto_setup).

The only effect of changing this flag is that two parameters are changed in the following ways.

  set(auto_setup) -> set(predicate_elim).
  set(auto_setup) -> assign(eq_defs, unfold).

  clear(auto_setup) -> clear(predicate_elim).
  clear(auto_setup) -> assign(eq_defs, pass).

set(auto_limits).    % default set
clear(auto_limits).

The only effect of changing this flag is that two parameters are changed in the following ways.

  set(auto_limits) -> assign(max_weight, 100).
  set(auto_limits) -> assign(sos_limit, 10000).

  clear(auto_limits) -> assign(max_weight, INT_MAX).
  clear(auto_limits) -> assign(sos_limit, -1).

An Experimental Automatic Mode

set(auto2).
clear(auto2).    % default clear

Automatically Adjusting the sos_limit Parameter

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

assign(lrs_interval, n).  % default n=50, range [1 .. INT_MAX]

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

These three parameters work together and are used to automatically adjust the parameter sos_limit by means of a "limited resource strategy" [RV-lrs]. If lrs_ticks ≥ 0, the method is applied.

This is an experimental feature and is not recommended for general use.

Raw Mode

set(raw).
clear(raw).    % default clear

This is a sort of anti-automatic mode, which allows the user to completely specify the search strategy, with less chance of interference from the default settings of various options. For example, to generate all binary resolvents, one can simply set the flags raw and binary_resolution instead of finding and clearing the flags that restrict resolution.

The flag works by making the following changes.

   set(raw) -> clear(auto).
   clear(auto) -> clear(auto_inference).
   clear(auto) -> clear(auto_setup).
   clear(auto_setup) -> clear(predicate_elim).
   clear(auto_setup) -> assign(eq_defs, pass).
   clear(auto) -> clear(auto_limits).
   clear(auto_limits) -> assign(max_weight, 2147483647).
   clear(auto_limits) -> assign(sos_limit, -1).
   clear(auto) -> clear(auto_denials).
   clear(auto) -> clear(auto_process).
   set(raw) -> clear(ordered_res).
   set(raw) -> clear(ordered_para).
   set(raw) -> assign(literal_selection, none).
   set(raw) -> clear(back_demod).
   set(raw) -> clear(cac_redundancy).
   set(raw) -> assign(backsub_check, 2147483647).
   set(raw) -> set(lightest_first).
   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).