Removing the Tableaux-CDCL and CDCL solvers

[bclement-ocp]

Supporting all these solvers multiply the testing configurations and make it more difficult to perform changes to the SatML solver: the Tableaux-CDCL has a special entry point (the "hybrid" frontend) into the SatML solver, and the code is full of if-then-else conditions for the two components (in_theory and in_interpretation) of the CDCL-Tableaux hybrid. These conditions are true for the CDCL-Tableaux solver and false for the CDCL solver, but we also have special paths for cases where only one of them is set to true.

Ideally, I would like to remove the Tableaux-CDCL and the CDCL solvers entirely, as well as the --no-tableaux-cdcl-in-theories and --no-tableaux-cdcl-in-instantiation flags (which, confusingly enough, affect CDCL-Tableaux solver and not Tableaux-CDCL) and make Alt-Ergo error out if they are used. In order to do that, we should be sure that there is no reason to use any of these solvers instead of the Tableaux or CDCL-Tableaux solvers which would be kept as is (but the code of the CDCL-Tableaux solvers could be streamlined and simplified).

Following previous investigations by @Halbaroth into the different SAT solvers in Alt-Ergo, I have compared the variants (Tableaux-CDCL and CDCL-Tableaux) against the base solvers (Tableaux and CDCL) on our internal dataset.

(Note that there have also been discussions about removing the Tableaux solver entirely, but this is a different issue -- notably there seems to be differences in the way the Tableaux and CDCL-Tableaux solvers interact with instantiation that would be worth investigating and could lead to further improvements to the CDCL-Tableaux solver)

The result of the investigation is that:

• Tableaux-CDCL is strictly worse than Tableaux: it solves the same amount of problems (+2-2) but is slower (6h06 vs 5h40, about 8% slower).
• CDCL-Tableaux is better than CDCL, but not strictly so: it is significantly faster (3h04 vs 4h26, about 30% faster) and solves more problems, but there are still a few problems that are solved only by the CDCL solver (the comparison is +2048-132 in favor of the CDCL-Tableaux solver).

Given these results, I think that:

• It is fine to remove the Tableaux-CDCL solver entirely and immediately;
• Removing the CDCL solver would require doing some investigations first to understand more about the problems that we lose when going from CDCL → CDCL-Tableaux. We can recover some, but not all, by doing known tricks (e.g. always propagating equalities to the theories, even when they are not relevant).
• We might consider going from two flags (in_theories and in_instantiation) to a single flag for the CDCL-Tableaux solver, but I don't think going from two flags to a single flag significantly changes the extra burden when working on the solver.

@Gbury thoughts?

[bclement-ocp]

@Gbury ping — if you agree with the analysis above, removing the Tableaux-CDCL variant would make it easier to implement features needed for FPA support in the CDCL (and CDCL-Tableaux) solver.

[Gbury]

That makes sense to me. i'm in favor of removing Tableaux-CDCL, and investigating the cases where CDCL is better so that we can consider removing it in the future.

[Halbaroth]

Kill it with fire.

[Halbaroth]

@bclement-ocp did you address this issue in your PR for FPA support?

[bclement-ocp]

I have a half-finished PR for this lying around somewhere — I will try to dig it up.