ConSol-Lab / Pumpkin

A lazy clause generation constraint solver written in Rust.
Apache License 2.0
17 stars 4 forks source link

PanicException thrown for UNSAT models #79

Closed IgnaceBleukx closed 3 weeks ago

IgnaceBleukx commented 3 weeks ago

Hi,

I have a very simple unsatisfiable model in Python which, when posted to Pumpkin causes an exception. Other UNSAT models run fine.

The following code reproduces the issue on the main branch:

mport pumpkin_py as pm

model = pm.Model()

p = model.new_integer_variable(0,3,name="p")
q = model.new_integer_variable(0,3,name="q")
r = model.new_integer_variable(0,3,name="r")
s = model.new_integer_variable(0,3,name="s")

from pumpkin_py import constraints

c1 = constraints.LessThanOrEquals([s.scaled(3), p,r], 1)
c2 = constraints.AllDifferent([p,q,r,s])

model.add_constraint(c1)
model.add_constraint(c2)

model.satisfy()

Raises the following stacktrace:

hread '<unnamed>' panicked at pumpkin-solver/src/engine/constraint_satisfaction_solver.rs:407:9:
assertion failed: self.is_conflicting()
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
Traceback (most recent call last):
  File "/tmp/test.py", line 18, in <module>
    model.satisfy()
pyo3_runtime.PanicException: assertion failed: self.is_conflicting()
ImkoMarijnissen commented 3 weeks ago

Thank you for raising this issue; I will take a look at what is happening!

IgnaceBleukx commented 1 week ago

Thanks, this is indeed fixed in the commit you mentioned :)