|
本年度は初年度なので、サーベイを中心に行った。来年度に本格的な実装を行う予定である。
現在のSAT solverには様々な知識が盛り込まれている。知識をルールとしてプログラムに導入するのであるが、ルールをたくさん盛り込めば、当然探索効率が良くなる傾向がある。しかし一方で、ルールの適用にかかるオーバヘッドがかさみ、単位時間辺りの探索速度は低下し、トータルとして見た解答時間は遅くなることがある。これが計算機で実装した時の大きなジレンマである。
つまり、どのルールの組み合わせを導入するかによって、solverとしての性能は大きく変化する。また、探索の前に前処理を行うのが一般的であるが、前処理によっても大きく性能が著しく変化する。前処理の方法によっては、その後の探索エンジンの機能を大きく引き出すことができることもある。つまり探索における基本ルールの組み合わせだけでなく、前処理の方法との組み合わせや、前処理と探索エンジンとの間における力の入れ方のバランスが非常に難しい。
本年度の試験的に実装では、問題に対する得手不得手が大きく、まだ実用に耐えない。探索の基本ルールの組み合わせや、前処理の方法との組み合わせがうまく噛み合っていない。来年度は現在定評のあるChaffやMiniSATなどのsolverの前処理や、基本ルールを部分的に盛り込みつつ、問題に対する得手不得手の少ない、安定した性能を発揮できるsolverの開発を行う予定である。
|
