Hans de Nivelle - 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 ResolutionArticle

Authors: Hans de Nivelle

    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
    Accepted on: August 9, 2018
    Submitted on: March 9, 2017
    Keywords: Computer Science - Logic in Computer Science,F.4.1,I.2.3

    1 Document citing this article

    Consultation statistics

    This page has been seen 1595 times.
    This article's PDF has been downloaded 269 times.