一种改进的动态几何图形的生成算法

李晓霞

摘要：如何根据用户输入的已知条件生成几何图形是几何定理机器可读证明过程中首先要解决的问题。针对几何定理机器证明过程中图形的生成及动态变换问题，结合几何命题的构造性特点，提出了一种改进的几何约束求解算法，该方法通过代数方程组来表示和处理几何图形的约束关系，并将代数方程组化简为三角列式，通过对三角列式的求解来完成图形的生成和变换。通过对比证明该算法克服了传统方法的一些缺陷，并能较好地实现几何图形的动态特性。

关键词：几何约束关系； 约束求解； 谓词语句； 构造语句； 三角列

中图分类号：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.