Clingo LP for Sudoku -- first pass, not yet satisfiable form

role(robot).

base(cell(I,J,K,L,R)) :- index(I), index(J), index(K), index(L), filler(R).

input(robot,mark(I,J,K,L,R)) :- index(I), index(J), index(K), index(L), digit(R).

true(cell(1,1,1,1,b),1).

true(cell(1,1,1,2,b),1).

true(cell(1,1,1,3,b),1).

true(cell(1,1,2,1,b),1).

true(cell(1,1,2,2,b),1).

true(cell(1,1,2,3,3),1).

true(cell(1,1,3,1,b),1).

true(cell(1,1,3,2,8),1).

true(cell(1,1,3,3,b),1).

true(cell(1,2,1,1,b),1).

true(cell(1,2,1,2,7),1).

true(cell(1,2,1,3,5),1).

true(cell(1,2,2,1,b),1).

true(cell(1,2,2,2,b),1).

true(cell(1,2,2,3,b),1).

true(cell(1,2,3,1,6),1).

true(cell(1,2,3,2,b),1).

true(cell(1,2,3,3,b),1).

true(cell(1,3,1,1,6),1).

true(cell(1,3,1,2,3),1).

true(cell(1,3,1,3,b),1).

true(cell(1,3,2,1,b),1).

true(cell(1,3,2,2,b),1).

true(cell(1,3,2,3,b),1).

true(cell(1,3,3,1,b),1).

true(cell(1,3,3,2,b),1).

true(cell(1,3,3,3,2),1).

true(cell(2,1,1,1,2),1).

true(cell(2,1,1,2,9),1).

true(cell(2,1,1,3,b),1).

true(cell(2,1,2,1,b),1).

true(cell(2,1,2,2,b),1).

true(cell(2,1,2,3,b),1).

true(cell(2,1,3,1,3),1).

true(cell(2,1,3,2,b),1).

true(cell(2,1,3,3,b),1).

true(cell(2,2,1,1,b),1).

true(cell(2,2,1,2,b),1).

true(cell(2,2,1,3,b),1).

true(cell(2,2,2,1,2),1).

true(cell(2,2,2,2,b),1).

true(cell(2,2,2,3,6),1).

true(cell(2,2,3,1,b),1).

true(cell(2,2,3,2,b),1).

true(cell(2,2,3,3,b),1).

true(cell(2,3,1,1,b),1).

true(cell(2,3,1,2,b),1).

true(cell(2,3,1,3,3),1).

true(cell(2,3,2,1,b),1).

true(cell(2,3,2,2,b),1).

true(cell(2,3,2,3,b),1).

true(cell(2,3,3,1,b),1).

true(cell(2,3,3,2,7),1).

true(cell(2,3,3,3,1),1).

true(cell(3,1,1,1,9),1).

true(cell(3,1,1,2,b),1).

true(cell(3,1,1,3,b),1).

true(cell(3,1,2,1,b),1).

true(cell(3,1,2,2,b),1).

true(cell(3,1,2,3,b),1).

true(cell(3,1,3,1,b),1).

true(cell(3,1,3,2,2),1).

true(cell(3,1,3,3,8),1).

true(cell(3,2,1,1,b),1).

true(cell(3,2,1,2,b),1).

true(cell(3,2,1,3,4),1).

true(cell(3,2,2,1,b),1).

true(cell(3,2,2,2,b),1).

true(cell(3,2,2,3,b),1).

true(cell(3,2,3,1,5),1).

true(cell(3,2,3,2,1),1).

true(cell(3,2,3,3,b),1).

true(cell(3,3,1,1,b),1).

true(cell(3,3,1,2,5),1).

true(cell(3,3,1,3,b),1).

true(cell(3,3,2,1,1),1).

true(cell(3,3,2,2,b),1).

true(cell(3,3,2,3,b),1).

true(cell(3,3,3,1,b),1).

true(cell(3,3,3,2,b),1).

true(cell(3,3,3,3,b),1).

legal(robot,mark(I,J,K,L,X),T) :- time(T), true(cell(I,J,K,L,b),T), digit(X), not row(I,K,X), not col(J,L,X), not square(I,J,X).

row(I,K,X) :- time(T), true(cell(I,1,K,1,X),T).

row(I,K,X) :- time(T), true(cell(I,1,K,2,X),T).

row(I,K,X) :- time(T), true(cell(I,1,K,3,X),T).

row(I,K,X) :- time(T), true(cell(I,2,K,1,X),T).

row(I,K,X) :- time(T), true(cell(I,2,K,2,X),T).

row(I,K,X) :- time(T), true(cell(I,2,K,3,X),T).

row(I,K,X) :- time(T), true(cell(I,3,K,1,X),T).

row(I,K,X) :- time(T), true(cell(I,3,K,2,X),T).

row(I,K,X) :- time(T), true(cell(I,3,K,3,X),T).

col(J,L,X) :- time(T), true(cell(1,J,1,L,X),T).

col(J,L,X) :- time(T), true(cell(1,J,2,L,X),T).

col(J,L,X) :- time(T), true(cell(1,J,3,L,X),T).

col(J,L,X) :- time(T), true(cell(2,J,1,L,X),T).

col(J,L,X) :- time(T), true(cell(2,J,2,L,X),T).

col(J,L,X) :- time(T), true(cell(2,J,3,L,X),T).

col(J,L,X) :- time(T), true(cell(3,J,1,L,X),T).

col(J,L,X) :- time(T), true(cell(3,J,2,L,X),T).

col(J,L,X) :- time(T), true(cell(3,J,3,L,X),T).

square(I,J,X) :- time(T), true(cell(I,J,1,1,X),T).

square(I,J,X) :- time(T), true(cell(I,J,1,2,X),T).

square(I,J,X) :- time(T), true(cell(I,J,1,3,X),T).

square(I,J,X) :- time(T), true(cell(I,J,2,1,X),T).

square(I,J,X) :- time(T), true(cell(I,J,2,2,X),T).

square(I,J,X) :- time(T), true(cell(I,J,2,3,X),T).

square(I,J,X) :- time(T), true(cell(I,J,3,1,X),T).

square(I,J,X) :- time(T), true(cell(I,J,3,2,X),T).

square(I,J,X) :- time(T), true(cell(I,J,3,3,X),T).

true(cell(I,J,K,L,X),T+1) :- time(T), does(ROLE,mark(I,J,K,L,X),T).

true(cell(I,J,K,L,X),T+1) :- time(T), true(cell(I,J,K,L,X),T), does(ROLE,mark(S,T,U,V,Y),T), S!=I.

true(cell(I,J,K,L,X),T+1) :- time(T), true(cell(I,J,K,L,X),T), does(ROLE,mark(S,T,U,V,Y),T), T!=J.

true(cell(I,J,K,L,X),T+1) :- time(T), true(cell(I,J,K,L,X),T), does(ROLE,mark(S,T,U,V,Y),T), U!=K.

true(cell(I,J,K,L,X),T+1) :- time(T), true(cell(I,J,K,L,X),T), does(ROLE,mark(S,T,U,V,Y),T), V!=L.

goal(robot,100,T) :- time(T), not open(T).

goal(robot,0,T) :- time(T), open(T).

terminal(T) :- time(T), not playable(T).

filler(X) :- time(T), digit(X).

filler(b).

open(T) :- time(T), true(cell(I,J,K,L,b),T).

playable(T) :- time(T), legal(robot,mark(I,J,K,L,X),T).

index(1).

index(2).

index(3).

digit(1).

digit(2).

digit(3).

digit(4).

digit(5).

digit(6).

digit(7).

digit(8).

digit(9).

:- does(R,M,T), not legal(R,M,T).

:- 0{ terminal(T) : time(T) }0.

:- terminal(T), role(robot).

time(1..58).

1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T), 1 <= T, T <= 57.

:- not goal(robot,100,58).