数独はSATに限る、わけではないようだけれど

充足可能問題を解くsolverのminisatを利用して、数理パズルの一種である数独を解いてみようというtutorialを見つけた。なるほど。
論理式の乗法標準形というのを見て、たまたま今図書館から借りてきて眺めているゲーム作成本に出ていた、マップチップを思い出した。