Unsatisfiable Subset Functionality

Minimal Unsatisfiable Core Utilities.

__all__ = ['AssumptionWrapper', 'Subset', 'SubsetComputer'] module-attribute

AssumptionWrapper(literal: int, symbol: Symbol, sign: bool) dataclass

Container class for assumptions.

__hash__() -> int

Return self.literal for hashing.

Subset(assumptions: set[AssumptionWrapper]) dataclass

Bases: ABC

Container class for different types for subsets.

assumptions_string: str property

A rendered string representation of the assumptions.

symbol_strings: set[str] property

A set of rendered string representation of the assumption symbols.

__iter__() -> Iterator[tuple[clingo.Symbol, bool] | int]

Iterate of the assumption symbols.

__str__() -> str

Return a string representation of the subset.

iter_literals() -> Iterator[int]

Iterate over all assumption literals in the unsatisfiable subset.

iter_symbols() -> Iterator[tuple[clingo.Symbol, bool]]

Iterate over all assumption symbols in the unsatisfiable subset.

SubsetComputer(control: clingo.Control, assumptions: Iterable[int | tuple[Symbol, bool]], lattice_factory: LatticeFactory | None = None)

Compute fundamental subsets of unsatisfiable problems.

Construct the SubsetComputer with the given control, assumptions, and optional lattice factory.

PARAMETER	DESCRIPTION
control	The clingo control object. TYPE: Control
assumptions	The assumptions to use for computing relevant subsets. TYPE: Iterable[int | tuple[Symbol, bool]]
lattice_factory	The lattice factory to use for choosing the next subset to check, by default None. TYPE: LatticeFactory | None DEFAULT: None

last_mus: MinimalUnsatisfiableSubset | None property

The last MUS that was found.

is_valid(assumptions: set[int]) -> bool

Check whether the program with the provided assumptions is valid.

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals to check the SubsetComputer's program's validity against. TYPE: set[int]

RETURNS	DESCRIPTION
valid	Indicates wheter the SubsetComputer's input is valid.

mcs(assumptions: Iterable[int | tuple[Symbol, bool]] | None = None) -> MinimalCorrectionSet | None

Find a singlular MCS. This method is a wrapper around SubsetComputer.multiple().

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals that form an unsatisfiable subset (US). TYPE: Iterable[int | tuple[Symbol, bool]] | None DEFAULT: None

RETURNS	DESCRIPTION
mcs	A MinimalCorrectionSet if one is found or None if the input is invalid.

mss(assumptions: Iterable[int | tuple[Symbol, bool]] | None = None) -> MaximalSatisfiableSubset | None

Find a singlular MSS. This method is a wrapper around SubsetComputer.multiple().

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals that form an unsatisfiable subset (US). TYPE: Iterable[int | tuple[Symbol, bool]] | None DEFAULT: None

RETURNS	DESCRIPTION
mss	A MaximalSatisfiableSubset if one is found or None if the input is invalid.

multiple(assumptions: Iterable[int | tuple[Symbol, bool]] | None = None, types: set[type[MinimalUnsatisfiableSubset] | type[MaximalSatisfiableSubset] | type[MinimalCorrectionSet]] | None = None, maximum: int | None = None, timeout: float | None = None) -> Generator[Subset, None, None]

Find multiple fundamental subsets filtered by the types argument.

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals that form an unsatisfiable subset (US). TYPE: Iterable[int | tuple[Symbol, bool]] | None DEFAULT: None
types	A set of Subset classes that filters which kinds of subsets are yielded in the search. Equals {MinimalUnsatisfiableSubset} by default. TYPE: set[type[MinimalUnsatisfiableSubset] | type[MaximalSatisfiableSubset] | type[MinimalCorrectionSet]] | None DEFAULT: None
maximum	The maximum amout of subsets to be found. The search is stopped after this amout is reached. TYPE: int | None DEFAULT: None
timeout	Sets a timeout in seconds, that if exceeded stops the subset search. TYPE: float | None DEFAULT: None

YIELDS	DESCRIPTION
subset	A subets matching the types specified in types.

mus(assumptions: Iterable[int | tuple[Symbol, bool]] | None = None, timeout: float | None = None) -> Subset

Find a singlular MUS via linear elimination.

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals that form an unsatisfiable subset (US). TYPE: Iterable[int | tuple[Symbol, bool]] | None DEFAULT: None
timeout	Sets a timeout in seconds, that if exceeded stops the search and returns the already found MUS literals. TYPE: float | None DEFAULT: None

RETURNS	DESCRIPTION
mus	A MinimalUnsatisfiableSubset if one is found or an UnsatisfiableSubset if timeout is exceeded or the input is invalid.

computer

Container class for subset computation.

SubsetComputer(control: clingo.Control, assumptions: Iterable[int | tuple[Symbol, bool]], lattice_factory: LatticeFactory | None = None)

Compute fundamental subsets of unsatisfiable problems.

Construct the SubsetComputer with the given control, assumptions, and optional lattice factory.

PARAMETER	DESCRIPTION
control	The clingo control object. TYPE: Control
assumptions	The assumptions to use for computing relevant subsets. TYPE: Iterable[int | tuple[Symbol, bool]]
lattice_factory	The lattice factory to use for choosing the next subset to check, by default None. TYPE: LatticeFactory | None DEFAULT: None

last_mus: MinimalUnsatisfiableSubset | None property

The last MUS that was found.

is_valid(assumptions: set[int]) -> bool

Check whether the program with the provided assumptions is valid.

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals to check the SubsetComputer's program's validity against. TYPE: set[int]

RETURNS	DESCRIPTION
valid	Indicates wheter the SubsetComputer's input is valid.

mcs(assumptions: Iterable[int | tuple[Symbol, bool]] | None = None) -> MinimalCorrectionSet | None

Find a singlular MCS. This method is a wrapper around SubsetComputer.multiple().

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals that form an unsatisfiable subset (US). TYPE: Iterable[int | tuple[Symbol, bool]] | None DEFAULT: None

RETURNS	DESCRIPTION
mcs	A MinimalCorrectionSet if one is found or None if the input is invalid.

mss(assumptions: Iterable[int | tuple[Symbol, bool]] | None = None) -> MaximalSatisfiableSubset | None

Find a singlular MSS. This method is a wrapper around SubsetComputer.multiple().

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals that form an unsatisfiable subset (US). TYPE: Iterable[int | tuple[Symbol, bool]] | None DEFAULT: None

RETURNS	DESCRIPTION
mss	A MaximalSatisfiableSubset if one is found or None if the input is invalid.

multiple(assumptions: Iterable[int | tuple[Symbol, bool]] | None = None, types: set[type[MinimalUnsatisfiableSubset] | type[MaximalSatisfiableSubset] | type[MinimalCorrectionSet]] | None = None, maximum: int | None = None, timeout: float | None = None) -> Generator[Subset, None, None]

Find multiple fundamental subsets filtered by the types argument.

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals that form an unsatisfiable subset (US). TYPE: Iterable[int | tuple[Symbol, bool]] | None DEFAULT: None
types	A set of Subset classes that filters which kinds of subsets are yielded in the search. Equals {MinimalUnsatisfiableSubset} by default. TYPE: set[type[MinimalUnsatisfiableSubset] | type[MaximalSatisfiableSubset] | type[MinimalCorrectionSet]] | None DEFAULT: None
maximum	The maximum amout of subsets to be found. The search is stopped after this amout is reached. TYPE: int | None DEFAULT: None
timeout	Sets a timeout in seconds, that if exceeded stops the subset search. TYPE: float | None DEFAULT: None

YIELDS	DESCRIPTION
subset	A subets matching the types specified in types.

mus(assumptions: Iterable[int | tuple[Symbol, bool]] | None = None, timeout: float | None = None) -> Subset

Find a singlular MUS via linear elimination.

PARAMETER	DESCRIPTION
assumptions	A set of assumption literals that form an unsatisfiable subset (US). TYPE: Iterable[int | tuple[Symbol, bool]] | None DEFAULT: None
timeout	Sets a timeout in seconds, that if exceeded stops the search and returns the already found MUS literals. TYPE: float | None DEFAULT: None

RETURNS	DESCRIPTION
mus	A MinimalUnsatisfiableSubset if one is found or an UnsatisfiableSubset if timeout is exceeded or the input is invalid.

lattice

Wrappers for the musclingo lattice classes.

AssumptionLatticeFactory(bias: bool)

Bases: LatticeFactory

Factory for creating AssumptionLattice instances.

Construct an AssumptionLatticeFactory with the given bias.

PARAMETER	DESCRIPTION
bias	The bias to use for the lattice. TYPE: bool

new(literals: set[int]) -> AssumptionsLattice

Create a new AssumptionLattice instance.

PARAMETER	DESCRIPTION
literals	A list of literals to use for the lattice. TYPE: set[int]

RETURNS	DESCRIPTION
A new AssumptionLattice instance.

LatticeFactory

Bases: ABC

Factory for creating Lattice instances.

new(literals: set[int]) -> Lattice abstractmethod

Create a new Lattice instance.

PARAMETER	DESCRIPTION
literals	A list of literals to use for the lattice. TYPE: set[int]

RETURNS	DESCRIPTION
A new Lattice instance.

sets

Container classes for sets.

MaximalSatisfiableSubset(assumptions: set[AssumptionWrapper]) dataclass

Bases: Subset

Container class for maximal satisfiable subsets (MSS).

MinimalCorrectionSet(assumptions: set[AssumptionWrapper]) dataclass

Bases: Subset

Container class for minimal correction sets (MUS).

MinimalUnsatisfiableSubset(assumptions: set[AssumptionWrapper]) dataclass

Bases: Subset

Container class for minimal unsatisfiable subsets (MUS).

SatisfiableSubset(assumptions: set[AssumptionWrapper]) dataclass

Bases: Subset

Container class for satisfiable subsets.

Subset(assumptions: set[AssumptionWrapper]) dataclass

Bases: ABC

Container class for different types for subsets.

assumptions_string: str property

A rendered string representation of the assumptions.

symbol_strings: set[str] property

A set of rendered string representation of the assumption symbols.

__iter__() -> Iterator[tuple[clingo.Symbol, bool] | int]

Iterate of the assumption symbols.

__str__() -> str

Return a string representation of the subset.

iter_literals() -> Iterator[int]

Iterate over all assumption literals in the unsatisfiable subset.

iter_symbols() -> Iterator[tuple[clingo.Symbol, bool]]

Iterate over all assumption symbols in the unsatisfiable subset.

UnsatisfiableSubset(assumptions: set[AssumptionWrapper]) dataclass

Bases: Subset

Container class for unsatisfiable subsets.

render_assumption(assumption: AssumptionWrapper) -> str

Render assumption in text format.

PARAMETER	DESCRIPTION
assumption	The assumption to be rendered. TYPE: AssumptionWrapper

RETURNS	DESCRIPTION
The rendered assumption string.

render_assumption_set(assumptions: set[AssumptionWrapper]) -> str

Render assumptions in text format.

PARAMETER	DESCRIPTION
assumptions	A set of assumption to be rendered. TYPE: set[AssumptionWrapper]

RETURNS	DESCRIPTION
The rendered assumptions string.

utils

Utilities for the MUS functionality of clingexplaid.

AssumptionWrapper(literal: int, symbol: Symbol, sign: bool) dataclass

Container class for assumptions.

__hash__() -> int

Return self.literal for hashing.

unwrap(wrapped: Iterable[AssumptionWrapper]) -> set[int]

Unwrap an iterable sequence of assumptions into its set of literals.

Functionality for Unsat Constraints.

__all__ = ['UnsatConstraintComputer'] module-attribute

UnsatConstraintComputer(control: clingo.Control | None = None)

Computes the constraints of an unsatisfiable program that are the cause for the unsatisfiability.

Construct an UnsatConstraintComputer with the given control object.

PARAMETER	DESCRIPTION
control	The clingo control object. TYPE: Control | None DEFAULT: None

get_constraint_location(constraint_id: int) -> Location | None

Return the location of the constraint with constraint_id.

get_unsat_constraints(assumption_string: str | None = None) -> dict[int, str]

Return the unsatisfiable constraints of the initialized UnsatConstraintComputer.

parse_files(files: Sequence[str]) -> None

Initialize the UnsatConstraintComputer with a list of program.

parse_string(program_string: str) -> None

Initialize the UnsatConstraintComputer with a program string.

constants

Constant definitions for the unsat_constraints package.

unsat_constraint_computer

Unsat Constraint Utilities.

UnsatConstraintComputer(control: clingo.Control | None = None)

Computes the constraints of an unsatisfiable program that are the cause for the unsatisfiability.

Construct an UnsatConstraintComputer with the given control object.

PARAMETER	DESCRIPTION
control	The clingo control object. TYPE: Control | None DEFAULT: None

get_constraint_location(constraint_id: int) -> Location | None

Return the location of the constraint with constraint_id.

get_unsat_constraints(assumption_string: str | None = None) -> dict[int, str]

Return the unsatisfiable constraints of the initialized UnsatConstraintComputer.

parse_files(files: Sequence[str]) -> None

Initialize the UnsatConstraintComputer with a list of program.

parse_string(program_string: str) -> None

Initialize the UnsatConstraintComputer with a program string.