2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み

摘要

論理式の充足可能性判定問題（SAT問題）を解くSATソルバの高速化の一手法として，馬野らは2010年にCNFへの基本対称節の導入を提案した．彼らのSATソルバは，節中の真リテラルと偽リテラルの個数をカウンタに保持する方法による実現であるためバックトラックが重いという欠点がある．そこで，Minisatに代表される現在主流のソルバが採用する節あたり二つのリテラルを監視する方法（2リテラル監視法）に基づく実現が可能であれば，バックトラックが軽くなるため更なる高速化が期待できる．しかしながら，基本対称節の性質から二つのリテラルのみの監視では十分でなく，そのままでは高速化が期待できない．本論文では，通常の節（OR節）は二つのリテラルを監視し，基本対称節については節中のリテラルをすべて監視する方法を提案する．実際にこれをMinisatに組み込むことで，本手法の有効性を評価する．