文献

J-GLOBAL ID：201802249527310169   整理番号：18A1841902

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

A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints

著者 (4件)： 南雄之 (神戸大学大学院システム情報学研究科) ,  宋剛秀 (神戸大学情報基盤センター) ,  番原睦則 (神戸大学情報基盤センター) ,  田村直之 (神戸大学情報基盤センター)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 35  号： 3  ページ： 3_65-3_78(J-STAGE)  発行年： 2018年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

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

シソーラス用語： *Boole代数 ,  *充足可能性問題 ,  *符号化 ,  伝搬 ,  データ表現 ,  評価試験 ,  ベンチマーク ,  性能評価
準シソーラス用語： 情報伝搬 ,  中間表現【計算機プログラム】

分類 (3件)： システム・制御理論一般  (IA02010H) ,  論理代数  (JB03000H) ,  符号理論  (ND02030R)

タイトルに関連する用語 (5件)： 基数 ,  制約 ,  擬似 ,  SAT符号化 ,  手法