すべての変数が存在記号で束縛された冠頭標準形プレスブルガー文の真偽判定の高速化手法

情報処理学会 Web Site 被引用文献2件 参考文献11件

書誌事項

タイトル別名
  • スベテ ノ ヘンスウ ガ ソンザイ キゴウ デ ソクバクサレタ カン トウヒョ
  • Techniques to Reduce Computation Time in Decision Procedure for Prenex Normal Form Presburger Sentences Bounded only by Existential Quantifiers
  • 定理自動証明

この論文をさがす

説明

すベての変数（整数型）が存在記号で束縛された冠頭標準形のプレスブルガー文（EPP文）の真偽判定を高速化する方法と，その評価について述べる．判定するEPP文中の不等式から定まる有限個の値を代入して式中の変数を一つずつ消去していくCooper・直井の判定法を用いる．判定高速化のため，次の工夫（1）?（4）を施した：（1）変数消去のたびに，式をなるべく簡単化し，式中に出現する変数や不等式を減らす，（2）構文木の根に近い位置に出現する不等式中の変数から先に消去する，（3）EPP文が偽であることを検証する場合には，簡単化によって変数が数個程度に減少したとき，実数上の線形計画法を利用して式の充足不能性を（変数消去法を用いず）直接調べる，（4）Cooper・直井の判定法では，変数に関する多元連立1次合同式の解をバックトラック探索により求めるが，このとき解の個数が少ないと予想される変数から解を探索する．従来，実際的な例題ではEPP文の変数が20?30個程度になる場合があり，Cooper・直井の判定法では実用時間で真偽判定を行えなかったが，以上の工夫により，そのような多くのEPP文の真偽をCPU時間10分程度（Pentium Pro200MHz）で判定できるようになった．

In this paper we present an efficient implementation of a decision procedure EPP-sentences(prenex normal form Presburger sentences bounded only by existential quantifiers).Our procedure is based on the Cooper and Naoi's algorithm.In the algorithm,variables in a given expression are eliminated by substituting several values obtained from inequalities in the expression.For speed-up,we have added the following devices to the algorithm;(1)simplify every expression obtained by any substitution,so to decrease the number of variables and inequalities,(2)adopt an elimination-order such that a variable close to the root of the syntax tree of the expression will be substituted first,(3)when the number of variables is enough decreased,check directly if the expression is satisfiable or not,using liner programming technique on real numbers,and(4)at searching solutions for simultaneous linear congruences by back tracking,search first the solutions for a variable which is expected to have less number of solutions.Our procedure can determine the truth of a lot of EPP-sentences,which contain 20 through 30 variables,within about ten minutes(Pentium Pro 200 MHz).

収録刊行物

被引用文献 (2)*注記

もっと見る

参考文献 (11)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ