/* Symbolic Sudoku in Picat. The model solves a symbolic Sudoku puzzle using these steps - convert the symbolic version to a plain integer puzzle - solves the integer puzzle - and converts it back to symbols again Here's the problem (s1) and the solution: _ _ b _ _ e _ g i a _ e _ _ c _ _ _ _ _ _ _ _ _ f _ _ _ a _ d _ _ i _ _ _ i _ _ _ _ _ h _ _ _ d _ _ i _ a _ _ _ i _ _ _ _ _ _ _ _ _ a _ _ c _ f f h _ c _ _ d _ _ c f b h d e a g i a g e i f c b d h i d h b a g f c e g a c d e h i f b b i f g c a e h d h e d f b i g a c d c i e g f h b a e b g a h d c i f f h a c i b d e g The model has some assumptions which might not work well for some other symbolic problems, especially that it assumes that a <-> 1, b <-> 2, etc, with the conversion by ASCII +/- 96. So how would 0 be converted? To a? and then b -> 1, etc? What about other symbols such as 'A' and '1'? This program was created by Hakan Kjellerstrand, hakank@gmail.com See also my Picat page: http://www.hakank.org/picat/ */ import util. import sat. main => go. go => nolog, problem(s1,SymGrid), print_grid(SymGrid), IntGrid = conv_grid(SymGrid), sudoku(IntGrid), SymGridSol = conv_grid(IntGrid), print_grid(SymGridSol), nl, fail, nl. /* Show the intermediate integer solution as well: 1 7 5 9 6 3 2 4 8 9 4 8 2 1 7 6 3 5 7 1 3 4 5 8 9 6 2 2 9 6 7 3 1 5 8 4 8 5 4 6 2 9 7 1 3 4 3 9 5 7 6 8 2 1 5 2 7 1 8 4 3 9 6 6 8 1 3 9 2 4 5 7 */ go2 => nolog, problem(s1,SymGrid), print_grid(SymGrid), IntGrid = conv_grid(SymGrid), sudoku(IntGrid), print_grid(IntGrid), SymGridSol = conv_grid(IntGrid), print_grid(SymGridSol), nl, fail, nl. /* _ w _ _ s p _ _ x g e i a _ _ _ h r _ _ _ _ u _ _ o p _ v _ k h _ _ _ y _ n _ _ _ l s _ _ q _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ p _ d _ q _ m _ x _ w s j b _ _ _ _ _ s _ n w d _ u f v j _ k _ b _ _ _ _ _ _ q n _ _ b _ _ m l _ _ _ _ _ o d t v j _ k _ i x h v _ _ _ _ f b _ _ _ d g l a i _ _ _ _ _ _ n e _ _ _ r b _ h v _ s p u _ _ _ j m w _ _ t _ _ c _ o g _ _ q c _ e _ _ h i _ _ _ _ r _ s _ _ _ _ _ w u _ a k _ _ i _ o j y _ f _ w _ _ _ _ e c g _ q _ _ x _ _ _ _ _ _ a _ _ w _ _ _ x _ _ _ u l _ f h _ y p t x j _ o w k q _ _ _ _ _ g _ l _ _ _ _ _ v _ _ f d e _ n l y _ r _ _ w _ o _ s a _ _ _ v t _ g i _ r _ u _ _ h _ x _ _ i _ y _ _ _ j _ _ _ b _ a s _ _ _ f b a _ m _ v _ _ _ _ _ k h u p _ _ y _ _ l q _ q y _ w g n _ u a _ _ _ _ c _ _ k _ _ x _ p d e _ _ _ _ k r x _ _ _ _ e _ l _ y _ _ _ o w d h n _ _ _ _ o u _ _ _ _ _ b _ m q _ _ a g _ _ e i x _ _ _ _ r _ v o _ _ b p _ w _ _ _ j f x _ q l _ y k _ g b _ a _ _ u _ _ _ r v _ i f n _ d e p _ _ _ _ _ _ _ i _ _ _ g v _ _ j _ x _ _ _ r _ _ _ u _ _ _ _ _ l _ s j _ _ _ _ _ _ _ _ _ a _ _ _ _ _ n _ d h _ x _ k r _ _ _ _ _ _ _ y q u _ f _ _ a _ _ _ _ e l p f v _ _ _ w d o r h _ _ _ t _ _ q _ n _ _ _ _ _ _ u _ _ d _ i a g _ _ _ _ k n _ p h o _ v _ r _ _ h o _ _ _ _ _ _ e _ x c _ _ d _ _ _ i _ _ _ _ _ t k w m j s p f b x g e i a t q o h r y c d l u v n o p d v r k h u t j y b n m x g l s w i q e f a c u a e t y c r o i v k p h d l q n m f x g w s j b c h l i x s q n w d g u f v j p k a b e o r t m y q n g f b a e m l y c r s w o d t v j u k p i x h v s w u m f b c q x d g l a i k o y p h r n e t j y r b x h v d s p u n k e j m w q f t a i c l o g f j q c p e l g h i o t b y r v s n x m a k w u d a k n l i t o j y m f h w p u r d e c g s q v b x e t o d g n a k r w q s c x v i b u l j f h m y p t x j m o w k q s c u a p g b l e i d y h v n r f d e p n l y j r f b w m o h s a x c q v t u g i k r v u k c h p x d l i q y n e t j o g f b m a s w s g f b a i m e v o t x d r k h u p n w y j c l q i q y h w g n t u a l j v f c b m k s r x o p d e j m s p k r x f c q a e t l g y i b u o w d h n v l y h o u j s w n k b d m q p c a g v t e i x f r n d r e v o t i b p s w u c h j f x m q l g y k a g b x a t l u y m h r v k i f n w d e p j s q c o w c i q f d g v a e j n x o y s r l h k u t b p m m l t s j q c p k f v o g e a u y w r b n x d h i x i k r n m v h j s p y q u w f g t a d c b o e l p f v y e b w d o r h l i s t x c q k n m a j g u b u c w d x i a g t m f j k n e p h o l v y r q s h o a g q u y l e n x c r b d m v j i s p f k w t Proved unique solution by SAT in 1.2s. */ go3 => nolog, problem(s19,Sym), print_grid(Sym), sudoku(Sym,Sol), print_grid(Sol), fail, nl. % Wrapper for converting Sym <-> Int % Assumption: the Grid must contain some nonvars. conv_grid(Grid) = SymGrid, is_int_grid(Grid) => SymGrid = int_grid_to_sym(Grid). conv_grid(Grid) = sym_grid_to_int(Grid). % Convert between Int <-> Sym grids int_grid_to_sym(IntGrid) = SymGrid => N = IntGrid.len, SymGrid = new_array(N,N).array_matrix_to_list_matrix, foreach(I in 1..N) foreach(J in 1..N) if nonvar(IntGrid[I,J]) then SymGrid[I,J] = int_to_sym(IntGrid[I,J]) end end end. sym_grid_to_int(SymGrid) = IntGrid => N = SymGrid.len, IntGrid = new_array(N,N).array_matrix_to_list_matrix, foreach(I in 1..N) foreach(J in 1..N) if nonvar(SymGrid[I,J]) then IntGrid[I,J] = sym_to_int(SymGrid[I,J]) end end end. % Check for the type of grid: integer (or symbolic). % We assume that at least some of the nonvars is % either ints or syms is_int_grid(Grid) => N = Grid.len, Vs = [V : I in 1..N, J in 1..N, V = Grid[I,J], nonvar(V)], integer(Vs[1]). % Print the grid print_grid(Grid) => N = Grid.len, foreach(I in 1..N) foreach(J in 1..N) if var(Grid[I,J]) then printf("_ ") else printf("%-2w ", Grid[I,J]) end end, nl end, nl. % Convert 1->a, 2-> b, ... int_to_sym(Int) = chr(Int+96). % Convert a -> 1, b -> 2, ... sym_to_int(Sym) = ord(Sym)-96. % % Standard CP Sudoku model % sudoku(Board), is_int_grid(Board) => N = Board.len, N2 = ceiling(sqrt(N)), Vars = Board.vars(), Vars :: 1..N, foreach(Row in Board) all_different(Row) end, foreach(Column in transpose(Board)) all_different(Column) end, foreach(I in 1..N2..N, J in 1..N2..N) all_different([Board[I+K,J+L] : K in 0..N2-1, L in 0..N2-1]) end, solve($[ffd,down], Vars). % Solve a Symbolic Sudoku sudoku(Grid,Solution) => IntGrid = conv_grid(Grid), sudoku(IntGrid), Solution = conv_grid(IntGrid). % % Data % % % This is problem p1 from sudoku.pi % problem(s1,Data) => Data = [[_, _, b, _, _, e, _, g, i], [a, _, e, _, _, c, _, _, _], [_, _, _, _, _, _, f, _, _], [_, a, _, d, _, _, i, _, _], [_, i, _, _, _, _, _, h, _], [_, _, d, _, _, i, _, a, _], [_, _, i, _, _, _, _, _, _], [_, _, _, a, _, _, c, _, f], [f, h, _, c, _, _, d, _, _]]. % % This problem 19 from Gecode's sudoku.cpp % http://www.gecode.org/gecode-doc-latest/sudoku_8cpp-source.html % It's problem 19 in sudoku.pi % problem(s19,Data) => Data = [[_, w, _, _, s, p, _, _, x, g, e, i, a, _, _, _, h, r, _, _, _, _, u, _, _], [o, p, _, v, _, k, h, _, _, _, y, _, n, _, _, _, l, s, _, _, q, _, _, _, _], [_, _, _, _, _, _, _, _, _, _, _, p, _, d, _, q, _, m, _, x, _, w, s, j, b], [_, _, _, _, _, s, _, n, w, d, _, u, f, v, j, _, k, _, b, _, _, _, _, _, _], [q, n, _, _, b, _, _, m, l, _, _, _, _, _, o, d, t, v, j, _, k, _, i, x, h], [v, _, _, _, _, f, b, _, _, _, d, g, l, a, i, _, _, _, _, _, _, n, e, _, _], [_, r, b, _, h, v, _, s, p, u, _, _, _, j, m, w, _, _, t, _, _, c, _, o, g], [_, _, q, c, _, e, _, _, h, i, _, _, _, _, r, _, s, _, _, _, _, _, w, u, _], [a, k, _, _, i, _, o, j, y, _, f, _, w, _, _, _, _, e, c, g, _, q, _, _, x], [_, _, _, _, _, _, a, _, _, w, _, _, _, x, _, _, _, u, l, _, f, h, _, y, p], [t, x, j, _, o, w, k, q, _, _, _, _, _, g, _, l, _, _, _, _, _, v, _, _, f], [d, e, _, n, l, y, _, r, _, _, w, _, o, _, s, a, _, _, _, v, t, _, g, i, _], [r, _, u, _, _, h, _, x, _, _, i, _, y, _, _, _, j, _, _, _, b, _, a, s, _], [_, _, f, b, a, _, m, _, v, _, _, _, _, _, k, h, u, p, _, _, y, _, _, l, q], [_, q, y, _, w, g, n, _, u, a, _, _, _, _, c, _, _, k, _, _, x, _, p, d, e], [_, _, _, _, k, r, x, _, _, _, _, e, _, l, _, y, _, _, _, o, w, d, h, n, _], [_, _, _, o, u, _, _, _, _, _, b, _, m, q, _, _, a, g, _, _, e, i, x, _, _], [_, _, r, _, v, o, _, _, b, p, _, w, _, _, _, j, f, x, _, q, l, _, y, k, _], [g, b, _, a, _, _, u, _, _, _, r, v, _, i, f, n, _, d, e, p, _, _, _, _, _], [_, _, i, _, _, _, g, v, _, _, j, _, x, _, _, _, r, _, _, _, u, _, _, _, _], [_, l, _, s, j, _, _, _, _, _, _, _, _, _, a, _, _, _, _, _, n, _, d, h, _], [x, _, k, r, _, _, _, _, _, _, _, y, q, u, _, f, _, _, a, _, _, _, _, e, l], [p, f, v, _, _, _, w, d, o, r, h, _, _, _, t, _, _, q, _, n, _, _, _, _, _], [_, u, _, _, d, _, i, a, g, _, _, _, _, k, n, _, p, h, o, _, v, _, r, _, _], [h, o, _, _, _, _, _, _, e, _, x, c, _, _, d, _, _, _, i, _, _, _, _, _, t]].