情報処理学会 第76回全国大会講演要旨

命題論理式の充足性を解くSATソルバは近年の高速化により、様々な応用がなされている。代表的な高速SATソルバは手続き言語で記述されている。一方、実行速度の問題はあるが関数型言語が人工知能やWebサービスの記述への応用も含めて新たなプログラミングの手法として注目されている。そこで既存のSATソルバの高速化技法に加え、GCをできるだけ起こさないような実装を取ることで妥当な範囲での速度低下に抑えることを目的として、Haskell言語によるSATソルバを実装した。その実装方針を説明し、評価を行う。