fuzzy_dl_owl2.fuzzydl.query.min.min_satisfiable_query

Calculates the minimal degree of satisfiability for a fuzzy concept using Mixed-Integer Linear Programming optimization.

Description

The software determines the lowest possible truth degree at which a specific fuzzy concept remains satisfiable within a given ontology, either in isolation or relative to a particular individual. By extending the standard satisfiability logic, it transforms the logical verification process into a mathematical optimization problem that minimizes a variable representing the satisfiability threshold. During execution, the system clones the underlying knowledge base to preserve the original state, activates dynamic blocking if existential quantifiers are present, and constructs a specific objective expression to guide the solver. The optimization process ultimately yields a non-negative solution representing the minimal degree, or signals an inconsistency if the ontology cannot be satisfied under the given constraints.

Classes

MinSatisfiableQuery

This class defines a query to retrieve the minimal degree to which a fuzzy concept is satisfiable, either in general or with respect to a specific individual. It functions by transforming the logical problem into an optimization task, minimizing a variable that represents the satisfiability threshold. To use this entity, instantiate it with a Concept and optionally an Individual, then pass a KnowledgeBase to the solve method. The execution process clones the knowledge base to prevent side effects, handles existential restrictions by enabling dynamic blocking, and returns the calculated minimal degree or a status indicating inconsistency.

Module Contents

UML Class Diagram for MinSatisfiableQuery

class MinSatisfiableQuery(c: fuzzy_dl_owl2.fuzzydl.concept.concept.Concept)

class MinSatisfiableQuery(c: fuzzy_dl_owl2.fuzzydl.concept.concept.Concept, a: fuzzy_dl_owl2.fuzzydl.individual.individual.Individual)

Bases: fuzzy_dl_owl2.fuzzydl.query.satisfiable_query.SatisfiableQuery

This class defines a query to retrieve the minimal degree to which a fuzzy concept is satisfiable, either in general or with respect to a specific individual. It functions by transforming the logical problem into an optimization task, minimizing a variable that represents the satisfiability threshold. To use this entity, instantiate it with a Concept and optionally an Individual, then pass a KnowledgeBase to the solve method. The execution process clones the knowledge base to prevent side effects, handles existential restrictions by enabling dynamic blocking, and returns the calculated minimal degree or a status indicating inconsistency.

__min_sat_query_init_1(c: fuzzy_dl_owl2.fuzzydl.concept.concept.Concept) → None

This method initializes the minimum satisfiability query object with a specific fuzzy concept intended for satisfiability testing. It delegates the core initialization logic to the parent class constructor, passing the provided concept to establish the internal state required for the query. This routine is part of the object’s construction lifecycle, ensuring that the query is properly configured to evaluate the logical consistency of the given concept.

Parameters:

c (Concept) – The fuzzy concept to be evaluated for satisfiability.

__min_sat_query_init_2(

c: fuzzy_dl_owl2.fuzzydl.concept.concept.Concept,

a: fuzzy_dl_owl2.fuzzydl.individual.individual.Individual,

) → None

Initializes the minimum satisfiability query by delegating to the superclass constructor with the provided concept and individual. This method sets up the internal state necessary to evaluate whether the concept is satisfiable with respect to the specific individual. It acts as a constructor variant that binds the concept and individual arguments to the query instance.

Parameters:

• c (Concept) – The fuzzy concept to be tested for satisfiability.

• a (Individual) – The individual entity used to evaluate the concept’s satisfiability.

__str__() → str

Returns a human-readable string representation of the satisfiability query, formatted to indicate the concept being evaluated. If an individual is associated with the query instance, the string includes the individual’s identifier in brackets. The output always concludes with a greater-than-or-equal-to symbol, suggesting a threshold or comparison context.

Returns:

A string representation of the object, formatted as a satisfiability query for the concept and optionally the individual.

Return type:

str

preprocess(kb: fuzzy_dl_owl2.fuzzydl.knowledge_base.KnowledgeBase) → None

Prepares the KnowledgeBase to handle the query by transforming it into an optimization problem and solving the resulting constraints. It first inspects the conclusion string for existential quantifiers, enabling dynamic blocking on the KnowledgeBase if specific patterns are found. A new semi-continuous variable is then introduced into the underlying MILP solver to serve as the objective target. The method updates the internal variable counter, sets the objective expression to minimize this new variable, and adds a constraint linking the negated conclusion to the variable’s degree. Finally, it triggers the immediate solving of the accumulated assertions.

Parameters:

kb (KnowledgeBase) – The KnowledgeBase object that encapsulates the MILP solver, manages variable and assertion state, and controls solving behavior.

solve(kb: fuzzy_dl_owl2.fuzzydl.knowledge_base.KnowledgeBase) → fuzzy_dl_owl2.fuzzydl.milp.solution.Solution

Attempts to solve the minimal satisfiable query by optimizing the provided knowledge base. The method modifies the input knowledge base by incrementing its binary variable counter and creates a clone of the base, optionally excluding the ABox based on configuration or the presence of a specific individual. If no individual is currently assigned, a new one is generated within the cloned context. The process involves solving the ABox (if applicable), preprocessing the data, and executing an optimization routine against the objective expression. The resulting solution value is enforced to be non-negative. In the event of an inconsistent ontology, the method catches the exception and returns a solution indicating inconsistency. Additionally, the method tracks and updates the internal timing statistics for the operation.

Parameters:

kb (KnowledgeBase) – The knowledge base defining the ontology and constraints for the optimization problem.

Returns:

A Solution object representing the optimal value found for the objective expression. If the ontology is inconsistent, returns a Solution indicating an inconsistent knowledge base. The solution value is guaranteed to be non-negative.

Return type:

Solution