assumption in rc2

[you-li-nu]

Hello -

We have an algorithm which maintains a set of structures. In each iteration, we assert new values using solve(assumption) to assign new values to those structures. In this way, the structures can be reused in the incremental solving process.

Now we are attempting to adapt the algorithm to rc2. We observe that the compute() function in rc2 does not support assumption. Now we have 3 conjectures: (1) modify compute() so that it will support assumption. Is this possible? (2) garbage collect the clauses of the structures after each iteration. How to achieve this in rc2? (3) add new structures before each iteration, keep the old structures unchanged, but increase the weight for the new clauses. Such that the old structures are decayed.

We are looking forward to your suggestions. Thanks.

[alexeyignatiev]

Hi @you-li-nu,

This is a very good question. Unfortunately, I don't know of any MaxSAT solvers that support incrementality in the manner of MiniSat-like assumptions interface. Actually, implementing one efficiently represents a significant engineering effort.

I have a yet unpublished version of RC2 that does it. But I am not sure when it will become ready to be available. Also, I know that the group of Matti Järvisalo have been working on an incremental hitting-set based MaxSAT solver like MaxHS. As far as I know, they may have some preliminary results. Not sure about solver availability though.

As for PySAT and RC2, can you give me a simple example of what exactly your needs are (a small bunch of clauses and 2-3 iterations of MaxSAT calls)? This way I can think over possible ad hoc implementations for your needs.

[you-li-nu]

Hi Alexey,

Thanks for your reply!

Actually what we have is a function: F(p, q, y), where p, q are two input vectors and y is the output vector. We initiate F_1 ... F_n in parallel, which are all identical in structure. All p1 ... pn = p are forced to be identical. In each iteration, we choose new values for q1 ... qn and add them to the 'assumption', and then use maxsat solver to solve for p, such that the maximal number of (yi, yj), i, j /in 1...n are different. After each iteration, we add some constraint based on the returned p to all F.

Now if we are not allowed to use assumption, we could add q1 ... qn as hard clauses instead, and add new F1 ... Fn on top of previous ones in each iteration. Then we could assign a greater weight to the soft clauses of the new functions, such that the old functions are decayed. Even though, the model gets larger and larger after every iteration, as we are adding new F1 ... Fn instead of reuse previous ones. So probably we need to create new solvers after several iterations to delete unused F.

Is there a better approach? Thank you in advance!

[alexeyignatiev]

I can't say that I understand much. Is it correct that your p's are just unconstrained variables used in F's and the (unweighted) soft clauses are pairs (yi, yj)? Also, are q's meant to be assumptions under which different observations can be made for F's/y's?

[Nangos]

Hi Alexey,

I am you-li-nu's teammate currently in charge of the system implementation. I should be able to provide more details.

The p's are not directly constrained (in the sense that no unit clauses contain p), but for each iteration the solver runs, a lot of hard clauses that indirectly constraint the p's are added to the CNF. The q's are just used as a heuristic guide in our algorithm, and they need to be directly constrained (i.e. hard-coded) to different values for each iteration. Therefore, although these indirect constraints for p's can be added incrementally, the direct constraints for q's are ad-hoc (i.e. they should only exist in the current iteration). The problem is that, these ad-hoc constraints, which could be modeled as assumptions, do not have an easy implementation with the current RC2.

As for the (y_i, y_j) pairs, they are actually fixed soft constraints, each weighing the same, that need no change once initialized. For each iteration, the values of p's should be chosen by the MaxSAT solver for the "maximal number of (yi, yj), i, j /in 1...n are different".

Currently, we simply recreate a new solver for each iteration. As a result, if the algorithm runs for O(n) iterations, the number of operation of adding a clause is O(n^2). We wonder if there might be more efficient approaches based on the newest RC2 under development.

Thank you again for your timely replies to us.

[alexeyignatiev]

Hi Guannan,

Well, I am afraid the best option for you may be to recreate a solver from scratch, just like what you already do.

Alternatively, you can try to add new constraints on the q variables by giving them a weight larger than the sum of all the soft clauses from the previous iterations. This should work, with no solver restart needed. But the solver's state may become messed up by the older cores after a number of iterations.

What you really need is a MaxSAT solver having an incremental assumptions-like interface a-la MiniSat. Currently, RC2 does not have such capability (and to the best of my knowledge, none of the MaxSAT solvers do). It should do so eventually as I believe this is the way to go. As I mentioned in my earlier replies, the group of Matti Järvisalo have been working on an incremental MaxHS-like solver. They have a paper accepted at CP'21 (the conference will be later this month). I am not sure if the implementation is already available but you may want to find out.

[Nangos]

Thank you very much for the timely reply!