Approximately Solving Set Equations

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
TitelProceedings of the 30th International Workshop on Unification (UNIF'16)
Seiten37-41
Seitenumfang5
PublikationsstatusVeröffentlicht - 2016
Peer-Review-StatusJa

Externe IDs

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

Schlagworte