OBDDを用いたnon-exhaustiveなSAT Solver(セッション4)
スポンサーリンク
概要
- 論文の詳細を見る
本稿ではOBDDを用いたnon-exhaustiveな、すなわち全解探索でないSAT Solverの原理を提案し、DIMACS等のベンチマークの結果を示す。また、探索順序を自然な線形順序を用いた場合、最悪の場合指数オーダ領域が必要となることを示す。
- 一般社団法人情報処理学会の論文
- 2006-01-20
本稿ではOBDDを用いたnon-exhaustiveな、すなわち全解探索でないSAT Solverの原理を提案し、DIMACS等のベンチマークの結果を示す。また、探索順序を自然な線形順序を用いた場合、最悪の場合指数オーダ領域が必要となることを示す。