Strange behaviour in the UserPropagate `propagate` function #7465

JoanEspasa · 2024-11-26T20:27:12Z

JoanEspasa
Nov 26, 2024

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!

Answered by CEisenhofer

Feb 11, 2025

Should be fixed with #7551

View full answer

NikolajBjorner · 2024-11-26T20:52:16Z

NikolajBjorner
Nov 26, 2024
Maintainer

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.

3 replies

JoanEspasa Nov 26, 2024
Author

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 Nov 26, 2024
Maintainer

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 Nov 27, 2024

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 · 2025-02-10T16:48:49Z

JoanEspasa
Feb 10, 2025
Author

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

0 replies

NikolajBjorner · 2025-02-10T17:05:47Z

NikolajBjorner
Feb 10, 2025
Maintainer

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

4 replies

CEisenhofer Feb 10, 2025
Collaborator

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

CEisenhofer Feb 10, 2025
Collaborator

Regarding example: I will have a look at it

CEisenhofer Feb 11, 2025
Collaborator

Should be fixed with #7551

Answer selected by JoanEspasa

JoanEspasa Feb 11, 2025
Author

Thanks both for having a look and fixing it :)

Strange behaviour in the UserPropagate propagate function #7465

Uh oh!

JoanEspasa Nov 26, 2024

Replies: 3 comments · 7 replies

Uh oh!

NikolajBjorner Nov 26, 2024 Maintainer

Uh oh!

JoanEspasa Nov 26, 2024 Author

Uh oh!

NikolajBjorner Nov 26, 2024 Maintainer

Uh oh!

lukerooney7 Nov 27, 2024

Uh oh!

JoanEspasa Feb 10, 2025 Author

Uh oh!

NikolajBjorner Feb 10, 2025 Maintainer

Uh oh!

CEisenhofer Feb 10, 2025 Collaborator

Uh oh!

CEisenhofer Feb 10, 2025 Collaborator

Uh oh!

CEisenhofer Feb 11, 2025 Collaborator

Uh oh!

JoanEspasa Feb 11, 2025 Author

Strange behaviour in the UserPropagate `propagate` function #7465

JoanEspasa
Nov 26, 2024

Replies: 3 comments 7 replies

NikolajBjorner
Nov 26, 2024
Maintainer

JoanEspasa Nov 26, 2024
Author

NikolajBjorner Nov 26, 2024
Maintainer

JoanEspasa
Feb 10, 2025
Author

NikolajBjorner
Feb 10, 2025
Maintainer

CEisenhofer Feb 10, 2025
Collaborator

CEisenhofer Feb 10, 2025
Collaborator

CEisenhofer Feb 11, 2025
Collaborator

JoanEspasa Feb 11, 2025
Author