基数制約に基づくMaxSATソルバーにおける変数アクティビティ調整とその評価

情報処理学会

この論文をさがす

抄録

MaxSAT問題とは、与えられた論理式に対し、充足可能な節の最大数を求める問題の事である。MaxSAT問題は人工知能やスケジューリングなど様々な分野で応用されており、問題を速く解く事は重要である。現在わが研究室ではQMaxSATを開発しており、競技会において良い結果を残している。本論文では、QMaxSATのCNF符号化方式を改良し、それに対して評価実験及び考察を行う。現在QMaxSATではBailleuxによる符号化を用いている。この符号化の際に生じる中間変数のアクティビティを変化させ、それに伴う性能の変化を評価する。現在のものとは異なる手法の符号化を用いることにより、性能の向上を図る。

収録刊行物

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ