Using the feature of incremental SAT to solve a sequence of SAT problems

[yulinzhang]

Hi, I am using the incremental SAT feature of cadical to solve a sequence of SAT problems:
problem 1: a or b or c or d
problem 2 with an additional clause: not a
problem 3 with an additional clause: not b
problem 4 with an additional clause: not c
I want to output the solutions for each of these problems.

Here is the input file:
p inccnf
1 2 3 4 0
a -1 0
a -2 0
a -3 0

But it only shows me the result of the first cube: -1 2 3 4 0

Is there anything wrong with my command (cadical input.cnf) or specification?

Really appreciate your help.

[arminbiere]

This 'inccnf' format was originally invented by Siert Wieringa for API less bounded model checking, where you are searching for the first assumption which satisfied the formula and then actually exit. This is the default behavior for CaDiCaL now. Can you motivate an application where this is different?

Here the corresponding excerpt from usage ('cadical --help'):

For incremental files each cube is solved in turn. The solver
stops at the first satisfied cube if there is one and uses that
one for the witness to print. Conflict and decision limits are
applied to each individual cube solving call while '-P', '-L' and
'-t' remain global. Only if all cubes were unsatisfiable the solver
prints the standard unsatisfiable solution line ('s UNSATISFIABLE').

[yulinzhang]

I want to use the incremental SAT feature:

Many applications of SAT are based on solving a sequence of incrementally generated SAT instances. In such scenarios the SAT solver is invoked multiple times on the same formula under different assumptions. Also the formula is extended by adding new clauses and variables between the invocations. It is possible to solve such problem by solving the incrementally generated instances independently, however this might be very inefficient compared to an incremental SAT solver, which can reuse knowledge acquired while solving the previous instances (for example the learned clauses).

If I understand correctly, it asks you to solve a sequence of SAT problems, which are by built incrementally adding clauses or assumptions. The solver will only exit when there is no solution to the current problem, since there is no way to satisfy future problems with additional constraints.

I saw that cadical does implement ipasir.h, which is related to the incremental SAT feature. But I just wonder whether there is any command-line tool that allows me to use this feature, instead of using C/C++ code.

[arminbiere]

It would be possible to add for instance printing the solution each time rather easily. However, I am curious about applications of this and if there aren't any, there is no point of adding this feature. In 'UNSAT, ..., UNSAT, SAT' applications where you are seeking a first model, it is clear what you want (just use that first model). In the 'SAT,SAT' situation, it is unclear what you do with this first model. The choice of the set of assumptions (for the second model) can not depend on the actual values of the first model. For instance I could add a '--continue' or '--all' flag that continues solving assumptions and does not stop at the first satisfiable one. Again, do you have a real use case for this?

[yulinzhang]

Yes. I am trying to use SAT solver to solve a particular optimization problem, which can be specified by a set of boolean constraints and an enumerable objective function. The values of the objective function are small bounded integer values, which can be enumerated easily. Hence, for each value of the objective function, we got an SAT instance. We are interested in finding the minimum objective value such that the corresponding SAT instance is satisfied.

An example is minimum graph coloring: the objective function k is the total number of colors being used, and the constraints are from graph coloring. Each k will give you a k-graph coloring problem, which is modeled by an SAT problem with parameter k. To find the minimum k, we will decrease k from n (the number of vertices in the graph) to 1, and solve the corresponding k-SAT problem. This gives us a sequence of k-SAT problems, and we are interested in finding the minimum k that can be satisfied.

If you are trying to model this problem, the k-1-graph coloring can be constructed from k-graph coloring with additional clauses. In addition, it is a 'SAT, SAT, SAT, ..., UNSAT' situation.

[arminbiere]

Then do you only need the last model? So could have a command line option '--last' ...

[yulinzhang]

Right, I only need the last model. But I do not want the solver to quit after seeing a single "satisfaction". I want it to continue solving new instances. I guess, for now, I can only call ipasir.h to implement this (I did not find "--last" being supported as a command-line option in the latest release of cardical).

[arminbiere]

I think this is indeed a valid use question for the 'inccnf' input. I will keep this on my TODO stack for the next release.

[yulinzhang]

Thanks.