I have a better understanding of satML and a couple partially working prototypes for doing this, but did not run any large-scale benchmarks with them yet. There are still some things I am not entirely sure how to do properly with the combined CDCL+Tableaux solver, and I have realized that the optimization part is also affected by this, which I somehow overlooked initially. It should not be too big of a deal, but it is a bit annoying — and does make me want to pause this work until #921 is completed (even though I am not sure how much #921 touches this specific part of the optimization code).
(The following are mostly intended to be notes for myself when I get back to this)
I currently have two prototypes:
One that "just" allows satML atoms to be of type X.r Xliteral.view and is well integrated with the existing solver
One that separates case splits from satML atoms and is slightly less well integrated with the solver, but trying to replicate the current behavior of try_it / look_for_sat as much as possible
(I have not tried implementing something for the Tableaux solver but as I mentioned last week I don't anticipate too much difficulty there, as the Tableaux solver is simpler — but also it is less important because mostly unused)
The main issue with the first solution is that I don't really know how to do "garbage collection", which means that all the case splits that we have done in one branch of the sat will still be present in other branches. I think I can pop them when cancelling (e.g. splits made at level 7 will be collected when cancelling to a lower level), but they could still end up in learnt clauses, which is an issue, especially since I think that being able to incorporate splits into learnt clauses is an advantage of this first method over the second one. Might want to disable learning for clauses that involve case splits.
The main issue with the second solution is that the case splits really feel bolted on. In particular, there is no clause learning, and there are subtleties that I don't 100% understand yet — with this implementation, I still have infinite loops of making the same case split over and over again, which I think is due to throwing away the splits too early, but it seems to me like not doing that would require re-implementing a whole chunk of what is done for booleans and might not be worth it.
My current opinion is that the right way forward is: Xliteral in atoms (it is not as hard as I thought — modulo, again, CDCL+Tableaux and Tableaux+CDCL shenanigans that I don't have quite looked at in detail yet), but the same logic that I wanted to do for the separate case splits.
Some progress report:
I have a better understanding of satML and a couple partially working prototypes for doing this, but did not run any large-scale benchmarks with them yet. There are still some things I am not entirely sure how to do properly with the combined CDCL+Tableaux solver, and I have realized that the optimization part is also affected by this, which I somehow overlooked initially. It should not be too big of a deal, but it is a bit annoying — and does make me want to pause this work until #921 is completed (even though I am not sure how much #921 touches this specific part of the optimization code).
(The following are mostly intended to be notes for myself when I get back to this)
I currently have two prototypes:
X.r Xliteral.viewand is well integrated with the existing solvertry_it/look_for_satas much as possible(I have not tried implementing something for the Tableaux solver but as I mentioned last week I don't anticipate too much difficulty there, as the Tableaux solver is simpler — but also it is less important because mostly unused)
The main issue with the first solution is that I don't really know how to do "garbage collection", which means that all the case splits that we have done in one branch of the sat will still be present in other branches. I think I can pop them when cancelling (e.g. splits made at level 7 will be collected when cancelling to a lower level), but they could still end up in learnt clauses, which is an issue, especially since I think that being able to incorporate splits into learnt clauses is an advantage of this first method over the second one. Might want to disable learning for clauses that involve case splits.
The main issue with the second solution is that the case splits really feel bolted on. In particular, there is no clause learning, and there are subtleties that I don't 100% understand yet — with this implementation, I still have infinite loops of making the same case split over and over again, which I think is due to throwing away the splits too early, but it seems to me like not doing that would require re-implementing a whole chunk of what is done for booleans and might not be worth it.
My current opinion is that the right way forward is:
Xliteralin atoms (it is not as hard as I thought — modulo, again, CDCL+Tableaux and Tableaux+CDCL shenanigans that I don't have quite looked at in detail yet), but the same logic that I wanted to do for the separate case splits.