How to prevent user_propagator propagated clauses from being ignored

[wbthomason]

I'm currently trying to implement a version of SATPlan with the user propagator. In enforcing the frame axioms (basically, a state variable may only change values between steps if an action that changes the state variable is used at the same step), I propagate clauses corresponding to the related actions being chosen. However, these clauses seem to be ignored/not satisfied. I'm wondering if there's a way around this (or something that I'm doing incorrectly).

To elaborate: Assume that I have some set of state variables s1, ..., sk, some set of action variables a1, ..., am, and n steps (where a step is a complete setting of state variables combined with a single action). Actions have effects, which are lists of state variables that they set to true or false at the step at which the action is chosen.

I model this by creating Boolean constants s1@1, s1@2, ..., s1@n, s2@1, ... and correspondingly a1@1, a1@2, .... In my user propagator implementation, if a state variable si@j is fixed, I propagate e.g. si@j => si@j-1 || a1@j || a3@j (for the case that si@j was fixed to true, and a1 and a3 are the actions that make si true) by calling:

propagate(1u, &si_at_j_id, z3::mk_or(si_at_prev_step, a1_at_j, a3_at_j))

However, I'll often see that, shortly after this propagation, all of si@j-1, a1@j, a3@j are set to false - contradicting the clause I propagated. Is this expected, or something obviously wrong that I'm doing? If not, is there a way to work around this and ensure that a propagated clause "counts"? (I did see in https://github.com/Z3Prover/z3/blob/master/examples/userPropagator/example.pdf that propagated clauses are treated as hints more than assertions)

Thank you!

[NikolajBjorner]

There could be two ways:

You can change the propagator to deal directly with 3 cases:

si_at_j_id and ~si_at_prev_step and ~a1_at_j => a3_at_j
si_at_j_id and ~si_at_prev_step and ~a3_at_j => a1_at_j
si_at_j_id and ~a3_at_j and ~a1_at_j => si_at_prev_step

You may need to re-propagate the clause multiple times in separate branches. It should not be the case that the clause is false in the same backtracking context. That is, you should observe a pop before you get anything that contracts the clause. If you do, I am not sure what is going on without digging into details.

It might be possible to re-assert the propagated clause during a callback to pop as well. This interaction is not yet tested.

[wbthomason]

Thanks! It is possible, though, that si@j will be fixed before any of si@j-1, a1@j, or a3@j, which would make the conditions of those implications indeterminate - which was the motivation for the original propagated clause. I'm not sure if e.g. propagating the OR in the indeterminate case and the single-expression clauses in fully determined cases would do anything, but I can certainly try.

It might be possible to re-assert the propagated clause during a callback to as well.

Sorry - a callback to final? Or fixed?

Thank you for your help!

[NikolajBjorner]

Alright, since si@j could be fixed last, then with the do-it-yourself propagator, you have either the option of adding propagations for the 4th case and thereby effectively implementing your own watch index or just detect conflicts (without propagation) and rely on lemma learning to eventually propagate.

[NikolajBjorner]

I have fixed reply above to mention "pop" (the pop event handler).

[wbthomason]

Thanks for your help - splitting the original propagated clause up (with the aforementioned 4th case), as you suggested, seems to have done the trick. Thanks again!