Hints
Hint clauses can be used to help guide Prover9's search. Prover9's input can contain any number of hint lists (which are simply concatenated by Prover9).Each list of hint clauses must start with formulas(hints). and end with end_of_list. Any clause is acceptable as a hint. For example (the label attributes are optional),
formulas(hints).
x ' * (x * y) = y # label(6).
x * (x * y) = y # label(7).
x * (y * (x * y)) = e # label(8).
x ' ' * e = x # label(9).
x ' * e = x # label(10).
x ' = x # label(11).
x * e = x # label(12).
x * (y * x) = y # label(13).
x * y = y * x # label(14).
end_of_list.
A derived clause matches a hint if it subsumes the hint. If a clause matches more than one hint, the first matching hint is used.
In Otter, "matching a hint" can mean (depending on the parameter settings) subsumes, subsumed by, or equivalent to. These other types of matching may be added to Prover9 if there is any demand for them.
Hints are used primarily when selecting given clauses. The mechanism for doing this is the given-clause selection procedure. In short, the default value of the hints_part parameter says to select clauses that match hints (lightest first) whenever any are available.
Hints are also used when deciding to keep a new clause. Clauses that match hints are not deleted by any of the parameters max_weight, max_vars, max_literals, or max_depth.
Where do Hints Come From?
Hints frequently consist of proofs, perhaps many, of related theorems.Bob Veroff developed the concept, installing code for hints in an early version of Otter, to experiment with his method of proof sketches [Veroff-hints, Veroff-sketches]. In the proof sketches method, a difficult conjecture is attacked by first proving several (or many) weakened variants of the conjecture, and using those proofs as hints to guide searches for a proof of the original conjecture.
The program Prooftrans, which is distributed along with Prover9, can be used to extract proofs from a Prover9 output file and transform the proofs to lists of hints suitable for input to subsequent Prover9 jobs.
An Example
This example consists of four jobs. The first is a proof of a nontrivial theorem called "hard". The other three jobs prove the hard theorem indirectly by first proving an easier theorem (in this case, the easier theorem simply the harder theorem with an extra assumption); then using the proof of the easier theorem as hints to help prove the hard theorem.- A Prover9 job that proves the hard theorem.
prover9 -f hard.in > hard.out
- A proof of the easier thorem.
prover9 -f easy.in > easy.out
- A Prooftrans job converts the proof of the easier theorem into a list of hints.
prooftrans hints -f easy.out > easy.hints
- A Prover9 job that uses the hints to prove the harder theorem.
prover9 -f hard.in easy.hints > hard-hints.out
Special Weight Assignments
When the given clause selection procedure calls for a clause that matches a hint, the lightest such clause is chosen. Ordinarily, clauses that match hints are weighed just as any other clause is weighed. However, if one believes some hints are more important that others, one can, in effect, say "any clause that matches this hint gets a specific weight". This is accomplished by attaching a bsub_hint_wt attribute to the hint, as in the following example.
formulas(hints).
x ' * (x * y) = y # label("very important hint") # bsub_hint_wt(-100).
end_of_list.
Another way to assign a special weight is with the following flag.
set(breadth_first_hints). clear(breadth_first_hints). % default clear
Setting this flag causes all clauses that match hints to receive weight 0. The effect is as if each hint had the attribute bsub_hint_wt(0). This causes clauses that match hints to be selected in the order they are generated.
The weight assigned by any of the preceding methods may be modified if the flag degrade_hints is set.
Hint Degradation
In many searches that use hints, a given hint can match many different derived clauses. As a hint matches more and more clauses, we wish its influence to diminish. This is the idea behind Veroff's hint degradation method.set(degrade_hints). % default set clear(degrade_hints).
If this flag is set, a weight penalty is added to clauses that match hints that have been previously matched. The following procedure is used. Given a newly derived clause, say C, assume we find a hint that matches the clause; let n be the number of times the hint has already been matched; then the weight of C is increased by (n * 1000). In other words, 1000 is added for each previous match of the hint.The effect of this procedure is (usually) that clauses matching hints are selected in the following order: clauses matching hints that have not been matched before, clauses matching hints that have been matched once before, and so on.
Keeping/Limiting Clauses the Match Hints
Ordinarily, when a clause matching a hint is derived, the clause will be retained even if it violates limits such as max_weight. Setting the following flag will cause those limits to be applied to such clauses, and it may be useful with trying to simplify known proofs.set(limit_hint_matchers). clear(limit_hint_matchers). % default clear
If this flag is set, the parameters max_weight, max_literals, max_depth, and max_vars will be applied to clauses that match hints (as well as to clauses that don't match hints).Otherwise (the default), those limits will not be applied to clauses that match hints.
Back Demodulation of Hints
When hints come from proofs in which equality and rewriting play a major role, they may have trouble guiding a search, because the rewriting may occur in different ways in the new search. In particular, a hint may fail to match a clause, because the clause has been rewritten and the hint has not. This is the motivation for the following feature.set(back_demod_hints). % default set clear(back_demod_hints).
If this flag is set, hints are back demodulated. That is, they are kept simplified with respect to the current set of demodulators.
Labels on Hints
Label attributes on hint clauses get special treatment. When a hint containing a label matches a clause, the label attribute is copied to the clause.The following flag addresses the situation in which the input contains sets of equivalent hints. (This situation frequently occurs when the hints contain many proofs of similar theorems.)
set(collect_hint_labels). clear(collect_hint_labels). % default clear
If this flag is set, and the hints list contains a set of equivalent hints, only the first copy of the hint is retained. However, the labels from all of the other equivalent hints are collected and put on the retained copy. When a clause matches the retained hint, it gets copies of all of the labels from the equivalent hints.If this flag is clear, when a clause matches a set of equivalent hints, it receives the label (if any) from the first copy only.
Reporting Hints from a Proof
The following two flags report, after a proof is found, which hints took part in it. Both write their output as formulas(...) lists, so the results can be pasted directly into an input file as a hints list for a later search.set(print_matched_hints). clear(print_matched_hints). % default clear
If this flag is set, three lists are printed after each proof.Together these say how much of the proof the hints actually accounted for, which is the usual way of judging whether a hints list is earning its keep.
- MATCHED HINTS — the hints that were matched by clauses in the proof.
- HINT MATCHERS — the proof clauses that matched a hint.
- NON HINT MATCHERS — the proof clauses that did not.
set(print_new_hints). clear(print_new_hints). % default clear
If this flag is set, a NEW HINTS list is printed after each proof, containing the clauses of the proof that did not match any hint and that were not input clauses, goals or denials — that is, the genuinely new steps.Adding these to the hints list is the usual way of accumulating hints across a series of related searches.
Giving Up When the Hints Run Out
assign(max_nohints, n). % default n=-1, range [-1 .. INT_MAX]
If n is greater than 0, and n given clauses in a row are neither input clauses nor hint matchers, the search stops. Prover9 reports% 200 givens in a row w/o an input clause or a hint matcher (max_nohints).and exits with the message max_nohints.The counter is reset whenever a given clause is an input clause or matches a hint, so this measures how far the search has drifted from the hints, not how many non-matching clauses it has seen in total.
If n is -1 (the default), the search is never stopped for this reason. This is useful when a hints list is expected to guide the whole search: rather than letting a search that has lost the thread run to its time limit, abandon it early and try different settings.
Hint Expiry and Statistics
When a large hints list is used, many of the hints may stop being useful part way through a search, yet they continue to cost time in the hint-matching index. The following options let Prover9 drop hints that have gone stale, and report on how the hints are being used.Hint Expiry
assign(hint_expiry, n). % default n=-1, range [-1 .. INT_MAX]
If n is greater than 0, hints that have been matched, but not within the preceding n given clauses, are removed from the hint index. Hints that have never been matched are always kept.If n is -1 (the default), no hints are ever expired.
When hints are expired, a message such as % Expired 12 hints at given #4000 (388 active). is sent to the standard error file.
assign(hint_expiry_min, n). % default n=1, range [1 .. INT_MAX]
The number of times a hint must have been matched before it becomes eligible for expiry. Raising this value protects hints that have been matched only a few times.
assign(hint_sweep_interval, n). % default n=1000, range [1 .. INT_MAX]
How often the expiry sweep runs, in given clauses. The sweep is performed when the number of given clauses is a multiple of n. This parameter has no effect unless hint_expiry is greater than 0.
Hint Matching
set(hint_match_once). clear(hint_match_once). % default clear
If this flag is set, a hint is removed from the hint index as soon as it matches a kept clause, so that it cannot match again. The hint remains in the hints list for the purpose of statistics.This can save a substantial amount of time when many clauses match the same hint, but note that later clauses matching that hint will not receive its special treatment.
assign(hints_fpa_depth, n). % default n=10, range [1 .. 100]
The indexing depth used for the FPA index that finds candidate hint matches. Deeper indexing gives more precise retrieval at the cost of a larger index.This sets the depth of the hint index only. See Indexing for the parameters that control when index nodes switch to hash tables.
Hint Statistics and Diagnostics
set(hint_match_stats). clear(hint_match_stats). % default clear
Whenever the input contains hints, Prover9 reports at the end of the search how many of them were matched, how many were redundant, and how many are still active, along with the distribution of match counts. This summary is printed whether or not this flag is set. For example,Hint match stats: total=15, redundant=11, active=4, matched=2 match counts: min=1, mean=1.0, median=1, max=1If no hint was matched, a shorter form is printed instead:Hint match stats: no hints were matched. total=15, redundant=6, active=9This is useful for deciding whether a hints list is actually helping, and for tuning hint_expiry.Setting this flag adds a re-match histogram to that report. For hints that were matched more than once, Prover9 records the distance, in given clauses, between successive matches, and reports the count, minimum, mean and maximum along with a bucketed histogram. The histogram is omitted if no hint was matched more than once.
The re-match distances say how long a hint stays useful, which is what hint_expiry needs to be set against: an expiry distance shorter than the typical re-match distance will drop hints that were still going to be used.
assign(hint_derivations, n). % default n=0, range [0 .. INT_MAX]
If n is greater than 0, then whenever a kept clause matches one of the first n hints, Prover9 prints the derivation of that clause, in the same format as a proof, labeled Hint derivation (Proof).This is a diagnostic aid: it shows how the search arrived at the clauses that the hints were meant to steer it toward. It does not change the search.
Resonators
Resonators are Larry Wos's resonance strategy: a list of term patterns that identify clauses considered especially valuable, each with a flat weight to assign to the clauses that match it. Like hints, resonators guide the search without changing what is logically derivable.list(resonators). weight(f(x,y), 1). weight(g(x), 2). end_of_list.Each member of the list must have the form weight(pattern, n).
Resonator matching uses Wos semantics, which differ from the matching used for ordinary weighting rules: every variable position in the pattern — whether a named variable or an anonymous _ variable — is an independent wildcard that matches any subterm, including a complex term, with no requirement that repeated variables match the same thing. Constant and function positions must match structurally. This generalizes Otter's wt_match semantics, which matched only variables, to the full-term setting needed for resonators in algebraic problems.
Resonators are consulted before ordinary weighting rules, and the first one that matches wins: a clause matching any resonator receives that resonator's weight instead of its ordinary symbol-count weight. The substituted weight is used both for given-clause selection (lower weight means higher priority) and for max_weight retention.
If any resonators are installed, Prover9 says so near the start of the output, for example
% 3 resonators installed (Wos wildcard matching).