SAT

Microsoft Researchが作ったZ3というツールがあります。これを使うと魔方陣や数独などを簡単に解くことができます。簡単にと言っても使い方は難しいです。今回はPythonでZ3を使って覆面算を解いてみます。Macで試しました。