高中的时候才知道数独，还买了本小册子，至今没填完。
用SMT求解器解数独简直大才小用，而且不用费一点脑力就能用SMT来描述一个数独问题。数独里的每一个格子可以直接对应到SMT里的一个变量，然后根据数独的规则向这些变量加上约束。对于已知的格子，直接让对应变量等于那个值。
sudoku game = do
-- 81个变量
vs :: [SWord8] <- mkExistVars 81
-- 已知的值
zipWithM_ setVar game vs
-- 每个变量 1 <= x <= ⑨
mapM_ (\x -> constrain $ x .>= 1 &&& x .<= 9) vs
-- 行/列/九个小方格。这一团地图是神马？(╯°口°)╯(┴—┴)
mapM_ (mapM_ (allDiff . map (vs !!)))
[ map (take 9 . iterate (+ 9)) [0 .. 8]
, map (take 9 . iterate (+ 1)) (take 9 [0, 9 ..])
, map (concat . take 3 . iterate (map (+ 9)) . take 3 . iterate (+ 1))
[0,3,6,27,30,33,54,57,60]
]
-- 也不知道是谁规定的，最后都要返回一个SB的true ╮(￣▽￣)╭
return (true :: SBool)
where
setVar 0 _ = return ()
setVar x v = constrain $ v .== fromIntegral x
allDiff [] = return ()
allDiff (x:xs) = mapM_ (constrain . (x ./=)) xs >> allDiff xs要用1秒左右才能解出来传说中最难的数独，不过不伤脑能有这个速度也算不错了。
这种约束简单而且能直接和SMT变量对应的问题都很好解。
其实更有趣的是生成数独问题。