文献

J-GLOBAL ID：202202224410122379   整理番号：22A1171344

ホーンシステムにおけるリードワンス切断面証明の解析【JST・京大機械翻訳】

Analyzing Read-Once Cutting Plane Proofs in Horn Systems

著者 (3件)： Wojciechowski Piotr (LDCSEE, West Virginia University, Morgantown, WV, USA) ,  Subramani K. (LDCSEE, West Virginia University, Morgantown, WV, USA) ,  Chandrasekaran R. (Computer Science and Engineering, University of Texas at Dallas, Dallas, TX, USA)
資料名： Journal of Automated Reasoning  (Journal of Automated Reasoning)
巻： 66  号： 2  ページ： 239-274  発行年： 2022年 
JST資料番号： D0269E  ISSN： 0168-7433  CODEN： JAREEW  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 本論文では,Horn制約システム(HCS)と呼ばれる整数プログラムのクラスに対する切断面証明システムの変形を研究した。簡単に言えば,線形不等式[数式:原文を参照]のシステムは,[数式:原文を参照]における各入力が集合[数式:原文を参照]に属するならば,Horn制約システムと呼ばれ,さらに,列当たり1つの正の入力がある。著者らの焦点は,切断面証明システムの変形におけるそのようなプログラムの充足可能性の証明,すなわち, re中の導出である。HornシステムはHorn公式を一般化し,すなわち,CNF公式は,1つ目当たり1つの正のリッターで,CNF公式を一般化する。Horn clausal公式を書き換えるHornシステムは,Horn Clausal制約システム(HClCS)と呼ばれる。切削面計算(CP)は,命題CNF公式と整数プログラムの不満足性を決定するよく知られた計算である。通常,CPは付加規則(ADD)と分割規則(DIV)から成る。付加規則のみ(CP-ADD)による切断面計算は,[数式:原文を参照]の制約を必要としないことを示した。また,切断面証明システムにおけるHorn Clausal制約システムにおける読取り返答の存在を研究した。読影再fuは不完全であることを示した。HCSのADD規則のみを用いた読取り返答を見つける問題は,HCSの右手側が集合[数式:原文を参照]に属する場合でもNP困難であることを示した。さらに,HClCSのADD規則のみを用いた読取り返答を見つける問題はNP困難であることを示した。次に,ADDとDIVルールの両方を使用するとき,これらの問題はハードのままであることを示した。次に,その右手側が集合[数式:原文を参照]に属するHCSの最短読影発見を見つける問題は,再fuがADD規則だけを使用するとき,NPO BP完全であり,また,再fu中がADDとDIV規則の両方を使用することができることを示す。最後に,ADD規則のみを用いて,Horn制約のシステムの読取り返答を見つけるためのパラメータ化指数時間アルゴリズムを提供した。Copyright The Author(s), under exclusive licence to Springer Nature B.V. 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  不等式 ,  *システム ,  規則 ,  ホーン ,  線形性 ,  落葉落枝 ,  命題 ,  NP困難 ,  パラメタリゼーション
準シソーラス用語： 読影 , 【Automatic Indexing@JST】

分類 (3件)： 論理代数  (JB03000H) ,  計算理論  (JB02000A) ,  人工知能  (JE08000Z)

タイトルに関連する用語 (4件)： ホーン ,  切断面 ,  証明 ,  解析