feat(CDCL-Tableaux): Do not make irrelevant decisions

[bclement-ocp]

The CDCL-Tableaux solver uses the structure of the original formula both to limit the literals that are propagated to the theory module and to focus the (sub)-terms of the formula to use for instantiation.

Effectively, it only uses literals that are either asserted directly (possibly as part of a conjunction), or that are the first literal that was decided in a disjunction. For instance, if the formula [P / Q] is asserted, and we decide that [P] holds, [P] will be propagated to the theory module and used for instantiation -- but if we ever decide or prove that [Q] holds (or does not hold), that information will be ignored by the theory and instantiation modules.

In these conditions, deciding on [Q] is unlikely to help us make any progress, and so this patch prevents the CDCL-Tableaux solver from taking decisions on such irrelevant variables.

Benchmarks: This PR is +121-44 (net: +77) and a slight performance boost (around 1.5%) on AE-Format.

[bclement-ocp]

Updated for compatibility with #1027

[Halbaroth]

Suggested change

	because otherwise instanciation requires a complete boolean model. *)
	because otherwise instantiation requires a complete boolean model. *)

[Halbaroth]

Nit: I think by unknown you mean unassigned.

[Halbaroth]

Why do we need a complete boolean model in this case?

[bclement-ocp]

Turns out this is a more complex question than I expected :) I used this condition because (a) that it is the condition used for early stopping when the lazy_cnf is empty (so it made sense to keep this condition) and (b) not having this condition was crashing here in a state that was clearly caused by the frontend expecting some atoms to be decided when they were not, hence my description of "we need a complete boolean model".

Turns out the truth is a bit more complicated, and I will try to explain what happens here.

Here are some facts:

• The get_cdcl_tableaux_inst () is enabled by default in the CDCL-Tableaux solver
• This flag instructs the instantiation mechanism to use only "relevant" (for some definition of "relevant") atoms when looking for terms during instantiation
• The definition of "relevant" that is used above can be found here and ultimately asks SatML for its instantiation_context. If get_cdcl_tableaux_th () is enabled then we ask the theory; if it is not enabled then we look into the env.relevants field, which corresponds to the definition used in this PR.
• If the get_cdcl_tableaux_inst () flag is disabled, the conj field from the SatML frontend is used instead (see atoms_from_sat_branches) to find the atoms to use for future instantiation rounds.
• The relevants field (and the lazy_cnf field) in SatML are updated when backtracking
• The conj field, being maintained by the frontend and not by SatML itself, is not updated when backtracking

Given those facts, we can see that if get_cdcl_tableaux_inst () is false, the SatML frontend expects that all assertions from previous instantiations, even previous instantiations that are no longer relevant, are enforced by the solver (otherwise we fail here). Using get_cdcl_tableaux_inst () as a condition here is also coherent with the fact that it is the condition used for early stopping when the lazy_cnf is empty.

For a concrete example: if we assert (P 3 ∧ Q 3) ∨ R 3 and we have ∀y, P y → y < 0 and ∀y, Q y → y > 0. The following happens independent of the value of get_cdcl_tableaux_inst ():

• The SAT explores the P 3 ∧ Q 3 branch first, and asserts P 3 and Q 3, which are relevant.
• The quantifiers are triggered, and we instantiate P 3 → 3 < 0 and Q 3 → 3 > 0.
• 3 < 0 is a contradiction, so we backtrack and learn ¬(P 3).
• We go into the R 3 branch. Neither P 3 nor Q 3 are relevant anymore.

Now we go to instantiation again, and here the behavior differs.

• If get_cdcl_tableaux_inst () is true, we look only into relevant atoms for instantiation. This means we only look into R 3, which has no triggers, and we are done¹.
• If get_cdcl_tableaux_inst () is false, on the other hand, we look into the conj field of the SatML frontend. Since it is not backtracked, we find all the previous instantiations there, in particular P 3 → 3 < 0 and Q 3 → 3 > 0. But if we only decide relevant atoms, we don't have a truth value for Q 3 (since it is not relevant)!

Footnotes

1. Technically I think we move to greedy quantifier instantiation, but nothing happens there either. ↩

[bclement-ocp]

Note: I think that "instantiation requires a complete boolean model" is a reasonable summary of this explanation for a code comment, given the amount of far-in-the-code implementation details it depends on.

This also asks the question of whether we want to keep the different SatML switches (looking at --no-cdcl-tableaux-in-theories, --no-cdcl-tableaux-in-instantiation in particular here, but also also thinking about --no-minimal-bj); they have been enabled by default for years, have non-trivial costs in terms of code complexity (as evidenced by the above comment), and I don't think anyone actually uses them (Why3 certainly does not, and we ourselves only enable them in the CI tests).

[Halbaroth]

Sure, we should test them and if there aren't useful, we may deprecated them in the next release.

[Halbaroth]

Can I merge?

[bclement-ocp]

Missed the review notification — done