No Cover Image

Conference Paper/Proceeding/Abstract 201 views 21 downloads

On Computing the Union of MUSes / Carlos Mencía; Oliver Kullmann; Alexey Ignatiev; Joao Marques-Silva

Theory and Applications of Satisfiability Testing – SAT 2019, Volume: 11628, Pages: 211 - 221

Swansea University Author: Oliver, Kullmann

Abstract

The situation is considered where a satisfiability problem represents for example a manufacturing specification, and thus unsatisfiability of the problem means that something is wrong with the specification. In response to this an infeasibility analysis is needed, where we consider the robust notion...

Full description

Published in: Theory and Applications of Satisfiability Testing – SAT 2019
ISBN: 978-3-030-24257-2 978-3-030-24258-9
ISSN: 0302-9743 1611-3349
Published: Springer, Cham
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa50334
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: The situation is considered where a satisfiability problem represents for example a manufacturing specification, and thus unsatisfiability of the problem means that something is wrong with the specification. In response to this an infeasibility analysis is needed, where we consider the robust notion of "union of MUSes", that is, all clauses need to be computed, which are potentially necessary for the contradiction to arise (become necessary after some some other clauses are removed).The paper proposes a novel algorithm for this problem, proves its correctness, and provides experimental evidence for practical applicability.
Keywords: minimal unsatisfiable subsets, infeasibility analysis, algorithms
College: College of Science
Start Page: 211
End Page: 221