Analyzing infeasibility and handling conflicts
In many cases the return status 'problem infeasible' or ' constraint inconsistent' is not a desirable situation since we really wish to find a solution to the problem we are solving. To support the user's analysis of the cause of the infeasibility Kalis can generate reports about sets of infeasible constraints. During the development of a model such a facility helps tracking model formulation errors and in applications inconsistencies in data are identified more easily.
We shall work once more with the Sudoku example from Section all_different: Sudoku. Instead of launching the enumeration through the CP solver we now prompt the user to input a value for a randomly chosen cell. If the value set by the user leads to an inconsistent state of the constraint system we invoke the solver display of the minimal set of constraints causing the infeasibility.
Implementation
The problem statement and setting of start data remain exactly the same as with the standard implementation of the problem seen in Section all_different: Sudoku. What is new are the prompt for user input and the subsequent handling of infeasibilities. The underlying mechanisms are markers (often referred to as choice points) to save the state of the constraint solver at a given moment and the possibility to return to the last such saved state. The corresponding Mosel subroutines are cp_save_state and cp_restore_state. After stating a new constraint but before propagating its effect (the automated propagation has been switched off through the setting of AUTO_PROPAGATE at the beginning of the model) we save the state of the constraint system. If the new constraint turns out to be infeasible the solver is set back to the state before the constraint propagation and we can then invoke the infeasibility analysis (cp_infeas_analysis).
The subroutine for solution printing has been replaced by a routine printing the values of all fixed variables.
model "Conflicts"
uses "kalis"
forward procedure print_values
setparam("kalis_default_lb", 1)
setparam("kalis_default_ub", 9) ! Default variable bounds
declarations
XS = {'A','B','C','D','E','F','G','H','I'} ! Columns
YS = 1..9 ! Rows
v: array(XS,YS) of cpvar ! Number assigned to cell (x,y)
end-declarations
forall(x in XS,y in YS) setname(v(x,y), "v("+x+","+y+")")
setparam("KALIS_AUTO_PROPAGATE", 0) ! Disable automatic propagation
! Data from "The Guardian", 29 July, 2005. http://www.guardian.co.uk/sudoku
v('A',1)=8; v('F',1)=3
v('B',2)=5; v('G',2)=4
v('A',3)=2; v('E',3)=7; v('H',3)=6
v('D',4)=1; v('I',4)=5
v('C',5)=3; v('G',5)=9
v('A',6)=6; v('F',6)=4
v('B',7)=7; v('E',7)=2; v('I',7)=3
v('C',8)=4; v('H',8)=1
v('D',9)=9; v('I',9)=8
! All-different values in rows
forall(y in YS) all_different(union(x in XS) {v(x,y)})
! All-different values in columns
forall(x in XS) all_different(union(y in YS) {v(x,y)})
! All-different values in 3x3 squares
forall(s in {{'A','B','C'},{'D','E','F'},{'G','H','I'}}, i in 0..2)
all_different(union(x in s, y in {1+3*i,2+3*i,3+3*i}) {v(x,y)})
! Prompt user for new assignments
declarations
NX: array(1..9) of string
val: integer
end-declarations
NX::(1..9)['A','B','C','D','E','F','G','H','I']
cp_save_state
res:=cp_propagate
print_values
setrandseed(3)
while (res and (or(x in XS,y in YS) not is_fixed(v(x,y))) ) do
! Select randomly a yet unassigned cell
rx:=round(0.5+9*random); ry:=round(0.5+9*random)
while (is_fixed(v(NX(rx),ry))) do
rx:=round(0.5+9*random); ry:=round(0.5+9*random)
end-do
! Prompt for user input
writeln(v(NX(rx),ry), " = ")
readln(val)
! Add the new constraint
v(NX(rx),ry)=val ! State a new constraint
cp_save_state ! Save system state before propagation
res:=cp_propagate ! Propagate the new constraint
! Print resulting board
print_values
end-do
! An infeasible state has been reached
if not res then
cp_restore_state ! Restore state before propagation
cp_infeas_analysis ! Analyze infeasibility, print report
else
writeln("Problem solved")
end-if
!****************************************************************
! Print fixed values
procedure print_values
writeln(" A B C D E F G H I")
forall(y in YS) do
write(y, ": ")
forall(x in XS)
write(if(is_fixed(v(x,y)), string(getval(v(x,y))), "."),
if(x in {'C','F'}, " | ", " "))
writeln
if y mod 3 = 0 then
writeln(" ---------------------")
end-if
end-do
end-procedure
end-model
Results
With the following user value input sequence:
v(F,7)[1,5..6,8] = 1 v(I,1)[1..2,7,9] = 1 v(I,8)[2,6..7] = 2
we obtain an infeasibility for the third value. The values printed at this stage and the report generated by the solver show why this value leads to a conflict.
A B C D E F G H I 1: 8 . . | . . 3 | . . 1 2: . 5 . | . . . | 4 . 7 3: 2 . 1 | . 7 . | . 6 9 --------------------- 4: . . . | 1 . . | . . 5 5: . . 3 | . . . | 9 . . 6: 6 . . | . . 4 | . . 7 --------------------- 7: . 7 . | . 2 1 | . . 3 8: . . 4 | . . . | . 1 2 9: . . . | 9 . . | . . 8 --------------------- ------------------------ Minimal Conflict Set ------------------------ 1 : AllDifferent(v(I,1),v(I,2),v(I,3),v(I,4),v(I,5),v(I,6),v(I,7),v(I,8),v(I,9 ))
Note: in the present example we examine the effect of adding just a single (bound) constraint to our problem. However, the infeasibility analysis functionality can be applied for any number and type of constraints.