首页    期刊浏览 2025年01月08日 星期三
登录注册

文章基本信息

  • 标题:ブール基数制約を経由した擬似ブール制約のSAT符号化手法
  • 作者:南 雄之 ; 宋 剛秀 ; 番原 睦則
  • 期刊名称:コンピュータ ソフトウェア
  • 印刷版ISSN:0289-6540
  • 出版年度:2018
  • 卷号:35
  • 期号:3
  • 页码:3_65-3_78
  • DOI:10.11309/jssst.35.3_65
  • 语种:Japanese
  • 出版社:Japan Society for Software Science and Technology
  • 摘要:

    本論文では,擬似ブール (Pseudo-Boolean; PB)制約の集合を命題論理式の充足可能性判定 (SAT)問題へ符号化する新しい手法として,ブール基数 (Boolean Cardinality; BC)制約を経由する方法を提案する.提案手法は,次の3つの特徴を持つ. 1つ目は,SATソルバーの単位伝播により一般化アーク整合性の維持が可能な点である. 2つ目は,同じ解を持つ同値なPB制約であれば係数や右辺の値が異なっても,同一の中間表現およびSAT問題に符号化可能な点である. 3つ目は,項数に対して係数の種類が少ないPB制約に対しては,中間表現が簡潔になり少ない節数でSAT符号化可能な点である.このようなPB制約は,国際PBソルバー競技会のベンチマーク問題にも頻出している.計算機実験では,代表的な既存手法で一般化アーク整合性維持が可能なBDD法,およびそれより弱い整合性検査が可能なSorter法と符号化後の節数と求解性能を比較した.結果として,異なる係数の種類が10%以下であるようなPB制約について,提案手法が節数と求解性能に関して比較した2手法よりも良いことを確認した.

Loading...
联系我们|关于我们|网站声明
国家哲学社会科学文献中心版权所有