極小モデル生成とMaxSATソルバーについて

DOI

説明

<p>モデル生成法とDPLL法の２つの証明手法の特徴を踏まえて、各手法による極小モデル生成 の実現法を紹介する。１階のモデル生成器MGTPを命題に特化したMiniMGとDPLL型SATソルバーMiniSATの性能比較を行う。制約充足問題は基数制約を付加してSAT問題に変換して解くことができる。代表的な基数制約の符号化方式Totalizerの改良版を提示し、MaxSAT問題を対象にその性能評価を行う。</p>

収録刊行物

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

  • CRID
    1390282763023113856
  • NII論文ID
    130007424369
  • DOI
    10.11517/pjsai.jsai2014.0_1d4os11a1
  • 本文言語コード
    ja
  • データソース種別
    • JaLC
    • CiNii Articles
  • 抄録ライセンスフラグ
    使用不可

問題の指摘

ページトップへ