パッキング配列問題の制約モデリングとSAT符号化  [in Japanese] Constraint Modeling and SAT Encoding of the Packing Array Problem  [in Japanese]

Access this Article

Author(s)

Abstract

制約モデリングは与えられた問題を効率よく解く上で重要な役割を果たすことが知られている.近年,大規模な命題論理の充足可能性判定(SAT)問題を高速に解くことが可能なSATソルバーが実現され,制約充足問題(CSP; Constraint Satisfaction Problem)をSAT問題に符号化して,高速なSATソルバーを用いて求解するアプローチが成功を収めている.本論文では,組合せデザイン分野の一問題であるパッキング配列(<I>PA</I>)問題を例にとり,SATに基づく制約モデリングについて考察する.<I>PA</I>は別名で相互直交的な部分ラテン方陣系とも呼ばれる困難な組合せ問題であり,データベースのディスク最適配置などへの応用が知られている.まず最初に,<I>PA</I>問題を異なる観点から捉えた4つの制約モデル(CSP表現)を提案する.次に,これらの制約モデルを順序符号化法を用いてSAT問題に符号化する方法を示す.なかでも,基本・相違モデルは,与えられた<I>PA</I>のパッキング制約について,その符号化後の節数を小さく抑えられる点が特長である.最後に,組合せデザイン・ハンドブックにある<I>PA</I>問題を用いて,提案する制約モデルの比較・評価を行った.実験の結果,最適値が未知であった2問について既知の上限が最適値であることを示し,5問について新しい下限を得ることに成功した.

Constraint modeling is known to play an important role in solving problems efficiently. Remarkable improvements of SAT solvers have been made over the last decade. Such improvements encourage researchers to solve Constraint Satisfaction Problems (CSPs) by encoding them into SAT. In this paper, we study SAT-based constraint modeling of the Packing Array (<I>PA</I>) problem in Combinatorial Designs. <I>PA</I> is also called mutually orthogonal partial latin squares and has been applied to optimal disk allocation in Databases. We first present four constraint models from different viewpoints of the <I>PA</I> problem, and then present their SAT encodings based on the order encoding. Particularly, <I>basic alldiff model</I> is designed to reduce the number of clauses for the packing constraints of a given <I>PA</I>. To evaluate the efficiency of our proposed models, we carried out experiments on the <I>PA</I> problems in Handbook of Combinatorial Designs. We succeeded in proving the optimality of previously known upper bounds for two arrays and in obtaining improved lower bounds for five arrays.

Journal

  • Computer Software

    Computer Software 31(1), 1_116-1_130, 2014

    Japan Society for Software Science and Technology

Codes

Page Top