情報処理学会 第74回全国大会講演要旨

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