Index-error during clause-allocation

[IgnaceBleukx]

Hi,

Potentially related to #118 (I encountered this case when minimizing an example for that issue).

I have the following piece of code for generating an UNSAT model:

from pumpkin_py import Model, constraints, Comparator

n = 3    
model = Model()

bvs = [model.new_boolean_variable(name=f"BV{i})") for i in range(n)]
ivs = [model.new_integer_variable(0,1,name=f"IV{i}") for i in range(n)]

neg_scaled = [model.boolean_as_integer(b).scaled(-1) for b in bvs]
model.add_constraint(constraints.LessThanOrEquals(neg_scaled, -1))

for i in range(n):
    is_0 = model.predicate_as_boolean(ivs[i], Comparator.Equal, 0)
    is_1 = model.predicate_as_boolean(ivs[i], Comparator.Equal, 1)

    model.add_constraint(constraints.Clause([is_1]))
    model.add_implication(constraints.Clause([is_0]), bvs[i])

model.satisfy(proof="test")

This raises the error

thread '<unnamed>' panicked at pumpkin-solver/src/engine/sat/clause_allocators/clause_allocator_basic.rs:52:32:
index out of bounds: the len is 0 but the index is 18446744073709551615

I did a little investigation already, and the model runs fine when putting the constaint "sum(bvs) >= 1" all the way at the end of the model.

Feel free to close this issue if the root cause is the same as #118 : )

[maartenflippo]

I will have a look at this on Monday. You could try to see whether this error still persists on the develop branch. Based on the error message I assume you are currently running the latest main.

[IgnaceBleukx]

Thanks! I'm currently indeed running on main

[maartenflippo]

I spent some time exploring why this crashes on the develop branch. I have not been able to figure it out yet, and will do more work on it. But I have not forgotten about this issue