User propagators vs. offline lemmas on demand, and clause deletion policies

[ThomasHaas]

I recently tried to replace an offline SMT approach (lemmas on demand) by a user propagator and found surprising regression.
In the former approach, we query a full model from the SMT solver, check for theory consistency, and then add new constraints (subsets of the model that are inconsistent) in an incremental fashion.
The user propagator based approach is pretty much the same, but we do the consistency check in the final check callback and raise conflicts on the inconsistent subsets.

On my (unsatisfiable) example benchmark, the former approach does around 350 consistency checks whereas the user propagator needed 5600. Even worse, the solving time goes from 8 seconds to over 9 minutes. From those 9 minutes, less than a minute is spent inside the user propagator itself, so it is not that the propagator itself is inefficient.

I was surprised to see such a high number of consistency checks. I guess this is because the conflict clauses are eligible for deletion. Is there a way to add non-deletable clauses from within the propagator? It seems adding standard clauses to the solver is forbidden.
Also, we raise a lot of conflicts in a single final callback. Does the solver generate conflict clauses for all of them or does he keep only those that, e.g., cause the most backtracking? We frequently observe that the final check is done at decision level 2000+ and afterwards the solver backtracks all the way down to somewhere around level 10.

[NikolajBjorner]

The build-in solvers leverage propagation to cut branches before final check.
It sounds like you are not emulating this behavior in the way you use the propagator.
It is up to you to figure out what can be propagated efficiently.

Only one conflict survives, the first. Maybe a way of filtering conflicts based on conflict level can be adapted, or tagging along more lemmas.

Remove note on using add_th_axiom. They are treated differently from lemmas, but do get removed when the scope is popped:

Persisting theory axioms is one possible change. You can try to change

z3/src/smt/theory_user_propagator.cpp

Line 354 in 736d634

ctx.mk_th_lemma(get_id(), m_lits);

to use add_th_axiom instead.
Surfacing this option can be achieved by either supplying a configuration option (that optionally could be toggled during search if needed)

[ThomasHaas]

The build-in solvers leverage propagation to cut branches before final check. It sounds like you are not emulating this behavior in the way you use the propagator. It is up to you to figure out what can be propagated efficiently.

The final goal is to do early propagation but since we already had the (non-incremental) offline approach implemented, it was easiest to first move the offline approach into the final callback to simulate the original behaviour and judge the overhead of tracking the solver.

Only one conflict survives, the first. Maybe a way of filtering conflicts based on conflict level can be adapted, or tagging along more lemmas.

Ok, this explains a lot. We frequently find 50+ disjoint conflicts in a single check that we all learn in the offline approach (since the checks are "infrequent" we try to learn as much as possible per check).
I just changed my offline solver to learn only a single conflict and adapted the user propagator to pick the smallest conflict in each check (often just 1-2 literals): The number of checks is now a lot closer (around 3100 for both).
Although the iteration numbers were similar, the propagator was still slower by factor 4-5 (it sometimes gets stuck backtracking without finding a model? EDIT: This might be an issue external of Z3, because I use a custom Java API around Z3).

Then I tried the following: I find the conflict in the final callback, but don't raise it immediately and instead return from the user propagator and then add the clause from the outside (like a hybrid approach). Interestingly, this only generated around 1900 checks although it learns exactly what the user propagator would. So I guess there is some form of clause deletion going on?

In a recent discussion #7087 you mentioned that one could learn any theory lemma, for example, symmetric conflict clauses.
So can I raise only a single conflict but learn arbitrarily many non-conflicting clauses?

Persisting theory axioms is one possible change. You can try to change

z3/src/smt/theory_user_propagator.cpp

Line 354 in 736d634

ctx.mk_th_lemma(get_id(), m_lits);

to use add_th_axiom instead. Surfacing this option can be achieved by either supplying a configuration option (that optionally could be toggled during search if needed).

Is this change only about the clause deletion policy or does this also allow one to learn multiple conflicts?

EDIT 2: The remaining slowdown was indeed due to the Java API using additional reference tracking (phantom references) to free Z3 resources. If I disable this tracking, the offline solver and the user propagator show basically the same performance although the user propagator does more checks. However, this is only when restricting the offline solver to learn a single conflict.
So if the user propagator was able to learn multiple conflicts, I think it would match or even slightly outperform the offline solver.

[NikolajBjorner]

The remaining slowdown was indeed due to the Java API using additional reference tracking (phantom references) to free Z3 resources.

We have a new way to avoid this. It is implemented for .Net and OCaml. It gets rid of the reference tracking at the Java level.
It requires some coding and testing which I haven't done on the Java side at this point. If you have extra bandwidth to make this change you will likely have a better Java experience.

Is this change only about the clause deletion policy or does this also allow one to learn multiple conflicts?

Only about clause deletion policy.

[ThomasHaas]

Thanks for the great answers.

We have a new way to avoid this. It is implemented for .Net and OCaml. It gets rid of the reference tracking at the Java level.
It requires some coding and testing which I haven't done on the Java side at this point. If you have extra bandwidth to make this change you will likely have a better Java experience.

I use a custom Java API rather than the Z3 one, so I would need to implement the solution there to test it (though if it works reasonably, I can try to port it to Z3's Java API). I remember seeing that the C# API requires explicit copying of the expressions returned in callbacks, if those should be kept beyond the callback's lifetime. I guess this is related to the "new way".

In the case of user propagators specifically, I think one would also get away with just not adding phantom references for the expressions returned to the callbacks, no? The reason is that those should match with a registered expression and the user propagator could just increment the reference count once on registration (and decrement on deleting the whole propagator).
I think as long as no expression outlives the user propagator itself, it should work.

Is this change only about the clause deletion policy or does this also allow one to learn multiple conflicts?

Only about clause deletion policy.

Would it be hard (implementation-wise) to make multiple conflict propagations possible? I feel like this is a useful feature when doing lemmas on demand or, more generally, when doing consistency checks in batches (i.e., only every N fixed callbacks) because then multiple conflicts can occur naturally.
I can even imagine scenarios where a single fixed value causes multiple conflicts: if you reason on graph acyclicity and a single added edge closes multiple disjoint cycles (disjoint up to the one common edge), then each of them results in a conflict.
In fact, our use-case is graph-based reasoning and our checking algorithm reports conflicts on cycles: in the offline approach we find a set of shortest cycles and generate a blocking clause for each of them.

[NikolajBjorner]

• You can save aside your multiple conflicts for the next propagation callback after a final check. At this point you can add them. You can accumulate such clauses down the undos.
• I asked GPT for help with porting. It came up with some non-well-formed code (in the first shot and I don't have a shiny agent yet to do the grunt work of building/debug/eval and fix within vscode yet). But it suggested to use the "finalize" method (well done!) in Z3Object.java and call an overloaded method decRef() in the subclasses. The decRef then calls Native.yZYdecRef. The methods for IDecRefQueue all go away. Instructions are as follows:

Your task is to port how reference counting is implemented in C# to Java.
The Csharp code is in the files ending with the extension .cs.
The Java code is in the files ending with the extension .java.
The Csharp code uses Native.Z3_enable_concurrent_dec_ref(m_ctx); when it creates a context in the file Context.cs.
The java code uses IDecRefQueue.java to implement reference tracking using phantom references. When a java object
becomes unreachable the phantom reference is enqueued to a queue. 
The Csharp code uses Z3Object as a base clase. The Dispose method calls DecRef which is overridden by derived classes.
The DecRef methods that are overriden call Native.Z3_dec_ref(m_ctx.nCtx(), obj) to decrement the reference count.
Instead of enqueuing Phantom references into a queue, the new Java code should use the pattern of the C# code.

[ThomasHaas]

You can save aside your multiple conflicts for the next propagation callback after a final check. At this point you can add them. You can accumulate such clauses down the undos.

FYI, the C++ user propagator example for Nqueens reports all placement conflicts in a single callback:

z3/examples/userPropagator/user_propagator_with_theory.h

Lines 26 to 45 in c40e72a

	for (const z3::expr &fixed: fixedValues) {
	unsigned otherId = queenToY[fixed];
	unsigned otherPos = currentModel[queenToY[fixed]];
	if (queenPos == otherPos) {
	z3::expr_vector conflicting(ast.ctx());
	conflicting.push_back(ast);
	conflicting.push_back(fixed);
	this->conflict(conflicting);
	continue;
	}
	int diffY = abs((int) queenId - (int) otherId);
	int diffX = abs((int) queenPos - (int) otherPos);
	if (diffX == diffY) {
	z3::expr_vector conflicting(ast.ctx());
	conflicting.push_back(ast);
	conflicting.push_back(fixed);
	this->conflict(conflicting);
	}
	}

Maybe the example should break after the first conflict and explain (with a comment) that multiple conflict propagation are pointless. This might help some users in the future.

[ThomasHaas]

• You can save aside your multiple conflicts for the next propagation callback after a final check. At this point you can add them. You can accumulate such clauses down the undos.

I thought about this workaround, but it does feel kinda sketchy. I will try it out and see how it goes though.

• I asked GPT for help with porting. It came up with some non-well-formed code (in the first shot and I don't have a shiny agent yet to do the grunt work of building/debug/eval and fix within vscode yet). But it suggested to use the "finalize" method (well done!) in Z3Object.java and call an overloaded method decRef() in the subclasses. The decRef then calls Native.yZYdecRef.

The solution confuses me. Doesn't this just put the burden of reference management on the user? I think people are in general not willing to do fine-granular disposal of each formula in a managed language (for large objects like solvers and contexts, this is fine).
In C# one can combine Dispose and a finalizer to get the best of both worlds, i.e., manual/early reclamation if Dispose is called and automatic/late reclamation if not. IIRC, this is not possible in Java though due to the lack of finalizers (that's why phantom references are used).

[NikolajBjorner]

Oh, I see

(Edit 2022-04-04: [JEP 421](https://openjdk.java.net/jeps/421) Deprecate Finalization for Removal has been integrated and delivered in JDK 18.)

[ThomasHaas]

You can save aside your multiple conflicts for the next propagation callback after a final check. At this point you can add them. You can accumulate such clauses down the undos.

I now tried this approach as follows: I have a Queue<Conflict> openConflicts and in each fixed-callback I deque a single unpropagated conflict and do propagateConsequence(empty, not(conflict.assignment())) (i.e., I generate "true => not (conflict)").
The number of checks went from 3100 down to around 1500, but the solving time did not improve that much (from 50 seconds down to 40 seconds). The offline approach does only 360 checks and needs around 8-9 seconds!
Assuming that all propagations go through now, I guess the remaining discrepancy must be due to clause deletion so I will try changing Z3's code as you suggested (EDIT: I just saw the update to your post).

PhantomReferences:
On the flip-side, I found a superior way of using PhantomReferences that makes them vastly more performant and even reduces memory footprint.
The current implementation relies on a map Map<PhantomReference<T>, Long> referenceMap that will degrade in performance when a large number of objects get registered (on my benchmark, 80% of time was spent accessing this map!).
This map can be replaced by a doubly-linked list of (subclasses of) phantom references which maintains O(1) insertion and deletion times (lookup time is irrelevant!). On the same benchmark, now only 10% of time spent was related to phantom references, reducing the solving time from 5 minutes down to 70 seconds.
You can see this implementation here: JavaSMT PR (JavaSMT copied their phantom reference handling from Z3's way of doing it)
I can port it over to Z3.

[NikolajBjorner]

Adding an option to allow you to persist clauses
3b90816

set smt.up.persist_clauses=true

[ThomasHaas]

Cool, thanks for the update.
I've tried it out and got the user propagator down to around 430 checks which is much closer to the 360 of the offline approach (not sure where the 70 extra checks come from).
The solving time is now 23 seconds vs. 8 seconds. With some Java-side optimization I should get it down to 20-21 seconds.
I don't know where the remaining 12-13 seconds get lost though (only 4 seconds are spent on the Java-side, so it shouldn't just be Java-sided overhead). Maybe it is related to the fact that I have to distribute the conflict clauses over multiple callbacks? In case you have an idea on why the user propagator performs worse, please let me know.
Anyway, now I'm more confident that I can overcome the remaining gap by adding early propagation :).

Two minor last questions:
(1) Can I dynamically change smt.up.persist_clauses=true during solving?
(2) What is the conceptual difference between mk_th_axiom and mk_th_lemma?

[NikolajBjorner]

• 1 yes, but not tested. Altogether I will need some iterations on this new feature. For example, it needs a fix for avoiding re-asserting the same clauses.
• 2 mk_th_axiom creates a clause that does not get garbage collected, expect when popping context. mk_th_lemma can be garbage collected. The idea is that mk_th_axiom is used to encode semantics of a theory, such as encoding the meaning of integer division using multiplication. mk_th_lemma is geared towards redundant clauses. A theory solver may produce lemmas that are consequences of existing theory axioms to shortcircuit search.