Formal Methods

理論上は爆発するはずの難問を、なぜ現代のコンピュータは瞬時に解けるのか：SATソルバーと論理充足のアルゴリズム