Approximately Solving Set Equations
Research output: Contribution to book/conference proceedings/anthology/report › Conference contribution › Contributed › peer-review
Contributors
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
Original language | English |
---|---|
Title of host publication | Proceedings of the 30th International Workshop on Unification (UNIF'16) |
Pages | 37-41 |
Number of pages | 5 |
Publication status | Published - 2016 |
Peer-reviewed | Yes |
External IDs
ORCID | /0000-0002-4049-221X/work/142247956 |
---|