Strange behaviour in the UserPropagate propagate function

[JoanEspasa]

Hi,

I am implementing a user propagator for a planning as SMT approach in Python.

Given an assignment on whether some actions are selected in a given timestep, I am able to infer whether other actions have to be assigned either True or False. I am attempting to propagate this information, to prevent them to semantically interfere with each other on the same step for the final plan. More concretely, I aim to implement a "lemmas on demand" approach for mutexes between actions that can happen in parallel.

For example, given 2 actions A and B, when the solver fixes A to True I can now tell that B must be false. My assumption is that in order to propagate this fact, I can call propagate() with the expression e = z3.Not(B), and the justification ids=[A] (a parameter to the propagate call. This is my understanding according to ( https://link.springer.com/chapter/10.1007/978-3-031-24950-1_5 ), which states "A propagation claim is (E ∧ F) ⇒ G where E is a subset of the reported equalities of Eq, F a subset of Fixed, and G an arbitrary formula constructed by Z3’s API", meaning I understand calling propagate(e=z3.Not(B), ids=[A]) should add the clause A->Not(B), or (Not(A) \/ Not(B)) to the solver.

However I have found when validating solutions, the number of steps increases significantly from an eager approach. This is incorrect as just giving a part of the formula on demand to the solver should not change the number of steps. The problem becomes overconstrained, so maybe the lemmas propagated are not forgot when a pop callback happens?
This makes me think that I am not understanding how the solver uses the parameters for ids.

Surprisingly, I have found that passing the same action for justification in twice (e.g. ids=[A, A]) actually causes the problem to be solved in the correct number of steps, and also makes a notable difference to the number of propagations/user propagations made by the solver. This implies my initial understanding is incorrect, as I thought that A \/ A -> Not(B) = Not(A) \/ Not(A) \/ Not(B) = Not(A) \/ Not(B), which I did not think would make a difference.

I just wanted to double check how to correctly use the propagate function and ask about the difference I am seeing.

Thanks in advance!

[NikolajBjorner]

• ids=[A] should be semantically the same as ids=[A,A] so I am not able to explain what you claim to observe.
• when propagating A => not B, it introduces a lemma at the current search level. The lemma can be garbage collected at pop. You have to re-introduce the lemma after a pop if you want it to be more sticky. It could always get garbage collected.
  Use smt.up.persist_clauses=true to force the clause associated with a propagation to be persisted across backtracking points.

[JoanEspasa]

• I will try to create a minimal example then to replicate the behaviour with ids.

• Regarding the length of the problem, I'm seeing the oposite behaviour: The problem is overconstrained and seems the clauses stick around too much if that makes sense. This makes me think that I'm incorrectly building the propagation.
  Just to confirm: to propagate Not(B) contingent to A=true, I should do propagate(e=z3.Not(B), ids=[A]) right?
  Once the solver pops the context, that clause will be forgotten. When internalising the clause, I assume the solver will build something semantically equivalent to introducing the lemma A -> Not(B) but I do not have to manually create the implication.

[NikolajBjorner]

• thanks
• yes, correct. You can also propagate(e= z3.Or(z3.Not(A), z3.Not(B)), []). Less efficient but same meaning.
• you can set smt.uppersist_clauses=true so the clause is not forgotten after pop.

[lukerooney7]

A minimal example showcasing differing behaviour:

Using the userpropagator in this Python example:

z3/examples/python/bincover.py

Line 252 in 94f0aff

self.propagate(bin.var, justification)

We can use the example 1 instance:
s = OptimizeBinCoverSolver() i1 = s.add_item(2) i2 = s.add_item(4) i3 = s.add_item(5) i4 = s.add_item(2) b1 = s.add_bin(3) b2 = s.add_bin(6) b3 = s.add_bin(1) s.optimize()

For the propagation function, we can compare the effect of:

• Approach 1:self.propagate(Not(bin.var), justification)
• Approach 2:self.propagate(Not(bin.var), justification + justification).

This gives a differing solution and statistics for number of propagations and user-propagations:

• Approach 1 Solution:

• Approach 1 Solver Stats:

• Approach 2 Solution:

• Approach 2 Solver Stats:

[JoanEspasa]

@NikolajBjorner I'm wondering if you had some time to look at this, or if we should move it to an issue?

[NikolajBjorner]

add @CEisenhofer
my recollection from trying this it didn't expose a correctness bug. It had to do with reproducibility under external changes.

[CEisenhofer]

I think smt.up.persist_clauses=true currently by default. (Not sure though if this should not be better false by default)

[CEisenhofer]

Regarding example: I will have a look at it

[CEisenhofer]

Should be fixed with #7551

[JoanEspasa]

Thanks both for having a look and fixing it :)