抄録/ポイント:
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
本論文では,擬似ブール (Pseudo-Boolean; PB)制約の集合を命題論理式の充足可能性判定 (SAT)問題へ符号化する新しい手法として,ブール基数 (Boolean Cardinality; BC)制約を経由する方法を提案する.提案手法は,次の3つの特徴を持つ. 1つ目は,SATソルバーの単位伝播により一般化アーク整合性の維持が可能な点である. 2つ目は,同じ解を持つ同値なPB制約であれば係数や右辺の値が異なっても,同一の中間表現およびSAT問題に符号化可能な点である. 3つ目は,項数に対して係数の種類が少ないPB制約に対しては,中間表現が簡潔になり少ない節数でSAT符号化可能な点である.このようなPB制約は,国際PBソルバー競技会のベンチマーク問題にも頻出している.計算機実験では,代表的な既存手法で一般化アーク整合性維持が可能なBDD法,およびそれより弱い整合性検査が可能なSorter法と符号化後の節数と求解性能を比較した.結果として,異なる係数の種類が10%以下であるようなPB制約について,提案手法が節数と求解性能に関して比較した2手法よりも良いことを確認した.(著者抄録)