一句话：将三值几何归结的包含/匹配归约为广义约束满足，提出直接算法、SAT 编码与局部一致性过滤。
在几何归结实现中，最昂贵的操作是包含测试（匹配）：给定只含变量原子、等式和存在量词的三值几何公式，以及只含常量原子的解释，判定该公式在该解释下是否为假。由于原子没有项结构，匹配十分困难。本文将匹配问题翻译为广义约束满足问题（GCSP），讨论高效求解方法，包括一个直接算法和两种到命题 SAT 的翻译；随后研究基于局部一致性检查的过滤技术，以先验反驳大量 GCSP。最后，作者改造匹配算法，使其找到仅使用解释极小子集的解，且该改造可与任意匹配算法结合。这些技术也可能用于独立于几何归结的约束求解。
In our implementation of geometric resolution, the most costly operation is subsumption testing (or matching): One has to decide for a three-valued, geometric formula, if this formula is false in a given interpretation. The formula contains only atoms with variables, equality, and existential quantifiers. The interpretation contains only atoms with constants. Because the atoms have no term structure, matching for geometric resolution is hard. We translate the matching problem into a generalized constraint satisfaction problem, and discuss several approaches for solving it efficiently, one direct algorithm and two translations to propositional SAT. After that, we study filtering techniques based on local consistency checking. Such filtering techniques can a priori refute a large percentage of generalized constraint satisfaction problems. Finally, we adapt the matching algorithms in such a way that they find solutions that use a minimal subset of the interpretation. The adaptation can be combined with every matching algorithm. The techniques presented in this paper may have applications in constraint solving independent of geometric resolution.Comment: This version was revised on 18.05.2018