Processing Inferred Clauses

Processing of inferred clauses is separated into two stages: (1) simplifying the clause and deciding whether to keep it, and if it is kept, (2) using the clause to operate on other clauses.

Processing Initial Clauses

Initial clauses in the sos list are processed, for the most part, as if they were derived by some inference rule. This process helps to ensure that Prover9's working set of clauses starts out in a good state, in particular, that no clause subsumes another, and that all clauses are simplified according to the working set of demodulators. Note the following exceptions.

The main exceptions to processing initial clauses is that the parameters max_literals, max_vars, max_weight, and max_depth are not applied.
All processing of initial sos clauses can be disabled by clearing the flag process_initial_sos.
Clauses in the initial usable list are never processed.
If there is an initial demodulators list, the clauses therein will be checked. If an equation is orientable but backward, it will be flipped, and a warning message will be printed. Otherwise, it must satisfy all of the ordinary constraints on demodulators. Having an initial demodulators list is useful, along with clearing the flag back_demod, if the user wishes to have a set of demodulators that is fixed throughout the search.

Algorithm for Processing Clauses

Processing initial and inferred clauses.

Start with clause c:
    1.  Simplify c:
        1a.  demodulate
	1b.  orient equalities
	1c.  simplify literals
        1d.  merge identical literals
	1e.  unit_deletion
	1f.  cac_redundancy
    2.  safe_unit_conflict check
    3.  max_literals, max_depth, max_vars, max_weight checks
    4.  evaluate for semantic selection
    5.  sos_limit check
    6.  subsumption check (forward)
    7.  assign an ID and keep the clause
    8.  unsafe unit conflict check
    9.  check if the clause should be a demodulator
    ---- (the following steps are delayed until finished with the given clause) ---
    10. factor c
    11. apply new_constants to c
    12. apply back_subsume with c
    13. apply back_demod with c
    14. apply back_unit_deletion with c
    15. move c to the sos list

Restricted denials (see flag restrict_denials) are not subject to the max_weight test.

Options for Processing Inferred Clauses

Demodulation Options

Dedmodulation is the process of using equations (demodulators) to rewrite terms. If a demodulator is oriented by the term ordering in effect (KBO, LPO, or RPO), it is applied unconditionally, heavy-to-light. If a demodulator is not oriented, it is applied only if the instance that would be used is oriented.

set(lex_order_vars).
clear(lex_order_vars).    % default clear

This flag allows an exception to the rule for applying nonorientable demodulators. If the flag is set, variables are treated as constants when comparing terms, with the precedence
function_order([x,y,z,u,v,w,v6,v7,v8, ...]).
That is, variables are smaller than any other symbols.
For example, with the (nonorientable) demodulator x*y = y*x, the term v7*v6 can be rewritten to v6*v7. Setting this flag can easily block proofs, but it can also drastically reduce the search space and still allow some proofs to be found.
If you have a difficult problem that involves a commutative, associative-commutative, or some other permutative operation, we recommend trying this option.

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

This parameter limits the number of rewrite steps that are applied to a clause during demodulation. If n=-1, there is no limit.

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

This parameter limits the amount (measured as symbol count) that demodulation can increase the size of a clause. If n=-1, there is no limit.

set(back_demod).      % default set
clear(back_demod).

If this flag is set, back demodulation is applied. If an orientable equation is derived, it is appended to the demodulators list. Non-orientable equations are appended based on the settings of the flags lex_dep_demod and lex_dep_demod_sane and the parameter lex_dep_demod_lim.
If an equation is added to demodulators, Then each clause in usable or sos that can be rewritten with the equation is copied and deleted, then the copy is treated as if it were generated by an inference rule. In particular, it will be processed, including demodulation, which will apply the new demodulator.

set(ac_demod).
clear(ac_demod).    % default clear

This flag says whether equations containing AC symbols may be used as demodulators.
By default they may not. When AC symbols are declared, an AC equation is used for paramodulation only, and no AC equation is adopted into the demodulators list. If this flag is set, an AC equation that is oriented by the AC-compatible ordering is adopted as a demodulator. Such equations are always adopted as oriented demodulators; the lex-dependent demodulator types (see lex_dep_demod) are not AC-compatible and are never used for AC equations.
The flag is clear by default because AC demodulators combined with AC matching can flood a search with large rewrite chains. The parameter ac_demod_weight can be used to keep AC demodulation gentler.
This flag has an effect only when at least one symbol has been declared associative-commutative.

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

If n is not -1, an AC equation is adopted as a demodulator only if its symbol count is at most n. If n is -1 (the default), there is no bound, and every oriented AC equation is adopted.
An equation that is not adopted is still used for paramodulation; it simply is not used to rewrite. Bounding the size of AC demodulators gives fewer and smaller demodulators, and less back-demodulation churn.
This parameter has an effect only when ac_demod is set.

set(ac_back_demod).
clear(ac_back_demod).    % default clear

This flag makes back demodulation aware of AC symbols.
When a new demodulator is derived, Prover9 ordinarily looks for clauses to rewrite using an ordinary (syntactic) match. In a problem with AC symbols, that misses clauses containing a term that matches the new demodulator only modulo associativity and commutativity. If this flag is set, the search for clauses to back demodulate is performed modulo AC instead, so those clauses are found and rewritten.
This flag has an effect only when all of the following hold:

at least one symbol has been declared associative-commutative;
back_demod is set (the default);
ac_demod is set (it is clear by default).
The last condition is easy to overlook. With ac_demod clear, no AC equation is ever adopted as a demodulator, so back demodulation never runs at all in an AC problem, and this flag has nothing to do. Setting ac_back_demod by itself changes nothing.
Matching modulo AC is more expensive than syntactic matching, which is why the flag is clear by default. It is worth trying on problems in which AC symbols appear in many kept clauses, and in which back demodulation is doing useful work.

set(lex_dep_demod).    % default set
clear(lex_dep_demod).

If this flag is set, then non-orientable equations can become demodulators (via the flag back_demod).

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

This parameter is a limit on the flag lex_dep_demod. A non-orientable equation cannot become a demodulator if it has more than n symbols. (The equation (x*y)*z=x*(y*z) has 11 symbols.) If n = -1, there is no limit.

set(lex_dep_demod_sane).    % default set
clear(lex_dep_demod_sane).

This flag is a restriction on the flag lex_dep_demod. If set, a non-orientable equation can become a demodulator only if its two sides have the same number of symbols.

set(otter_style_demod).
clear(otter_style_demod).    % default clear

This flag makes demodulation behave the way it does in Otter, so that demodulator sets written for Otter can be used with Prover9.
Otter does not distinguish predicate symbols from function symbols, so Otter demodulator sets commonly contain rules such as t(junk) = $T, which rewrite an atomic formula to $T. Prover9 ordinarily rejects such input, because it uses a symbol as either a relation symbol or a function symbol, but not both. Setting this flag relaxes that check, and the related check on symbols used with more than one arity.
In addition, when this flag is set, a positive literal whose argument has been rewritten to contain junk is replaced with $T, so that the ordinary tautology check deletes the clause. This reproduces Otter's treatment of junk terms.
Use this flag only when you are porting an Otter demodulator set. The relaxed checks mean that genuine input errors of these two kinds will no longer be reported.

set(unit_deletion).
clear(unit_deletion).    % default clear

This flag extends demodulation to include rewriting of literals with unit clauses. For example, if we have the unit clause p(x,a), then we can use it to remove instances of -p(x,a) from generated clauses. This process is like using the unit clause as the demodulator p(x,a) = TRUE. (Unit deletion is not actually implemented as demodulation.) This flag also causes back unit deletion to occur, that is, new unit clauses are used to remove literals from older clauses.

Simplifying and Deciding Whether to Keep Clauses

The options in this section appear in the order in which they are applied.

set(cac_redundancy).    % default set
clear(cac_redundancy).

If this flag is set, then an equational redundancy criterion is applied. If Prover9 finds that a binary operation is commutative or associative-commutative, it makes a note and uses that information to simplify clauses that are derived later in the search.
If a derived clause contains an equality alpha=beta, in which alpha and beta are equal with respect to commutativity or associativity-commutativity of the previously noted operations, the equality is simplified to TRUE.
For example, if Prover9 notes that x*y=y*x, and then some time later a clause containing the literal g(u*v)=g(v*u) is derived, that literal will be simplified to TRUE and the clause will be deleted. (Demodulation will not rewrite the two sides to the same term unless the flag lex_dep_demod is set.)

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

Clauses containing more than n literals will be deleted. If = -1, there is no limit. This parameter is never applied to initial clauses or to clauses that match hints.

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

If the depth of the clause is more than n, it will be deleted. If = -1, there is no limit. This parameter is never applied to initial clauses or to clauses that match hints.

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

Clauses containing more than n (distinct) variables will be deleted. If = -1, there is no limit. This parameter is never applied to initial clauses or to clauses that match hints.

assign(max_weight, n).  % default n=100.0, range [-DBL_MAX .. DBL_MAX]

Derived clauses with weight greater then n will be discarded. For this parameter, -1 does not mean infinity, because -1 is a reasonable value (clauses can have negative weights). This parameter is never applied to initial clauses, and it is not applied to clauses that match hints unless the flag limit_hint_matchers is set.

set(safe_unit_conflict).
clear(safe_unit_conflict).    % default clear

This flag provides for a safe, but more expensive, unit conflict test. If set, the unit conflict test will be done before the max_weight test is applied. If the flag is clear, the test will be done after the max_weight test is applied, allowing the possibility that a proof will be missed, because the final step was deleted by the max_weight parameter.

Performing Operations with the New Clause

The options in this section appear in the order in which they are applied.

set(factor).
clear(factor).    % default clear

If this flag is set, binary factoring is applied to newly-kept clauses. Note that factoring is an inference rule rather than a simplification rule, because a child is generated and the parent is retained. (If the child happens to subsume the parent, the parent will be deleted by the back subsumption process). Unlike other inference rules such as resolution, factoring is applied to a clause when it is kept, not when it is given.

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

If this parameter is greater than 0, Prover9 will apply a rule that introduces a new constant when it derives an equation that shows the existence of a constant. In particular, if a derived equation has the property that each side has exactly one variable and those two variables are different, a new constant will be introduced and set equal to one side of the equation. (Back demodulation will derive that the constant is equal to the other side.)
For example, if x' * x = y * y' is derived, the equation x' * x = c is produced, where the constant c does not occur anywhere else.
The value of the parameter limits the number of new constants that can be introduced by this rule.
(There is a more general rule allowing multiple variables. Also, there is an extension to the rule that introduces (non-constant) function symbols based on the intersection of the variables of the two sides. We have not found these extensions to be useful in practice, so we have not included them in Prover9.)
Unlike other inference rules such as resolution, the new_constants rule is applied to a clause when it is kept, not when it is given.

set(back_subsume).    % default set
clear(back_subsume).

If this flag is set, then back subsumption is applied with all new clauses. That is, when a new clause is kept, each clause subsumed by the new clause is deleted.

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

Back subsumption can be an expensive operation. This parameter tells Prover9 to check (once during the search) whether back subsmption is removing enough clauses to justify its use.
When the number of given clauses reaches this parameter, Prover9 will calculate the percentage of kept clauses that have been back subsumed; if it is less than 5%, back subsumption will be disabled.

set(ancestor_subsume).
clear(ancestor_subsume).    % default clear

This flag enables Otter's ancestor subsumption refinement, which changes what happens when two clauses are alphabetic variants of each other (that is, when each subsumes the other).
Ordinarily the older clause simply wins. If this flag is set, the two derivations are compared instead, and the subsumption is blocked if the clause that would be deleted has the strictly shorter derivation. The effect is to keep the copy of a clause that was reached by the cheaper route, which matters when one is searching for short proofs. The refinement is applied to both forward and back subsumption.
Blocking a subsumption is always sound; at worst it retains some redundant clauses, at a cost in performance.
By default, the cost of a derivation is its proof length (the number of distinct ancestors). The flag proof_weight (default clear) changes the metric to the number of input-clause leaves in the proof tree, counting shared ancestors each time they are used. This flag has no effect unless ancestor_subsume is also set.
When print_kept is set, blocked back subsumptions are reported in the output file.

Indexing (Expert)

Prover9 uses several indexes to find candidate clauses quickly: discrimination trees for demodulation and forward subsumption, and FPA/path indexes for resolution, paramodulation, and back subsumption. As an index node acquires many children, a linear scan of those children becomes the bottleneck, so a node may switch to a hash table once it has enough of them.

The two parameters below set those switch-over points. They are experimental, and intended for expert users tuning an individual problem. They affect only how long the search takes, never which clauses are derived or whether a proof is found. The defaults are appropriate for nearly all problems, and there is no general rule for choosing better values — they have to be found by experiment on the problem at hand. Large problems, with many demodulators or many kept clauses, are the ones most likely to benefit.

assign(fpa_hash_threshold, n).  % default n=4, range [0 .. 1000]

The number of children at which a node of an FPA index switches to a hash table. Lower values hash sooner, which costs memory and gains lookup speed; higher values keep the linear scan longer. FPA hashing is compiled in by default, so this parameter takes effect in a standard build.
This parameter applies to all of the FPA indexes. The separate parameter hints_fpa_depth controls the depth of the hint index, which is a different setting.

assign(discrim_hash_threshold, n).  % default n=-1, range [-1 .. 1000]

The number of children at which a node of a discrimination tree switches to a hash table. If n is -1 (the default), the nodes never switch and the linear scan is always used.
This parameter requires a special build. Discrimination-tree hashing is disabled at compile time in the standard build, because its overhead generally outweighs its benefit. In a standard build the parameter is accepted but has no effect. To enable it, rebuild with
make all XFLAGS=-DDISCRIM_HASH
See Index Hash Tables.
It is worth trying on problems with a very large demodulator set, where a discrimination tree can develop nodes with very many children.

Next Section: Output Files