MaxSAT SATの最適化問題への拡張: MaxSATソルバーの活用法

摘要

MaxSAT(Maximum satisfiability)は，SAT(Boolean satisfiability)を最適化問題に拡張したもので，SATでは解に優劣はないが，MaxSATではあり，最適解がMaxSAT解となる.MaxSATでは，問題はハード節とソフト節の集合として表される.ソフト節には重みがあり，重みは正整数で表される.重みはそのソフト節の重要性の度合いを示しており，ハード節はどのソフト節よりも重要で必ず満たさなければならない制約を表す.