tactics: new Z3 tactic "partition"

[Adorf]

I should like to suggest a new Z3 tactic dubbed "partition" that partitions a given SMT-problem (CSP) into minimal independent components.

The partition algorithm works on the primal constraint graph. (1) If two variables appear together in a constraint, they end up in the same CSP-component. (2) A constraint that has a variable in one of the CSP-components, ends up in that component.

The "partition" tactic should be a splitting tactic like "split-clause". The constraints in each component should be combined into a separate goal.

A tactical such as "then" could be used to serially solve each of the component-CSPs.

A tactic such as "par-then" could be used to solve the component-CSPs in parallel. It would be very useful if one could limit the number of threads used by "par-then".

[wintersteiger]

Just to clarify: Are you proposing to contribute a new tactic, or are you asking whether we can implement this for you?

[Adorf]

I do have the partition algorithms ready. They are implemented in Java. I assume that you need the algorithms in C, correct? So, a way (collaboration?) would have to be found to port them to C and to integrate them into the Z3 solver so that they could be used as a tactic.

[NikolajBjorner]

There are union-find facilities and for_each_expr combinators that let you walk expressions, collection symbols and then using union-find collect representatives for each assertion, merge the classes and then you can generate subgoals. There are several tactics in src/tactics that provide enough copy-paste material for the code that goes around.

[wintersteiger]

Yes, like @NikolajBjorner said, many pieces of the puzzle are already available. Z3 is written in C++, so an existing object hierarchy may be very easy to port. If your algorithms are already based on Z3 ASTs, then it may literally be a purely syntactic translation.

I'd say we are interested, but at the moment I don't have much time that I could devote to this. I'd be happy to help with general implementation questions and strategies though.

[Adorf]

My algorithms are based on Java-classes that implement Scheme objects. Thus the base is not far away from an AST.

@wintersteiger: your comment sounds like a cooperation offer to me.

[wintersteiger]

@Adorf: Not exactly an offer. At the moment I don't have much time to offer to anybody, so I can't really make a committment. But, I'll happily support anyone who is interested in this and has time to spend on it.

[chadbrewbaker]

I have a similar issue. Application is finding min-dominating sets for graphs, and each connected component can be solved independently. Why the need for a tactic, and not just a model splitter that takes a model and splits it into a list of independent models?

[Adorf]

@chadbrewbaker: if the goal were to obtain a single solution, we would not need to partition the CSP. However, as described in another posting (https://github.com/Z3Prover/z3/issues/473), we are interested in solving each independent CSP-component several times with additional constraints. Small component-CSPs have a small number of additional constraints. Large component-CSPs have a large number of such constraints. Partitioning the oroginal CSP makes the solution process much more efficient. In addition, the component-solutions can freely be combined afterwards.

[Adorf]

Suppose there were a tactic partition, then the following statement would partition the input formula into goals comprising minimal independent components, and submit each to a separate SMT-solver working in parallel with the others:

(check-sat-using (par-then partition smt))

That would be nice, wouldn't it?

[Adorf]

As I have learnt in the meantime (see https://github.com/Z3Prover/z3/issues/478), the tactic

(par-then partition smt)

would not only execute the second tactic in parallel, but would also stop when the first sat were found by one of the SMT-solvers. Instead

(check-sat-using (then partition smt))

would have to be used. However, that statement, elegant as it is, would unfortunately not benefit from concurrency.

[Adorf]

As I have learnt in the meantime, my hypothetical statement

(check-sat-using (par-then partition smt))

posted in the issue https://github.com/Z3Prover/z3/issues/469, does not do what I wanted. It would not necessarily solve all components. Instead

(check-sat-using (then partition smt))

would have to be used. However that statement would unfortunately not benefit from concurrency.

[Adorf]

@chadbrewbaker: rethinking this issue in view of the discussions led in related issues (particular https://github.com/Z3Prover/z3/issues/479), there is another, generally more compelling reason for the hypothetical tactic partition to work on a goal rather than to partition the solution: if the hypothetical tactic par-do existed, one could write

(check-sat-using (par-do partition smt))

and the CSP would be solved in parallel, which could potentiallly be much more efficient. If you have n cores simultaneously working on the split problem, the original CSP might be solved in 1/n time. Of course, as usual, the gain through concurrency depends on the structure of the subproblems.

[cheshire]

@Adorf I think I have done something similar before, only my partition was based on a certain set of variables "interesting" to me. Couldn't all of this be successfully done outside of Z3 though? Your partitioning code then may even stay in Java. Just creating a separate context for each partition and solving each on a separate thread should do the trick?

[Adorf]

@cheshire: that is exactly what we are doing at the moment.

One of the questions I am pursuing is, how much of what we are currently doing (in Java) outside an SMT-solver can actually be incorporated into the solver, by using suitable existing and potentially new tactics or tactic-combiners (tacticals).

I'm pretty sure we are not the only ones who have CSPs that can be partitioned into independent components. And I'm absolutely certain we are not the only ones fighting the run-time problems caused by NP-completeness. If a tactical such as par-do were in place, every Z3 user would benefit from concurrency. This is much better than everyone writing his/her own partitioning algorithm and brittle multi-threading code for solving the CSP-components concurrently.

The Z3-solver has come a long way towards supporting demanding user-requirements. In this case it looks as if it were only an epsilon away from supporting partition.

[chadbrewbaker]

I'm interested in partitioning at the task queue level, then having whichever compute node is free pick up a model to solve. Partitioning should be available with a command line utility.

[Adorf]

@chadbrewbaker: would you mind being more specific?

[chadbrewbaker]

Rabbit/Celery task queue fires off AWS lambda jobs to crunch z3. Results go in a second queue for post processing.

[ghost]

Hello all,

What I understood from reading the comments on this issue is that the logic for implementing the new tactic is largely contained in @Adorf's java classes. If this is the case, I don't mind working on implementing the new tactic with some guidance and advice along the way.

[nunoplopes]

Closing this. Feel free to submit a PR when ready. Thanks!