この本は、論理式の充足性判定を超高速に行うSATソルバーの能力だけを使って様々なプログラミングを行う本です。
SATソルバーとはそもそも何なのかの紹介からスタートして、最終的には非決定性BrainfuckプログラムをSATの問題に帰着することで、コンピュータサイエンスで極めて重要な概念「NP完全」の証明の実演を行うことを目指します。
「論理式だけで何でも問題を表す」、と聞くと単なる曲芸プログラミングだと思われがちですが、その中には様々なプログラミングテクニックと情報科学の実例が詰まっています。
あなたが、SATソルバーライフをきっと楽しめますように。
ネット上から読む時は、githubよりもGitBookの方が読みやすいよ
⇒ https://ledyba.gitbooks.io/programming-on-sat/content/