| 研究実績の概要 |
(1) 対称性制約に関して：大規模組合せ問題における主たる事例研究として、ラムゼー数に関する問題についての研究を行った。副対角線対称性や市松模様型対称性、及び各種対称性の複合適用の有効性を確認した。ソルバーSCSat3の改良を進め、幾つかの新しい結果を得た。中でもラムゼーグラフRG(4,6,34)について、副対角線対称性を完全に満たす新たな結果が得られた。
(2) 基数制約に関して：重み付きMaxSAT問題に不可欠な重み付き基数制約のCNF符号化について、Totalizer方式やModulo法等を基本とした幾つかの方式を設計・実装し、比較評価を行った。それらをQMaxSATソルバーに組み込んでベンチマーク問題を解いた結果、符号化後のCNFのサイズを格段に抑えられるなど、極めて効果的であることを確認した。
(3) MaxSAT応用に関して：AES暗号鍵に関するMaxSAT応用の研究成果をまとめた。また、帰納論理プログラミングをMaxSATによって模擬実行する手法の実証実験と改善を行った。さらに、ラムゼー数に関する問題に関して、対称性制約を最大限に充足するラムゼーグラフの探索にMaxSATソルバーが有効に利用できることを確認した。具体的には、ラムゼーグラフRG(5,5,42)を含め、重要なラムゼーグラフの多くがストライプ制約や副対角線制約を良く充足することが分かった。
(4) 以上に加え、基盤技術として必須のSATソルバーの高速化に関して、純リテラル削除の導入について研究を行い、ベンチマーク問題等において効果を確認した。
|
