首页    期刊浏览 2024年11月25日 星期一
登录注册

文章基本信息

  • 标题:位取り記数法に基づく整数有限領域上の制約充足問題のコンパクトかつ効率的なSAT符号化
  • 本地全文:下载
  • 作者:丹生 智也 ; 田村 直之 ; 番原 睦則
  • 期刊名称:コンピュータ ソフトウェア
  • 印刷版ISSN:0289-6540
  • 出版年度:2013
  • 卷号:30
  • 期号:1
  • 页码:1_211-1_230
  • DOI:10.11309/jssst.30.1_211
  • 出版社:Japan Society for Software Science and Technology
  • 摘要:

    本論文では,整数有限領域上の制約充足問題に現れる算術的な制約をSATに符号化する新しい方法としてコンパクト順序符号化を提案する.コンパクト順序符号化の基本アイデアは,各整数変数を位取り基数法(すなわちB進法)で表現することと,各桁を順序符号化を用いてSATに符号化することである(B ≥ 2,Bを基底と呼ぶ).コンパクト順序符号化はB = 2の場合には対数符号化と等価であり,Bが整数変数のドメインサイズ以上の時には順序符号化と等価である.その意味で,コンパクト順序符号化は両方の符号化の一般化であるとみなせる.また,典型的な制約充足問題であるオープンショップ・スケジューリング問題とグラフ彩色問題とを用いた比較実験により,コンパクト順序符号化が小規模(変数のドメインサイズが102未満)から大規模(変数のドメインサイズが107程度)までの広い範囲の問題に適用可能であり,順序符号化および対数符号化,また既存の制約ソルバーよりも高性能であることが確認できた.今後,基底Bの選び方に関する網羅的な実験が必要と考えられるが,現時点でコンパクト順序符号化は,様々な規模の制約充足問題に適用可能かつ効率的なSAT符号化の1つであるといえる.

国家哲学社会科学文献中心版权所有