TY - JOUR
T1 - Subsumption algorithms for three-valued geometric resolution
AU - de Nivelle, Hans
N1 - Publisher Copyright:
© 2018, Logical Methods in Computer Science. All rights reserved.
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85060231114&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85060231114&partnerID=8YFLogxK
U2 - 10.23638/LMCS-14(4:24)2018
DO - 10.23638/LMCS-14(4:24)2018
M3 - Article
AN - SCOPUS:85060231114
SN - 1860-5974
VL - 14
SP - 1
EP - 29
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
IS - 4-24
ER -