I have a huge problem with many (propositional and numerical) variables. I am not interested in most of the values of these variables and would like them to remain unassigned in my solution.
Specifically, similarly to a constraint network, I would like to assign some values to some variables and just check whether the constrains propagate or not. Moreover, I would like to do it incrementally (e.g., assign true to variable v0 and check if it propagates, then assign true to variable v5 and check if it propagates together with v0 at true, and so on..).
This is something similar to consequences which, however, seem to perform a complete assignment to the variables which, by performing a complete search, results, in my case, to be too much. Pushing and popping looks also similar but, again, propagation does not seem to occur unless you call the check procedure which, once more, performs a complete search.
Somehow related to z3: Is it possible to adjust the branching heuristics in Z3?, my problem has a particular structure which I would like to exploit in order to guide the search. So, another option would be to build my own solver which decides the next propositional variable's polarity, asks Z3 to propagate and to analyze possible conflicts, and stops the search whenever I like.
So, which is the best way to use Z3 as a constraint network? How hard would it be to build my own solver to drive the CDCL(T) search?
