Tiling¶
This is an adaptation of the tiling example from
Vladimir Lifschitz. An Experiment with Anthem: Semantic Equivalence of Tiling Programs. JELIA (1): 357-363 (2025).
The input is given by size/1 and the output by place/3. The problem comes
with two assumptions on the input: size has to be true for exactly one value,
and this value has to be greater than 3. These assumptions are given as
constraints in assumptions.lp.
:- #count{ S : size(S) } != 1.
:- size(S), S <= 3.
input: size/1.
output: place/3.
The two programs use different encodings of the tiling problem.
num(1..N) :- size(N).
{ place(X,Y,T) } :- num(X), num(Y), T = 1..3.
:- place(X,Y,T1), place(X,Y,T2), T1 != T2.
:- #count{ X,Y : place(X,Y,1) } != 1.
filled(X,Y) :- place(X,Y,1).
filled(X+I,Y) :- place(X,Y,2), I = 0..2.
filled(X,Y+I) :- place(X,Y,3), I = 0..2.
:- not filled(X,Y), num(X), num(Y).
:- place(X,Y,2), not num(X+I), I = 0..2.
:- place(X,Y,3), not num(Y+I), I = 0..2.
:- place(X,Y,2), place(X+I,Y,T), I = 1..2.
:- place(X,Y,3), place(X,Y+I,T), I = 1..2.
:- place(X,Y,2), place(X+I,Y-J,3), I = 1..2, J = 1..2.
:- place(X,Y,3), place(X-I,Y+J,2), I = 1..2, J = 1..2.
val(1..N) :- size(N).
{ h(X,Y) } :- val(X), val(Y), val(Y+2).
{ v(X,Y) } :- val(X), val(Y), val(X+2).
square(X,Y) :- val(X), val(Y).
covered(R,C+I) :- h(R,C), I = 0..2.
covered(R+I,C) :- v(R,C), I = 0..2.
:- square(R1,C1), square(R2,C2),
not covered(R1,C1), not covered(R2,C2), R1 != R2.
:- square(R1,C1), square(R2,C2),
not covered(R1,C1), not covered(R2,C2), C1 != C2.
:- h(R,C), h(R,C+(1..2)).
:- v(R,C), v(R+(1..2),C).
:- h(R,C), v(R-(0..2),C+(0..2)).
place(C,R,1) :- square(R,C), not covered(R,C).
place(C,R,2) :- h(R,C).
place(C,R,3) :- v(R,C).
The two programs are not externally equivalent. Running
anthem-cx tiling.1.lp tiling.2.lp tiling.ug --assumptions assumptions.lp
finds a counterexample of size 1; the witnessing input is size(6). The
reported size counts the distinct constants used in the input (here only the
constant 6), not the tiling grid size.