証明方程式の線形時間解法アルゴリズム

• Item type: SIG Technical Reports(1)
• 公開日: 1992-07-17
• タイトル: 証明方程式の線形時間解法アルゴリズム
• タイトル / 言語: en
• タイトル: Linear Time Algorithm for solving the Proving Equation
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: (株)東芝総合研究所
• 著者所属(英): en
• 著者所属(英): Information Systems Laboratory, Toshiba Research and Development Center.
• 著者名: 山崎, 勇
• 著者名(英): Isamu, Yamazaki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 命題論理における節集合Sの充足可能性問題は、Sが一般Horn条件を満たすならば、同次証明方程式に非負の整数解があるかどうかという問題と等価である（代数的証明原理）[1]。一般Horn条件とは、Sの充足可能性問題と等価な0，1整数計画問題の0，1制約を実数にまで緩和した問題によって充足可能性が判定できる、という条件と考えてよい。ところでこの緩和問題に実数の解があれば区間[0，1]での解もある、という補題が導ける。従ってこの緩和問題は[0，1]の範囲の解だけを探せばよく、リテラル数に線形の時間で解ける。この解法から、（同次）証明方程式の線形時間解法が導ける。一方リテラル数の線形時間で充足可能性が判定できる節集合のクラスについて、Chandruらは(dd) extended Horn setsなるクラスを導いているが[4]、このクラスはさらに拡大できることを示した。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Let S denote a set of clauses of propositional logic, and m the total number of literals in S. According to the Algebraic Proving Principle, a generalized Horn set S is unsatisfiable if and only if the linear Homogeneous Proving Equation derived from S has a nonnegative integral solution. A generalized Horn set is an S that is satisfiable if there exists an unconstrained real solution to the 0,1 integer programming problem equivalent to the original satisfiability problem. The author proved the lemma that if this relaxed problem has unconstrained real solution, then it has also [0,1] solution. Hence this relaxed problem is solvable in O(m) time. This leads us to an O(m) time algorithm for solving the (Homogeneous) Proving Equation. It is also shown that there is a super class to the class of (hidden) extended Horn sets given by Chandru and Hooker, whose satisfiability is still solvable in O(m) time.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN1009593X
• 書誌情報: 情報処理学会研究報告アルゴリズム（AL）; 巻 1992, 号 58(1992-AL-028), p. 9-16, 発行日 1992-07-17
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会