snuke https://blog.hatena.ne.jp/snuke/ あなたは嘘つきですかと聞かれたら「YES」と答えるブログ https://snuke.hatenablog.com/ programming パズル SAT solverで「数独」「美術館」「ひとりにしてくれ」を解きました。Githubにあげました。めっちゃ楽しかったので準急に多謝だー。（JOI春合宿で講義をしてくれた） 準備 SAT solverをインストールしましょう。僕はminisatにしました。（なんか入れるのに苦労したけど）SATを知らない人は適当に調べましょう。流れとしては、 パズルを連言標準形(CNF)の論理式にして SAT solverに投げて ビジュアライズする って感じです。 数独 多分一番簡単です。「x1,x2,...,x9 のうち、ちょうど１つだけがtrue」という式が書ければ勝ちです。これは、 x1 or x2 o… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fsnuke.hatenablog.com%2Fentry%2F2015%2F04%2F03%2F014316" title="SAT solverでパズルを解いた話 - あなたは嘘つきですかと聞かれたら「YES」と答えるブログ" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2015-04-03 01:43:16 rich https://snuke.hatenablog.com/entry/2015/04/03/014316 1.0 100%