Approximately Solving Set Equations
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
Abstract
Unification with constants modulo the theory ACUI of an associative (A), commutative (C) and idempotent (I) binary function symbol with a unit (U) corresponds to solving a very simple type of set equations. It is well-known that solvability of systems of such equations can be decided in polynomial time by reducing it to satisfiability of propositional Horn formulae. Here we introduce a modified version of this problem by no longer requiring all equations to be completely solved, but allowing for a certain number of violations of the equations. We introduce three different ways of counting the number of violations, and investigate the complexity of the respective decision problem, i.e., the problem of deciding whether there is an assignment that solves the system with at most l violations for a given threshold value l.
Details
Originalsprache | Englisch |
---|---|
Titel | Proceedings of the 30th International Workshop on Unification (UNIF'16) |
Seiten | 37-41 |
Seitenumfang | 5 |
Publikationsstatus | Veröffentlicht - 2016 |
Peer-Review-Status | Ja |
Externe IDs
ORCID | /0000-0002-4049-221X/work/142247956 |
---|