A scip model for solving the puzzle at https://www.puzzleprime.com/brain-teasers/deduction/broken-clock/

broken-clock.zpl

# A scip model for solving the puzzle at
# https://www.puzzleprime.com/brain-teasers/deduction/broken-clock/

set hours  := { 1..12 };
set pieces := { 1..3 };

# definition of next hour (modulo 12)
defnumb nexthour(h):= if (h==12) then ( 1) else (h+1) end;

# m[h,p]=1 means that the number h belongs to piece p
var m[hours * pieces] binary;
# each number belongs to exactly one piece
subto sph: forall <h> in hours  do sum <p> in pieces: m[h,p]==1;
# each piece contains at least one number
subto spn: forall <p> in pieces do sum <h> in hours : m[h,p]>=1;


# the sum of numbers on each piece
var sum1 integer; var sum2 integer; var sum3 integer;
subto shp1r: sum <h> in hours: h*m[h, 1] == sum1;
subto shp2r: sum <h> in hours: h*m[h, 2] == sum2;
subto shp3r: sum <h> in hours: h*m[h, 3] == sum3;
# the sum of the numbers on each piece is the same
subto sum1: sum1 == sum2;
subto sum2: sum1 == sum3;


# on which piece is a given number found?
var hour2piece[hours] integer >=1 <=card(pieces);
subto bl: forall <h,p> in hours*pieces do
	vif m[h,p]==1 then hour2piece[h]==p end;

# does a piece change take place at a given hour?
var piece_change_at[hours] binary;
subto pca1: forall <h> in hours do
	vif (hour2piece[h] != hour2piece[nexthour(h)])
		then piece_change_at[nexthour(h)]==1
		else piece_change_at[nexthour(h)]==0
	end;


# there are exactly 3 piece changes if all the pieces are slices
#        or exactly 4 piece changes if all the pieces are "bands"
subto pc3: sum <h> in hours: piece_change_at[h] >= 3;
subto pc4: sum <h> in hours: piece_change_at[h] <= 4;