Keep and Delete Rules (Advanced)

This page describes a mechanism that allows the user to have more control over which clauses are kept or deleted than by using the parameters max_weight, max_vars, max_literals, and max_depth.

The mechanism uses the Clause Properties language for specifying clauses that are to be kept or deleted.

Two lists can be given in the input: a "keep" list and a "delete" list. Here are examples of each.

list(keep).
    -horn & literals=3 & variables=0 & level<4.
    horn & variables<3.
end_of_list.

list(delete).
    weight > 30.
    weight > 20 & (-horn | variables > 4).
end_of_list.

Given a newly derived clause, the following procedure is applied.

If the clause satisfies any rule in the "keep" list, then
    the clause is kept;
else if the clause satisfies any rule in the "delete" list, then
    the clause is deleted;
else
    the clause is kept;

Note that if the clause satisfies rules in both lists, it is kept.

The ordinary parameters max_weight, max_vars, max_literals, and max_depth are can be thought of as shorthand for simple rules in the "delete" list. For example the pair of commands

assign(max_literals, 3).
assign(max_vars, 0).

are operationally equivalent to the "delete" list

list(delete).
    literals > 3.
    variables > 4.
end_of_list.

In fact, the parameters max_weight, max_vars, max_literals, and max_depth are implemented in Prover9 by constructing an internal "delete" list, and any "delete" list given by the user is simply appended to the internal list.

The rules in the "delete" list are not applied to initial clauses; that is, clauses that are input or derived before the selection of the first given clause.