Prover9 Manual Version 2009-11A

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.

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(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(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, range [INT_MIN .. INT_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.

Next Section: Output Files