Sudoku in Clingo

Question

I am trying to write a sudoku in clingo to learn the syntax a bit more. The part that I am satisfied with correctly represents the column/row constraints:

subgrid_size(3).
number(1..S*S) :- subgrid_size(S).
sudoku(X,Y,N) :- initial(X,Y,N).
1{sudoku(X,Y,N): number(N)}1 :- number(X), number(Y). %each coordinate has to have a unique N
1{sudoku(X,Y,N): number(X)}1 :- number(N), number(Y). %a number can only appear once per row
1{sudoku(X,Y,N): number(Y)}1 :- number(X), number(N). %a number can only appear once per col

Then I had tried to do something similar to enforce the subgrid constraint:

1{sudoku(X,Y,N): subgrid((X-1/S)*S+(Y-1)/S) }1 :- number(N),number(X), number(Y),subgrid_size(S).

This did not work, after a long time looking for solutions I found this(which works):

subgrid(X,Y,((X-1)/S)*S+(Y-1)/S):- number(X), number(Y), subgrid_size(S).
:- subgrid(X1,Y1,G), subgrid(X2,Y2,G),sudoku(X1,Y1,N), sudoku(X2,Y2,N), X1!=X2, Y1!=Y2.

Is there anyway to adapt the 1{...}1:- rule1..ruleN. line for the subgrid constraint so that it works?

Answer 1

Interesting approach! The immediate problem is that subgrid/1 in the choice rule is not defined anywhere. I get the error message:

info: atom does not occur in any rule head: subgrid(#Arith0)

Changing the choice rule to use subgrid/3 ...

1{sudoku(X,Y,N): subgrid(X, Y, (X-1/S)*S+(Y-1)/S ) }1 :-
    number(N), number(X), number(Y), subgrid_size(S).

... and including your subgrid/3 predicate ... now doesn't return an error, but returns unsatisfiable.

Here's what worked for me:

First I changed subgrid/3 slightly -- adding +1 to the third argument, so that subgrid labels were 1-9, instead of 0-8, ie now they are numbers:

subgrid(X, Y, (((X-1)/S)*S+(Y-1)/S)+1):-
    number(X),
    number(Y),
    subgrid_size(S).

Second, I used this choice rule:

1 { sudoku(X,Y,N):
    number(X), number(Y),
    subgrid(X,Y,M)
  } 1 :-
    number(N),
    number(M).

ie for every possible (N, M) combination, there is one sudoku(X,Y,N), where (X,Y) is in subgrid M.

Does that work for you?