Approximately Solving Set Equations

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-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 languageEnglish
Title of host publicationProceedings of the 30th International Workshop on Unification (UNIF'16)
Pages37-41
Number of pages5
Publication statusPublished - 2016
Peer-reviewedYes

External IDs

ORCID /0000-0002-4049-221X/work/142247956

Keywords