de Nivelle, Hans - Subsumption Algorithms for Three-Valued Geometric Resolution

lmcs:3179 - Logical Methods in Computer Science, December 11, 2018, Volume 14, Issue 4 - https://doi.org/10.23638/LMCS-14(4:24)2018
Subsumption Algorithms for Three-Valued Geometric Resolution

Authors: de Nivelle, Hans

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.


Volume: Volume 14, Issue 4
Published on: December 11, 2018
Submitted on: March 9, 2017
Keywords: Computer Science - Logic in Computer Science,F.4.1,I.2.3


Share

Consultation statistics

This page has been seen 296 times.
This article's PDF has been downloaded 128 times.