Unexpected behavior for very big groundings

[bonetblai]

I'm getting an unexpected UNSAT result for a program that results in a very big ungrounding (memory requirement is about 40Gb). In the attached .zip file there are 4 test cases that are explained in the file clingo_calls.txt. In all cases, the program is the same and what changes is a set of facts passed to the program, either mysolution0.lp, mysolution1.lp, mysolution2.lp, and choice.mysolution2.lp. These sets of facts satisfy the following: the facts in mysolution0.lp include all facts in mysolution1.lp which includes all facts in mysolution2.lp. Finally, the facts atom. in mysolution1.lp that do not appear in mysolution2.lp, appear in choice.mysolution2.lp as choices {atom.}

The outputs of the solver for each case, also in clingo_calls.txt, is SATISFIABLE for the first two cases and UNSATISFIABLE for the last two cases. This seems to be a bug in the solver due, perhaps, to the very large grounded program. I haven't been able to find a smaller example where this happens.

The solver is Clingo version 5.5.0

test.zip

[rkaminsk]

This might be due to an overflow. Not all overflows are detected. But if the number of supported atoms is exceeded, there should be an error message. Unfortunately, your encoding is too complicated and the grounding to big. I won't have a look at it.

[bonetblai]

Thanks for the quick answer. I have seen overflows due to number of atoms before, but this is not happening here. There is no error message, I have plenty of memory, and it seems that the grounder has finished. Any overflow might be happening within the solver. The output is below. If you give me some pointers inside the code, I might try to identify where the overflow occurs.

clingo version 5.5.0
Reading from solver_alt.lp ...
Solving...
UNSATISFIABLE

Models       : 0
Calls        : 1
Time         : 858.270s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 858.256s
Threads      : 6        (Winner: 0)

[rkaminsk]

The problem is immediately found unsatisfiable. Usually, I would try to find if there is a conflicting constraint before trying to find bugs in clingo. If you have the conflicting constraints, you can try to figure out why it is conflicting. Only if this fails, I would look at the code. That being said, maybe one of the HashSets/Vectors gets too large. You could add something like if (size >= 0x40000000) { throw std::runtime_error("sets getting dangerously large") } to the reserve methods in libgringo/gringo/hash_set.hh. I don't remember the exact supported size limits right now. Usually, the number of atoms gets problematic first because the grounder supports more symbols than the solver atoms. Glancing at your encoding it also does not look like integer overflows elsewhere should be problematic.

[rkaminsk]

This seems to be a problem in clasp's equivalence preprocessor. Removing option --sat-pre=0 and adding --eq=0 results in solutions. So it could either be a bug or overflow in the preprocessor. The size of the problem makes it very hard to debug this.

clingo-banane -c max_action_arity=4 -c num_predicates=12 --fast-exit --time-limit=57600 --eq=0 --stats=2 solver_alt.lp \
    grid-1rows-2cols-0shapes-0keys-0locks.lp \
    grid-1rows-2cols-1shapes-1keys-0locks.lp \
    grid-1rows-2cols-1shapes-2keys-0locks.lp \
    grid-2rows-1cols-0shapes-0keys-0locks.lp \
    grid-2rows-2cols-0shapes-0keys-0locks.lp \
    grid-2rows-2cols-1shapes-1keys-0locks.lp \
    grid-2rows-2cols-1shapes-1keys-1locks.lp \
    grid-2rows-2cols-1shapes-1keys-2locks.lp \
    grid-2rows-2cols-1shapes-2keys-1locks.lp \
    grid-2rows-2cols-2shapes-2keys-1locks.lp \
    partial.lp \
    mysolution2.lp
clingo version 5.6.0 (5454cef4)
Reading from solver_alt.lp ...
Solving...
Answer: 1
...
Optimization: 34 14 14 53 106
...
...
...
Answer: 607
...
Optimization: 34 8 10 28 52
*** Info : (clingo): INTERRUPTED by signal!
SATISFIABLE

TIME LIMIT   : 1
Models       : 607+
  Optimum    : unknown
Optimization : 34 8 10 28 52
Calls        : 1
Time         : 57600.031s (Solving: 57174.23s 1st Model: 1838.46s Unsat: 0.00s)
CPU Time     : 57597.908s

Choices      : 35947441
Conflicts    : 8970159  (Analyzed: 8970158)
Restarts     : 16381    (Average: 547.60 Last: 8880106)
Model-Level  : 511.1
Problems     : 1        (Average Length: 0.00 Splits: 0)
Lemmas       : 8970158  (Deleted: 8934274)
  Binary     : 1458     (Ratio:   0.02%)
  Ternary    : 1219     (Ratio:   0.01%)
  Conflict   : 8970158  (Average Length:   82.3 Ratio: 100.00%)
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%)
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%)
Backjumps    : 8970158  (Average:  3.88 Max: 7161 Sum: 34823745)
  Executed   : 8970158  (Average:  3.88 Max: 7161 Sum: 34823745 Ratio: 100.00%)
  Bounded    : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio:   0.00%)

Rules        : 152771302 (Original: 152366044)
  Choice     : 69206
  Minimize   : 5
Atoms        : 136065421 (Original: 136050581 Auxiliary: 14840)
Bodies       : 53274217 (Original: 52883919)
  Sum        : 30
  Count      : 472      (Original: 1529)
Equivalences : 33976207 (Atom=Atom: 0 Body=Body: 0 Other: 33976207)
Tight        : Yes
Variables    : 100894219 (Eliminated:    0 Frozen: 215797)
Constraints  : 68485561 (Binary:  89.9% Ternary:   9.9% Other:   0.2%)

[rkaminsk]

@BenKaufmann, this seems to be a bug in clasp's preprocessor. I have no clue how to debug this because the ground/nonground program is too large.

[rkaminsk]

This is indeed an overflow that is unfortunately not checked. The following patch correctly reports the problem:

diff --git a/src/logic_program_types.cpp b/src/logic_program_types.cpp
index 8008120..8f03dcf 100644
--- a/src/logic_program_types.cpp
+++ b/src/logic_program_types.cpp
@@ -546,6 +546,7 @@ PrgAtom::PrgAtom(uint32 id, bool checkScc)
 void PrgAtom::setEqGoal(Literal x) {
        if (eq()) {
                data_ = x.sign() ? x.var() : noScc;
+               POTASSCO_CHECK(data_ == (x.sign() ? x.var() : noScc), EOVERFLOW, "Id out of range");
        }
 }
 Literal PrgAtom::eqGoal(bool sign) const {

The data_ field only has 27 bits but we need 28 bits to represent all the atoms. @BenKaufmann, we should probably add a test (maybe a bit nicer). Or maybe we can we somehow raise this limit?

[rkaminsk]

Clingo now reports an overflow if preprocessing is enabled. Unfortunately, there is no easy way to simply raise this limit.