| 講演名 | 1999/11/16 多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装 柴田 直樹, 岡野 浩三, 谷口 健一, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 加算を持つ有理数の理論(有理数変数,有理数定数,+,-,=,<,∧,∨,∀,∃からなる理論)の上の冠頭形の閉論理式(PRP文と呼ぶ)の真偽判定ルーチンはプロトコルのテスト,ハードウェアのタイミング検証などに利用される.著者らは最も速いPRP文の真偽判定アルゴリズムよりを既に提案している.本稿では,筆者らが提案したアルゴリズムの多面体分割を用いた高速化法と,その評価について述べる.高速化法として,次の3点が挙げられる.1.多面体同士を併合し,その結果できる凹多面体も扱えるようにすることで,処理する多面体の数を最小限にする.2.投影の領域を計算する方法を改善し,真偽判定に必要ない多面体を処理する手間を減らす.3.投影の領域を計算する際の凹多面体同士の交差判定の回数を減らす. |
| 抄録(英) | Formerly, we have proposed the fastest decision algorithm for prenex-normal-form rational Presburger Sentences. The algorithm is used in areas of testing of protocols, timing verification of hardware, and so on. In this paper, we present techniques to reduce execution time of the algorithm. The techniques are based on three devices: 1. Making the algorithm merge polyhedra into a concave polyhedron and handle the concave polyhedron in order to minimize the number of polyhedra that express a region, 2. Improving a method to calculate a region of a shadow without processing extra polyhedra that don't affect the result of the decision and 3. Reducing the number of judgements on whether faces are crossing. |
| キーワード(和) | 加算を持つ有理数の理論 / 真偽判定アルゴリズム多面体 |
| キーワード(英) | Thoery of rationals with addtion / decision procedure and polyhedra |
| 資料番号 | COMP99-49 |
| 発行日 |
| 研究会情報 | |
| 研究会 | COMP |
|---|---|
| 開催期間 | 1999/11/16(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Theoretical Foundations of Computing (COMP) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装 |
| サブタイトル（和） | |
| タイトル（英） | A decision algorithm for rational Presburger sentences using a division routine of polyhedra |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 加算を持つ有理数の理論 / Thoery of rationals with addtion |
| キーワード(2)（和/英） | 真偽判定アルゴリズム多面体 / decision procedure and polyhedra |
| 第 1 著者 氏名（和/英） | 柴田 直樹 / Naoki SHIBATA |
| 第 1 著者 所属（和/英） | 大阪大学大学院基礎工学研究科情報数理系専攻 Division of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 岡野 浩三 / Kozo OKANO |
| 第 2 著者 所属（和/英） | 大阪大学大学院基礎工学研究科情報数理系専攻 Division of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 第 3 著者 氏名（和/英） | 谷口 健一 / Kenichi TANIGUCHI |
| 第 3 著者 所属（和/英） | 大阪大学大学院基礎工学研究科情報数理系専攻 Division of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 発表年月日 | 1999/11/16 |
| 資料番号 | COMP99-49 |
| 巻番号（vol） | vol.99 |
| 号番号（no） | 432 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |