一種改進的動態幾何圖形的生成算法

李曉霞

摘要：如何根據用戶輸入的已知條件生成幾何圖形是幾何定理機器可讀證明過程中首先要解決的問題。針對幾何定理機器證明過程中圖形的生成及動態變換問題，結合幾何命題的構造性特點，提出了一種改進的幾何約束求解算法，該方法通過代數方程組來表示和處理幾何圖形的約束關系，并將代數方程組化簡為三角列式，通過對三角列式的求解來完成圖形的生成和變換。通過對比證明該算法克服了傳統方法的一些缺陷，并能較好地實現幾何圖形的動態特性。

關鍵詞：幾何約束關系； 約束求解； 謂詞語句； 構造語句； 三角列

中圖分類號：TP181 文獻標識碼：A文章編號：2095-2163（2013）06-0088-04

幾何定理機器證明已有數十年的探索與發展，針對結論產生的可讀證明也日漸成熟，但人們對證明過程的分析與理解還是要依托借助于幾何圖形，而在分析幾何圖形時，仍然需要經常拖動圖形中的某些點，然后查看圖形的相應變化。因此，如何根據用戶輸入的已知條件生成動態幾何圖形，是幾何定理機器證明中亟待解決的首要問題。而幾何圖形是由幾何元素以及這些元素之間的約束關系所組成的，圖形的生成過程就是確定幾何元素及其約束關系的過程，而且在圖形動態變化時，還需要保持幾何元素之間的約束關系依然成立，在本質上這是一個約束求解的過程[1]。

1傳統的幾何約束求解方法

使用傳統的幾何約束求解算法在解答圖形問題時，首先要根據給出的已知幾何信息，確定某點P后，遍歷和點P相關的所有其他點P1，再依據相應的幾何約束關系生成或更新P1的狀態。然后，對點P1進行類似的操作，如此不斷持續，直到所有點都得到生成或點的狀態均實現了更新。該方法的原理比較簡單，但算法卻需要進行多次的遍歷比較，使得效率不是很高。同時由于傳統算法未能對幾何約束關系采取統一的表示方法，因此很難保證圖形的正確性及完整性，并且對于許多圖形的退化條件也未能給出正確的結果[1]。

使用代數方程來處理幾何圖形的約束關系在1948年Tarski就提出了，但由于該方法效率低，并未獲得實際的應用。1977年，吳方法的出現在幾何定理的機器證明方面取得了巨大的成功，吳方法通過引進坐標系，將幾何定理的前提條件（幾何約束）統一表示為代數方程的形式，定理的證明就等價于條件的代數方程能否推出結論的代數方程，實驗證明吳方法的證明效率是比較高的[2]。但吳方法主要適用于定理的判定，并不適用于定理的可讀證明，如果用吳方法去直接求解幾何圖形，則可能會導致求解結果和用戶所預期的結果相差甚遠，本文即試圖尋求一種高效的動態圖形生成算法。

2算法思想

受吳方法的啟示，本文將幾何圖形中的約束關系統一表示為代數方程組的形式，通過對代數方程組的化簡、求解來生成圖形。在將幾何定理的約束條件轉化為代數方程的過程中，一個關鍵步驟就是給定理中的點設定坐標參數。從理論上來說，點的坐標參數的任意性并不影響定理的有效性。然而參數選擇不當，很容易產生一個高度耦合的代數方程組，對這樣的代數方程組進行化簡和求解的復雜度也相應會增加很多。事實上，大部分的幾何定理都是構造型的（可以使用直尺和圓規作圖生成的），因此，可以將兒何定理轉化成構造形狀表示，使每條構造語句只引進一個新的點，并根據該構造順序依次給點的坐標參數賦值，由此得到一個依賴關系相對比較簡單的多項式方程組，再將該方程組局部消解為三角序列的形式，對該三角序列求解就可以快速地實現圖形的計算和變換。

3幾何命題的表示形式

3.1構造形式

因此，一個構造型幾何命題可以表示為GS = （C1，C2…Ck，G）。 這里的每條構圖語Ci（i=1…k） 都分別引入一個新的點，且當i>j時，構圖語句Ci中所有參數U都由之前的構圖語句Cj引進，G是命題結論。

例如：西門松定理（令點D是△ABC的外接圓（o）上的任意一點，從D點作三條垂線到三角形三條邊BC，AC和AB，分別交于E、F和G三個點，證明E、F和G三點共線。）的構造形式如下：

3.2謂詞形式

構造型幾何命題對于描述幾何定理的作圖過程與定理的證明都很方便，但在命題輸入時，構造語句更多地是注重點的順序，而與用戶平時看到的“由假設推得結論”的過程并不相符。因此，人們更習慣輸入前提條件所代表的是幾何圖形中各元素間的約束關系，并且一般都是以謂詞語句的形式表示的。謂詞形式由點的構造序列、假設條件和結論構成，幾何約束關系由謂詞表示[4]。

一個謂詞型的幾何命題可以表述為WS=（Pts，Ps，G）。其中，Pts是命題中的點的序列；Ps是代表命題中各元素間約束關系的謂詞語句；G是命題的結論。

謂詞語句在描述幾何命題時能夠更為直觀地反映命題的前提條件，但點的構造并不嚴格，若轉化成代數方程組，則對該方程組的求解就會比較復雜，因此，需要將用戶輸入的謂詞形式轉換為構造形式。

3.3幾何命題的謂詞形式到構造形式的轉化算法

根據謂詞語句中點的序列Pts，可以將幾何命題的謂詞形式轉化成構造形式，轉化算法如下：

（1）從Pts列表中選擇最后的點X（如果Pts為空，則退出），將點X從Pts中移除。

（2）從Ps中選取所有和X相關的謂詞。由于每個點至多有兩個參數，因此和該點相關的謂詞可能有0，1或2個，若超過兩個，則認為該點是過約束的，定理無法構造，算法結束。

（a）如果和點X相關的謂詞個數為0，則該點是一個自由點，生成構造語句（Point p）；

（b）如果和點X相關的謂詞個數為1，則該點是一個半自由點，生成相應的構造語句；

（c）如果和點X相關的謂詞個數為2，則該點是一個約束點，生成相應的構造語句。

（3）將Ps中所有和點X相關的謂詞都刪除，返回步驟（1）。

通過上述算法，當Pts為空時，就可以逐步得到與命題相關的構造語句。

4動態幾何圖形的生成

將幾何命題的約束條件表示為構造形式后，即可使用改進的幾何約束算法將幾何命題轉化為代數方程組，并對代數方程組進行化簡求解，最終生成動態幾何圖形。算法步驟如下：

（1）給幾何命題中的點分配坐標參數

本算法中的幾何命題采用以點為基礎的表示方法，因此只需要關注幾何定理中點的參數即可。在笛卡爾坐標下，每個點包含x和y兩個參數。 由于構造型幾何命題中的點是逐步引進的，每個構造語句只引進了一個新點，且構造的新點只和之前所構造的點彼此相關。因此，如果根據構造語句中點引進的順序依次給點的坐標分配參數，那么這個點的坐標參數將只依賴于在該點之前己經構造出來的點的參數，由此產生的多項式方程組中的參數依賴關系將會變得相對簡單[5]。令幾何定理中點的構造序列為{P1，P2，…，Pi}，則分配參數的方式為：Pi =（x2i-1， x2i）

其中，x2i-1 ，x2i對應點Pi的坐標參數x，y，對于這些參數變元，還需要給其規定順序，假定當且僅當i

（2）將幾何命題的約束條件轉化為代數方程組

幾何命題的謂詞語句都可以使用代數方程來表示，如點A（x1，x2），B（x3，x4），C（x5，x6）共線的謂詞語句為（OnLine A B C），該語句轉換成代數方程的表示形式為（x6-x2）*（x3-x1）-（x5-x1）*（x4-x2）= 0。

在幾何命題的構造語句中，除自由點外，每條構造語句都是由一條或者兩條謂詞語句產生的，而構造語句的代數方程就是該語句所對應的謂詞語句的代數方程。若構造的點是半自由點，則對應一個多項式方程，該方程引進兩個新參數，其它參數在這兩個參數之前引進；若構造的點是約束點，則對應兩個多項式方程，且引進兩個新參數。

令定理的前提條件所對應的多項式集合為HS，不失一般性，總是有：

（3）將代數方程組化簡為三角列形式

將一般的代數多項式方程組化簡為三角列形式，類似于將一個矩陣轉化成下三角形或者上三角形，該過程并不容易。本算法根據構造語句中點引進的順序依次給點的坐標賦值，由此產生的多項式方程組中的參數依賴關系則變得相對簡單，多項式方程組的耦合度也大大降低，對其化簡就會相對容易。

對于一個半自由點對應的多項式方程，可以把其中的一個參數當作自由變元，另一個參數則由當前的方程引進，因此這個方程不需要化簡就可以直接求解。而關于一個約束點對應兩個多項式方程，則只需要消掉其中一個方程當中的一個參數即可直接求解。因此，構造型幾何命題的多項式方程組的三角化就可以局部分塊進行。令點P的坐標參數為（xi， xi+1），在這里只需要考慮點P是一個約束點的情況，令點P的構造語句所對應的代數方程組是：

在三角列中每個多項式方程只引進一個新的參數。

（4）對三角形式的代數方程組進行順序求解，得到當前圖形的最新狀態。

在CS中，自由變元u1，…，ud對應圖形中的自由點，各變元的值是可以自由選擇的。當u1，…，ud的值被確定以后，剩下的變元x1，…，x2r就可以根據三角化以后的方程組依次求解。此時如果拖動鼠標，使得一個或者多個自由變元u1，…，ud的值發生變化，那么x1，…，x2r也會隨之發生變化，由此即可計算得到圖形中所有的點坐標。該方法使得圖形的基本約束關系始終成立，而且也可以得到滿意的動態效果。

5算法分析

利用代數方法處理幾何圖形的約束關系具有非常重要的意義，因其增強了幾何作圖的能力。通過在幾何定理機器證明平臺中大量的例子證明，該算法避免了傳統約束求解方法的許多問題，且具有如下優點：

（1）求解效率高

本算法中生成的代數方程組是逐步引進坐標點的，且最后三角化的方程組是依次求解的，如此，方程的求解效率就非常高，圖形生成的速度也十分快。

（2）約束求解的過程穩定

本算法中構造語句是基于點的，幾何命題可以通過代數方程直接利用求根根式計算得到，因此求解過程非常穩定，且隨意拖動圖形中的某個點時，不會產生跳躍現象。

（3）可以構造出幾何圖形的多種可能情況

在對代數方程組求解的過程中，對于四次以及四次以下的代數方程可以直接運用求根根式得到方程所有的解。因此，可以構造出幾何圖形的所有可能情況。

（4）重合點的自動發現和去除

在幾何作圖的過程中，經常會遇到產生重合點的情況。所謂重合點，就是指一個新作出的點實際上己經被先前的構造過程產生了。在本算法中能夠將幾何定理的前提條件都轉化成三角形式的代數方程組，且每當一個新的點構造出來的時候，可首先使用數值檢測方法，檢查這個點的坐標是否和先前己經構造的某個點重合[6]，如果兩者的坐標在某個誤差范圍之內，即可判定為重合點，去除該點。

當然本算法也存在不足之處，在用戶輸入的幾何命題前提條件時， 必須要輸入點的序列， 這就要求用戶首先對幾何圖形要有清楚的認識，且命題中涉及到構造特定長度的線段，或特定值的角度，或包含不等式時，使用該方法就存在困難，這也是今后該研究要努力探索的方向。

參考文獻：

[1]張巖.幾何約束求解的偶圖分解法[D].哈爾濱：黑龍江大學，2008：46-55.

[2]吳文俊.初等幾何判定問題與機械化證明[J].中國科學，1977，（6）50-56.

[3]林強， 高小山. 基于幾何約束求解的完備方法[J].計算機輔助設計與圖形學，2007，（7）23-26.

[4]李洪波.幾何定理機器證明的新探索[D].北京：北京大學，1994：23-41.

[5]CHOU S C，GAO X S，ZHANG J Z.A deductive database approach to automated geometry theorem proving and discovering[J]. Journal of Auto-mated Reasoning，2000，25（3）：219-246.

[6]李傳中，張景中.超級畫板[M]. 北京：北京師范大學出版社，2004.