Error when propagator returns unit conflict explanation

[ImkoMarijnissen]

When a Propagator returns a unit conflict explanation, the resolution conflict analysis breaks since it attempts to allocate a clause but the clause manager only accepts clauses of size 2

[EmirDe]

Under which circumstances did you encounter this problem?

Normally we would not expect to encounter a conflict from a propagator that is composed of a single predicate, since that would have been propagated at the root level. At least we would expect that behaviour with our propagators, although maybe our half-reified propagation does not (?).

[ImkoMarijnissen]

I encountered it with the constraint x in {1, 2, 3} and the constraint x <= 0, in which case the proof logging attempts to create a final learned clause when completing the proof but it cannot due to this issue; I think the half-reified propagator would not run into this problem since it would always add the reified literal to the unit explanation.

Would this always only hold at the root level? If a propagator always reasons as strongly as it can then I can imagine that to be true but is this an assumption we want to make about the propagator? For example, if we have a not equals propagator which only detects conflicts then it could indeed return a unit explanation at a non-root level.

[IgnaceBleukx]

I actually had this exact issue with another problem as well when trying to model an unsatisfiable 4x4 Latin Square using AllDifferent constraints:

import pumpkin_py as pm
from pumpkin_py import constraints

model = pm.Model()

vars = dict()
for i in range(4):
    for j in range(4):
        name = f'cells[{i},{j}]'
        vars[name] = model.new_integer_variable(1,4,name=name)

#row constraints
for i in range(4):
    cons = constraints.AllDifferent([vars[f'cells[{i},{j}]'] for j in range(4)])
    model.add_constraint(cons)

# column constraints
for j in range(4):
    cons = constraints.AllDifferent([vars[f'cells[{i},{j}]'] for i in range(4)])
    model.add_constraint(cons)

# given values
""" 
[[0,2,0,0],
 [0,1,0,4],
 [0,0,2,0],
 [0,0,3,0]]
"""

model.add_constraint(constraints.Equals([vars['cells[0,1]']], 2))
model.add_constraint(constraints.Equals([vars['cells[1,1]']], 1))
model.add_constraint(constraints.Equals([vars['cells[1,3]']], 4))
model.add_constraint(constraints.Equals([vars['cells[2,2]']], 2))
model.add_constraint(constraints.Equals([vars['cells[3,2]']], 3))

model.satisfy()

[EmirDe]

There are a few things that sound unusual to me, so good to check. Perhaps it would be easier to discuss in person when I get back but for now here are a few notes.

Conceptually, it is possible that a propagator reports a unit-sized conflict at a non-root level. But in practice we do not have this situation. For example, unless I am mistaken, none of our current propagators would do that, i.e., we would expect all our propagators to do these "simple" propagations already at the root. The fact that we had this situation might indicate a bug somewhere?

We normally never call conflict analysis at the root level. For example, if a propagator fails at the root level, the solver simply report infeasibility.

I suppose there may be a problem when we want to generate the full proof for problems that are unsatisfiable at the root level (before any search takes place - I guess this is also the problem with the Ignace's example). Say we have the constraint x >= 5 and x <= 4. Perhaps we need to handle this as a special case? Good to check with Maarten, I cannot fully recall what we agreed on for the new version of the proof producer.

It could be that a simple workaround is to allow allocating clauses of size one. This is a bit dangerous, since we cannot add a unit clause to the two watcher scheme, so we need to make sure that we do not attempt to create unit clauses in any other case.

But as far as the conflict analysis goes, after seeing a unit clause, the analysis will stop since unit clauses are asserting. After the analysis is done, explanation clauses are cleaned up any way, so the unit clause will not remain in the data structures. So things seem okay to me.

(The good news is that the revamped version does not have this problem.)

This ended up being a long post, perhaps it is indeed best if we discuss in person next week!

[maartenflippo]

I actually had this exact issue with another problem as well when trying to model an unsatisfiable 4x4 Latin Square using AllDifferent constraints:

import pumpkin_py as pm
from pumpkin_py import constraints

model = pm.Model()

vars = dict()
for i in range(4):
    for j in range(4):
        name = f'cells[{i},{j}]'
        vars[name] = model.new_integer_variable(1,4,name=name)

#row constraints
for i in range(4):
    cons = constraints.AllDifferent([vars[f'cells[{i},{j}]'] for j in range(4)])
    model.add_constraint(cons)

# column constraints
for j in range(4):
    cons = constraints.AllDifferent([vars[f'cells[{i},{j}]'] for i in range(4)])
    model.add_constraint(cons)

# given values
""" 
[[0,2,0,0],
 [0,1,0,4],
 [0,0,2,0],
 [0,0,3,0]]
"""

model.add_constraint(constraints.Equals([vars['cells[0,1]']], 2))
model.add_constraint(constraints.Equals([vars['cells[1,1]']], 1))
model.add_constraint(constraints.Equals([vars['cells[1,3]']], 4))
model.add_constraint(constraints.Equals([vars['cells[2,2]']], 2))
model.add_constraint(constraints.Equals([vars['cells[3,2]']], 3))

model.satisfy()

Just as in https://github.com/ConSol-Lab/Pumpkin/issues/116, this should be fixed in feat/remove-explicit-literals