Clearing only Heuristic values or only learned Conflict Clauses through the API.

[Horef]

Hello!
For context, me and my partner are doing a research project on the value of incremental solving, so that is where this question comes from.
I wanted to understand if it possible to clear only the heuristic values associated with the variables, or only the conflict clauses learned during the solution? (By using the api.)

As far as I understand, during the process of .solve() three things happen:

1. Variables are assigned values.
2. Heuristic values associated with each variable are updated.
3. Once a conflict occurs, conflict clauses are learned.

Now, if after the solver terminates we add new clauses and run .solve() again, in my understanding:

1. Assigned variable values are maintained, but checked against the new clauses (upd: I think they are destroyed).
2. Heuristic values are maintained. (What happens if new variables were added in the new clauses?)
3. Conflict clauses are maintained.

Now, in order to check the value of different aspects of incrementality, we want to be able to clear only the heuristic values, or only the conflict clauses before we call .solve() again. And in case assigned values are maintained, we want to be able to clear those out too.

Now, from looking at the cadical.hpp, I have come to the following ideas:
If I run disconnect_learner(), or connect_learner(dummy) and than disconnect_learner() on some dummy learner, will it clear out the learned clauses?
If I call reset_observed_vars(), will it reset both the assigned values, and the heuristic? (Or, in case assignments are cleared anyway, only the heuristic.)

Upd:
As far as I understand from this:

The important behaviour to remember is that adding, assuming or constraining a literal (immediately) destroys the satisfying assignment in the 'SATISFIED' state and vice versa resets all assumptions in the 'UNSATISFIED' state. This is exactly the behaviour required by the IPASIR interface.

Once I add a new clause (with new or old literals), the variable assignment is destroyed?

Thank you very much in advance.

[m-fleury]

It is more complicated that that.

Let's look at this

1. Variables are assigned values.
2. Heuristic values associated with each variable are updated.
3. Once a conflict occurs, conflict clauses are learned.

Please call 3, learned clauses, not conflict clauses.

You are missing the inprocessing part where the clauses are changed (think of the clause AvBvC and Av-C becoming the clauses AvBand Av-C but variable elimination is much more important). The impact of this is studied in https://abs.informatik.uni-freiburg.de/papers/2019/FBS_2019.pdf.

Now, if after the solver terminates we add new clauses and run .solve() again, in my understanding:

1. Assigned variable values are maintained, but checked against the new clauses (upd: I think they are destroyed).
2. Heuristic values are maintained. (What happens if new variables were added in the new clauses?)
3. Conflict clauses are maintained.

1. CaDiCaL has ILB (which is off by default IIRC) where the values are maintained and only the required ones are undone. Otherwise, the set values are reset. However, we maintain the cache of values to assign. This is not too important because we rephase after each solve.
2. The new variables are also added to the heuristics (there is a reverse option to decide if the value should be important or not). The relative ordering is maintained. On top of that there is another issue: the order is based on the order the clauses are given. So inprocessing clauses will change the order.
3. Correct.
4. The inprocessed clauses are maintained (although the inprocessing might be undone depending on the added clauses).

If I run disconnect_learner(), or connect_learner(dummy) and than disconnect_learner() on some dummy learner, will it clear out the learned clauses?

The learner is only a tracer: CaDiCaL will tell you what it learned. The learner offers not interaction.

If I call reset_observed_vars(), will it reset both the assigned values, and the heuristic? (Or, in case assignments are cleared anyway, only the heuristic.)

Observed variable is only related to the IPASIR-UP (see https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.SAT.2023.8/LIPIcs.SAT.2023.8.pdf).

Altogether, I am no sure what you are trying to do in light of inprocessing. Or do you plan to deactivate that?

[Horef]

Thank you very much for such an in-depth reply and explanations.
We have missed the importance of the inprocessing step and the complexity that it adds.

We want to be as true to the competitive sat as possible, so we wouldn't want to change any of the internal optimizations, let alone inprocessing.
Therefore, from your explanations I understand that it is indeed not very wise to pursue the goal of trying to remove either the learned clauses, or the heuristic values. We would limit ourselves to the comparison of cases of solving the problem incrementally vs from the ground up.

Thanks again for your time and explanations.

[m-fleury]

Actually, I think that it would be an interesting experience.

One way to do 2:

• keep track of the current set of clauses via the lrat tracer.
• instead of incrementally calling solve, create a new instance with the original clauses. This would test if the heuristic is reset.

One way to do 3:

• after each incremental call set lim.flush to 0 (there is API way to do, but this will flush all learned clauses soon). This requires some change to the code however.

Testing 1 can be done via the ILB option.