90006799

open access

Version of Record

ブール基数制約を経由した擬似ブール制約のSAT符号化手法

Japanese (日本語)

コンピュータ ソフトウェア

35(3)

65-78

日本ソフトウェア科学会

2018

2020-02-27

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.

学術雑誌論文

ここに掲載した著作物の利用に関する注意 本著作物の著作権は日本ソフトウェア科学会に帰属します．本著作物は著作権者である日本ソフトウェア科学会の許可のもとに掲載するものです．ご利用に当たっては「著作権法」に従うことをお願いいたします．