带未解释函数的等式理论(EUF)是一种表达能力较强的理论,在形式化方法中占据了重要的地位。本文研究的是无量词的EUF理论,该理论的判定问题已被证明是一个NP完全问题。这一理论的判定过程在形式化验证领域得到了广泛的应用,很多实际问题可以建模成EUF理论判定问题,电路的等价性验证、程序的等价性验证、编译的转换有效性验证等。针对EUF理论的可满足性求解问题,已经有可以判定它们的SMT求解器,这些基于同余闭包算法所实现的求解器目前仅仅能够求解EUF合取式。本文的目标是判定一般EUF公式,它的判定过程大体上分为两类:惰性编码和活性编码。惰性编码是一种基于SAT求解器与理论求解器交替使用的判定方法,而活性编码是一种将EUF公式归约为命题公式,仅仅使用SAT求解器的判定方法。活性编码判定过程不需要为EUF理论开发特定的理论求解器,该方法在解决某些问题时更具有优势,比如组合理论的判定问题。本文以寻找高效的EUF理论的活性编码判定过程为目的,研究了一种活性编码方法。该方法通过Ackermann归约以及基于非极性等式图的归约,将EUF公式归约为等可满足性的命题公式。在这个活性编码方法中,两个归约算法都分别给公式添加了大量的约束,因此该方法实现起来有很大的难度。为了简化这一方法的实现进程,本文提供了C++语言编写的DPLIB库,根据上述算法添加程序并成功编译于Linux系统,证明了该方法是一种可实现的判定过程,调用它可以求解一般的EUF公式。此外,本文给出了一列EUF合取式,对于同一示例分别使用本文提到的两种方法进行求解,实验数据表明,与同余闭包算法相比,上述活性编码方法有更高的求解效率。