多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装

柴田, 直樹; 岡野, 浩三; 谷口, 健一

多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装

柴田, 直樹; 岡野, 浩三; 谷口, 健一

電子情報通信学会技術研究報告. COMP, コンピュテーション, 1999, 99(432), 1-8

アクセス数:737件（2025-07-16 10:56 集計）

固定URL: https://hdl.handle.net/11094/27436

閲覧可能ファイル

ファイル	フォーマット	利用条件	サイズ	閲覧回数	利用開始日	説明	information
itr099_432_001	pdf	なし	946 KB	58	2014.04.11

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル	多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装
	A decision algorithm for rational Presburger sentences using a division routine of polyhedra
	タメンタイ　ブンカツ　ヲ　モチイタ　ユウリスウ　プレスブルガーブン　シンギ　ハンテイ　アルゴリズム　ト　ソノ　ジッソウ
著者	NRID 1000040335477 1000040335477 著者名柴田, 直樹 ; シバタ, ナオキ ; Shibata, Naoki
	NRID 1000070252632 1000070252632 著者名岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
	NRID 1000000029513 1000000029513 著者名谷口, 健一 ; タニグチ, ケンイチ ; Taniguchi, Kenichi
キーワード等	加算をもつ有理数の理論
	真偽判定アルゴリズム
	組合せ幾何学
	加算を持つ有理数の理論
	真偽判定アルゴリズム多面体
	Theoery of rationals with addtion
	decision procedure and polyhedra
抄録	加算を持つ有理数の理論(有理数変数,有理数定数,+,-,=,<,∧,∨,∀,∃からなる理論)の上の冠頭形の閉論理式(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.
出版者	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名	電子情報通信学会技術研究報告. COMP, コンピュテーション
巻(号)	99(432)
ページ	1-8
刊行年月	1999-11-16
言語	日本語
ハンドルURL	https://hdl.handle.net/11094/27436
NCID	AN10013152
アクセス権	open access
権利情報	Copyright © 1999 IEICE
権利情報	本文データはCiNiiから複製したものである
出版タイプ	Version of Record
カテゴリ	学術雑誌論文 Journal Article

資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
DCMI資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. COMP, コンピュテーション. 1999, 99(432), p. 1-8
DC.title	多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装
	A decision algorithm for rational Presburger sentences using a division routine of polyhedra
	タメンタイ　ブンカツ　ヲ　モチイタ　ユウリスウ　プレスブルガーブン　シンギ　ハンテイ　アルゴリズム　ト　ソノ　ジッソウ
DC.creator	柴田, 直樹
	シバタ, ナオキ
	Shibata, Naoki
	岡野, 浩三
	オカノ, コウゾウ
	Okano, Kozo
	谷口, 健一
	タニグチ, ケンイチ
	Taniguchi, Kenichi
DC.publisher	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
DC.language' scheme='DCTERMS.RFC1766	日本語
DC.type' scheme='DCTERMS.DCMIType	text
DCTERMS.issued' scheme='DCTERMS.W3CDTF	1999-11-16
DC.subject	加算をもつ有理数の理論
	真偽判定アルゴリズム
	組合せ幾何学
	加算を持つ有理数の理論
	真偽判定アルゴリズム多面体
	Theoery of rationals with addtion
	decision procedure and polyhedra
DCTERMS.abstract	加算を持つ有理数の理論(有理数変数,有理数定数,+,-,=,<,∧,∨,∀,∃からなる理論)の上の冠頭形の閉論理式(PRP文と呼ぶ)の真偽判定ルーチンはプロトコルのテスト,ハードウェアのタイミング検証などに利用される.著者らは最も速いPRP文の真偽判定アルゴリズムよりを既に提案している.本稿では,筆者らが提案したアルゴリズムの多面体分割を用いた高速化法と,その評価について述べる.高速化法として,次の3点が挙げられる.1.多面体同士を併合し,その結果できる凹多面体も扱えるようにすることで,処理する多面体の数を最小限にする.2.投影の領域を計算する方法を改善し,真偽判定に必要ない多面体を処理する手間を減らす.3.投影の領域を計算する際の凹多面体同士の交差判定の回数を減らす.
DCTERMS.abstract	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.
DC.rights	Copyright © 1999 IEICE
DC.rights	本文データはCiNiiから複製したものである
DC.format	27436
citation_title	多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装
citation_author	柴田, 直樹
	岡野, 浩三
	谷口, 健一
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	1999-11-16
citation_journal_title	電子情報通信学会技術研究報告. COMP, コンピュテーション
citation_volume	99
citation_issue	432
citation_firstpage	1
citation_lastpage	8
citation_public_url	https://hdl.handle.net/11094/27436

多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装

閲覧可能ファイル

論文情報

論文詳細を表示