Retrieve literals fixed under assumptions

[avdgrinten]

Hi,

I am using CaDiCaL to solve an application problem. I use the fixed () function to extract literals that the solver fixes. However, I would be even more interested in literals that are fixed under the current set of assumptions. (Use case: in case the solver yields an indetermine answer due to hitting a conflict limit, these literals further restrict the solution of my application problem and allow application-specific simplication.)

Can I simply add a modified version of fixed () to Internal that also considers decision levels above zero and wire it up via an External::assumption_fixed () to Solver::assumption_fixed ()?

  int assumption_fixed (int lit) {
    // ... (same as fixed ())
    if (res && vtab[idx].level > assumptions.size()) res = 0;
    if (lit < 0) res = -res;
    return res;
  }

Questions:

1. Are there any caveats? (I am not sure if CaDiCaL keeps assignments at decision level > 0 after a solve () call and whether the internal/external interface complicates this issue.)
2. Can I easily force the solver to stop after propagating the assumptions but before doing any real decisions? Combined with the function above that would allow a quick check whether a given set of literals implies other literals (while taking learnt clauses into account).

Best,
Alexander

[arminbiere]

This is a common requested feature (for integrating SAT solvers in MaxSAT and SMT solver). For an ASE'16 paper (section 7 - called it 'imply') on combinatorial testing we added something like that to a (separate) Lingeling version. I promised to implement this for MaxSAT users for some time now, but do not have an ETA. It would require to have a separate externally visible state though (maybe call it 'IMPLIED') and changes to the model based tester too. Then 'val' (I would just reuse that instead of 'assumption_fixed') should be allowed to be called in IMPLIED state too ...

[avdgrinten]

The imply(int lit) interface from your ASE'16 paper looks a lot cleaner than what I had in mind, indeed. Good to know that this is under consideration and thank you for your response!

[arminbiere]

I still did not get around to do this properly. One could in principle also just misuse the decision limit. I know of several users of CaDiCaL who used this approach.

[marekpiotrow]

I would like to use this property in the UWrMaxSat project. Could you explain in more details how to misuse the decision limit.

[arminbiere]

Before calling the solver you set the decision limit to zero. You can do this before or after adding assumptions. Then call the solver. It then returns immediately after just propagating the assumptions. If this gives a conflict you can even get failed assumptions (the core). Note, that there are lots of corner cases, that need to be checked by the caller.

I also just figured after reviewing the 'failing' code, that failed assumption cores are maybe in general in CaDiCaL too big: for root-level falsified literals the core should be empty while my current code marks them as failed. This is not incorrect though, since cores are not guaranteed to be minimal. Maybe the caller is already checking with 'fixed' whether an assumption is root-level implied.

Another issue is, that you might want to be able to obtain implied literals (from the assumptions). This is not doable at the point.

Finally, note that, CaDiCaL is optimized for heavy weight assumption usage (at this point), as in bounded model checking, where you usually only have one assumption or in general |assumptions| << |formula|. For the typical usage in MaxSAT with many assumptions there are some expected performance issues. As with most other solvers, completely resetting the solver after each call and reassuming all the assumptions even if only some changed is bad. There are published solutions for that (Randy Hickey with Fahiem Bacchus in SAT'19 and Jean-Marie Lagniez and myself in SAT'13), but this has not been properly integrated yet.

Anyhow, for your usage (unless you really need the implied literals from assumptions) you can do the following:

solver.add (...);
// add hard constraints first
...
solver.add (...);
solver.assume (...);
// add assumptions or soft constraints next
...
solver.assume (...);
solver.limit ("decisions", 0); // set decision limit to zero
int res = solver.solve ();
if (res == 0) {
  // Maybe something implied but no conflict.
  // You can not use 'solver.val (...)' here.
} else if (res == 20) {
  solver.failed (...); // Work with failed assumptions as usual
  ...
} else {
  assert (res == 10); {
  // You can get the assignment.
  ... solver.val (...);
}

[cormackikkert]

Hi Armin, does the separate version of lingeling, the one that implements imply(int lit) , allow obtaining implied literals (from assumptions)?

If not are you aware of any other SAT solvers I could use that allows this functionality?

Thanks,
Cormac

[arminbiere]

I would not recommend using that experimental version of Lingeling, but in principle yes, it is possible to add that functionality to CaDiCaL, but it will take some effort, for which at the very moment, right before competition deadline, we do not really have any cycles left.

[arminbiere]

Ok, I think in principle Katalins' (@kfazekas) new user propagator code allows to do at least a partial version of this now. What I mean with partial is that you get the literals implied by the assumed literals out of the solver. This might be different though what the original intention was, which could be interpreted to retrieve the backbones under assumptions. This is a totally different game though. If it is the former we can try to give an example for this.