From e1199493f43a9b891914abdb78657794a35922fb Mon Sep 17 00:00:00 2001 From: Hannes Weichelt Date: Thu, 9 May 2024 17:36:31 +0200 Subject: [PATCH] renamed MUC->MUS CoreComputer --- src/clingexplaid/cli/clingo_app.py | 6 +-- src/clingexplaid/muc/core_computer.py | 54 +++++++++++++-------------- 2 files changed, 30 insertions(+), 30 deletions(-) diff --git a/src/clingexplaid/cli/clingo_app.py b/src/clingexplaid/cli/clingo_app.py index 80930d0..733552a 100644 --- a/src/clingexplaid/cli/clingo_app.py +++ b/src/clingexplaid/cli/clingo_app.py @@ -192,7 +192,7 @@ def _method_muc( ) return - muc_string = " ".join(cc.muc_to_string(cc.minimal)) + muc_string = " ".join(cc.mus_to_string(cc.minimal)) self._print_muc(muc_string) if compute_unsat_constraints: @@ -213,9 +213,9 @@ def _method_muc( if program_unsat: mucs = 0 - for muc in cc.get_multiple_minimal(max_mucs=max_models): + for muc in cc.get_multiple_minimal(max_mus=max_models): mucs += 1 - muc_string = " ".join(cc.muc_to_string(muc)) + muc_string = " ".join(cc.mus_to_string(muc)) self._print_muc(muc_string) if compute_unsat_constraints: diff --git a/src/clingexplaid/muc/core_computer.py b/src/clingexplaid/muc/core_computer.py index d892043..b43de77 100644 --- a/src/clingexplaid/muc/core_computer.py +++ b/src/clingexplaid/muc/core_computer.py @@ -1,5 +1,5 @@ """ -MUC Module: Core Computer to get Minimal Unsatisfiable Cores +MUS Module: Core Computer to get Minimal Unsatisfiable Subsets """ from itertools import chain, combinations @@ -25,7 +25,7 @@ def __init__(self, control: clingo.Control, assumption_set: AssumptionSet): def _solve(self, assumptions: Optional[AssumptionSet] = None) -> Tuple[bool, SymbolSet, SymbolSet]: """ - Internal function that is used to make the single solver calls for finding the minimal unsatisfiable core. + Internal function that is used to make the single solver calls for finding the minimal unsatisfiable subset. """ if assumptions is None: assumptions = self.assumption_set @@ -39,8 +39,8 @@ def _solve(self, assumptions: Optional[AssumptionSet] = None) -> Tuple[bool, Sym def _compute_single_minimal(self, assumptions: Optional[AssumptionSet] = None) -> AssumptionSet: """ - Function to compute a single minimal unsatisfiable core from the passed set of assumptions and the program of - the CoreComputer. If there is no minimal unsatisfiable core, since for example the program with assumptions + Function to compute a single minimal unsatisfiable subset from the passed set of assumptions and the program of + the CoreComputer. If there is no minimal unsatisfiable subset, since for example the program with assumptions assumed is satisfiable, an empty set is returned. The algorithm that is used to compute this minimal unsatisfiable core is the iterative deletion algorithm. """ @@ -49,7 +49,7 @@ def _compute_single_minimal(self, assumptions: Optional[AssumptionSet] = None) - # check that the assumption set isn't empty if not assumptions: - raise ValueError("A minimal unsatisfiable core cannot be computed on an empty assumption set") + raise ValueError("A minimal unsatisfiable subset cannot be computed on an empty assumption set") # check if the problem with the full assumption set is unsatisfiable in the first place, and if not skip the # rest of the algorithm and return an empty set. @@ -57,37 +57,37 @@ def _compute_single_minimal(self, assumptions: Optional[AssumptionSet] = None) - if satisfiable: return set() - muc_members: Set[Assumption] = set() + mus_members: Set[Assumption] = set() working_set = set(assumptions) for assumption in assumptions: # remove the current assumption from the working set working_set.remove(assumption) - satisfiable, _, _ = self._solve(assumptions=working_set.union(muc_members)) - # if the working set now becomes satisfiable without the assumption it is added to the muc_members + satisfiable, _, _ = self._solve(assumptions=working_set.union(mus_members)) + # if the working set now becomes satisfiable without the assumption it is added to the mus_members if satisfiable: - muc_members.add(assumption) - # every time we discover a new muc member we also check if all currently found muc members already - # suffice to make the instance unsatisfiable. If so we can stop the search sice we fund our muc. - if not self._solve(assumptions=muc_members)[0]: + mus_members.add(assumption) + # every time we discover a new mus member we also check if all currently found mus members already + # suffice to make the instance unsatisfiable. If so we can stop the search sice we found our mus. + if not self._solve(assumptions=mus_members)[0]: break - return muc_members + return mus_members def shrink(self, assumptions: Optional[AssumptionSet] = None) -> None: """ - This function applies the unsatisfiable core minimization (`self._compute_single_minimal`) on the assumptions - set `assumptions` and stores the resulting MUC inside `self.minimal`. + This function applies the unsatisfiable subset minimization (`self._compute_single_minimal`) on the assumptions + set `assumptions` and stores the resulting MUS inside `self.minimal`. """ self.minimal = self._compute_single_minimal(assumptions=assumptions) - def get_multiple_minimal(self, max_mucs: Optional[int] = None) -> Generator[AssumptionSet, None, None]: + def get_multiple_minimal(self, max_mus: Optional[int] = None) -> Generator[AssumptionSet, None, None]: """ - This function generates all minimal unsatisfiable cores of the provided assumption set. It implements the - generator pattern since finding all mucs of an assumption set is exponential in nature and the search might not - fully complete in reasonable time. The parameter `max_mucs` can be used to specify the maximum number of - mucs that are found before stopping the search. + This function generates all minimal unsatisfiable subsets of the provided assumption set. It implements the + generator pattern since finding all mus of an assumption set is exponential in nature and the search might not + fully complete in reasonable time. The parameter `max_mus` can be used to specify the maximum number of + mus that are found before stopping the search. """ assumptions = self.assumption_set assumption_powerset = chain.from_iterable( @@ -120,21 +120,21 @@ def get_multiple_minimal(self, max_mucs: Optional[int] = None) -> Generator[Assu found_mucs.append(muc) yield muc # if the maximum muc amount is found stop search - if max_mucs is not None and len(found_mucs) == max_mucs: + if max_mus is not None and len(found_mucs) == max_mus: break - def muc_to_string(self, muc: AssumptionSet, literal_lookup: Optional[Dict[int, clingo.Symbol]] = None) -> Set[str]: + def mus_to_string(self, muc: AssumptionSet, literal_lookup: Optional[Dict[int, clingo.Symbol]] = None) -> Set[str]: """ - Converts a MUC into a set containing the string representations of the contained assumptions + Converts a MUS into a set containing the string representations of the contained assumptions """ # take class literal_lookup as default if no other is provided if literal_lookup is None: literal_lookup = self.literal_lookup - muc_string = set() + mus_string = set() for a in muc: if isinstance(a, int): - muc_string.add(str(literal_lookup[a])) + mus_string.add(str(literal_lookup[a])) else: - muc_string.add(str(a[0])) - return muc_string + mus_string.add(str(a[0])) + return mus_string