[IPASIR UP] Search with uninitialized search limits

[Dekker1]

When implementing a lazy solving approach, I ended up in a situation where Cadical (with the IPASIR UP interface) would start with an empty formula, where the check_model callback in the ExternalPropagator would then add the initial clauses. Although this callback proceeded correctly, Cadical would then immediately return the “unknown” result.

I managed to trace this back to Cadical checking the search limits in the extended CDCL loop, and because its limits weren't initialized would immediately exit. I found that ensuring that the limits always get initialized when having an external propagator in Internal::solve seems to solve a problem.

I’ve attached a patch with this small change and an additional assertion that limits are initialized when checked. I’d love to hear whether this is the correct approach, or whether I’m overlooking something.

ipasirup_init_limits-1.patch

[m-fleury]

The general idea of the interface is that you add the initial clauses before asking cadical to solve the problem (instead of adding them during the check_model).

But we should fix this, thanks for reporting.

@kfazekas is mobical able to generate such problems (so empty and only adding clauses during check_model)?

[m-fleury]

This was not fixed in 2.1, please continue adding at least one clause before calling solve.

[Dekker1]

A shame no fix made it into the 2.1 release. There certainly seem to be some great IPASIR-UP improvements in there.

I’m not sure whether the closing of this issue meant that no fix is planned for this issue. I just wanted to note that it is not just when no clauses are added to the solver (which not uncommon in our LCG solver), but this issue occurs also when the formula is solved during presolving. This makes the issue trickier than just “adding at least one clause” from the user side.

[m-fleury]

Reopening the issue.

but this issue occurs also when the formula is solved during resolving

What resolving do you mean here?

[Dekker1]

Sorry, that was meant to say “presolving” but got corrected by my phone 😅

[m-fleury]

Yeah but I am still confused how you trigger that.

int Internal::solve (bool preprocess_only) {
...
  int res = already_solved ();
  if (!res && preprocess_only && level)
    backtrack ();
  if (!res)
    res = restore_clauses ();
  if (!res) {
    init_preprocessing_limits ();
    if (!preprocess_only)
      init_search_limits ();
  }
  if (!res && !level)
    res = preprocess ();

You have a way to run the solver without hitting init_preprocessing_limits (). For this to happen you would need to have already_solved () to be non-zero in the first call, which only happens when (i) the problem was already unsat (cannot be); (ii) the constraints are trivially unsat (possible, but odd), (iii) the problem is empty (you claim it is not the case).

Or am I missing something?

Edit: or some example where this happens would be helpful.

[Dekker1]

Sorry. It seems that I might have misjudged this. I’ve only run into this issue when by happenstance creating formulas with no initial clauses. However, I saw the propagate() call in the already_solved () function and assumed that if propagation fixes everything this would also lead to the same situation. Now, looking in more detail, I believe that you are right, and this only seems to happen for empty formulas.

Still I would love to see a merged fix for this problem. The current behaviour that still calls the check_model callback, but then aborts the search because of the uninitialised search limits, seems clearly wrong. The required patch also seems minute, and the same check is done for other steps.