Unsatisfiable Subsets¶

These examples highlight how the different relevant unsatisfiable subsets (MUS, MSS, MCS) can be computed. We separate the examples into ones for finding a single subset versus ones for finding multiple.

Finding a single subset¶

Finding a single MUS¶

from clingexplaid.preprocessors import AssumptionPreprocessor, FilterSignature
from clingexplaid.unsat import SubsetComputer

PROGRAM = """
a(1..3).
{b(4..6)}.

a(X) :- b(X).

:- a(X), X>=3.
"""

ap = AssumptionPreprocessor(filters={FilterSignature("a", 1)})
ap.process(PROGRAM)
ap.control.ground([("base", [])])
sc = SubsetComputer(ap.control, ap.assumptions)


def shrink_on_core(core) -> None:
    mus = sc.mus(core)
    print(mus)


ap.control.solve(assumptions=list(ap.assumptions), on_core=shrink_on_core)

The SubsetComputer.mus() method can simple be swapped with SubsetComputer.mss() or SubsetComputer.mcs() to compute the respective other subset types

Finding a multiple subsets¶

Finding multiple MUSs¶

from clingexplaid.preprocessors import AssumptionPreprocessor
from clingexplaid.unsat import SubsetComputer

PROGRAM = """
a(1..3).
b(1..3).

:- a(X), b(X).
"""

ap = AssumptionPreprocessor()
ap.process(PROGRAM)
ap.control.ground([("base", [])])
sc = SubsetComputer(ap.control, ap.assumptions)

for i, mus in enumerate(sc.multiple()):
    print(f"{i}:", mus)

Finding multiple relevant subsets (MUS, MSS, and MCS)¶

from clingexplaid.preprocessors import AssumptionPreprocessor
from clingexplaid.unsat import SubsetComputer
from clingexplaid.unsat.sets import [
    MinimalUnsatisfiableSubset,
    MaximalSatisfiableSubset,
    MinimalCorrectionSet
]

PROGRAM = """
a(1..3).
b(1..3).

:- a(X), b(X).
"""

ap = AssumptionPreprocessor()
ap.process(PROGRAM)
ap.control.ground([("base", [])])
sc = SubsetComputer(ap.control, ap.assumptions)

types = [MinimalUnsatisfiableSubset, MaximalSatisfiableSubset, MinimalCorrectionSet]
for i, subset in enumerate(sc.multiple(types)):
    print(f"{i}:", subset)

Finding multiple MUSs with a custom Lattice¶

Clingo-Explaid's SubsetComputer uses an internal Lattice to decide the order in which subset candidates are explored. By default it uses the AssumptionLattice, which is defined in this MUS core utilities repository musclingo. You can also use your own lattice, by defining a custom LatticeFactory that provides it to the SubsetComputer. The following is an example showing this by re-implementing the AssumptionLattice.

from clingexplaid.preprocessors import AssumptionPreprocessor
from clingexplaid.unsat import SubsetComputer
from clingexplaid.unsat.lattice import LatticeFactory

PROGRAM = """
a(1..3).
b(1..3).

:- a(X), b(X).
"""


class MyLatticeFactory(LatticeFactory):
    def __init__(self, bias: bool):
        super().__init__()
        self._bias = bias

    def new(self, literals: set[int]):
        return AssumptionLattice(literals, bias=self._bias)


ap = AssumptionPreprocessor()
ap.process(PROGRAM)
ap.control.ground([("base", [])])
sc = SubsetComputer(ap.control, ap.assumptions, lattice_factory=MyLatticeFactory(True))

for i, mus in enumerate(sc.multiple()):
    print(f"{i}:", mus)