ブール基数制約を経由した擬似ブール制約のSAT符号化手法  [in Japanese] A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints  [in Japanese]

Access this Article

Author(s)

Abstract

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

In this paper, we propose a new encoding method for a set of PB (Pseudo-Boolean) constraints into propositional satisfiability (SAT) problems, in which Boolean Cardinality (BC) constraints are used as an intermediate form. The proposed method has the following three features. First, it can maintain general arc consistency by unit propagation of a SAT solver. Second, it can encode equivalent PB constraints with the same solutions—even their coefficients and right hand side value are different—into the same intermediate form and SAT instance. Third, for PB constraints whose number of kinds of coefficients is relatively small compared with the number of terms, the intermediate form becomes simpler and they can be encoded with a small number of clauses. Such PB constraints often appear in international PB solver competition benchmarks. In experiments, we compared the proposed encoding method with existing methods, BDD and Sorter. The former maintains general arc consistency by unit propagation, while the later maintains consistency checking that is weaker than general arc consistency. As the result, for PB constraints in which the number of different coefficients is not more than 10%, we confirmed that the proposed method is better than those two methods in terms of the number of encoded clauses and the efficiency in solver performance.

Journal

  • Computer Software

    Computer Software 35(3), 3_65-3_78, 2018

    Japan Society for Software Science and Technology

Codes

  • NII Article ID (NAID)
    130007487601
  • Text Lang
    JPN
  • ISSN
    0289-6540
  • Data Source
    J-STAGE 
Page Top