Package org.sat4j.tools.xplain

Implementation of an explanation engine in case of unsatisfiability.

See: Description

Interface Summary

Interface	Description
Explainer
MinimizationStrategy	Minimization technique used to reduce an unsatisfiable set of constraints into a minimally unsatisfiable subformula (MUS).

Class Summary

Class	Description
DeletionStrategy	An implementation of the deletion based minimization.
HighLevelXplain<T extends ISolver>	Computation of MUS in a structured CNF, i.e. the clauses belong to components, the explanation is to be extracted in terms of components.
InsertionStrategy	An implementation of the ReplayXplain algorithm as explained by Ulrich Junker in the following paper:
QuickXplain2001Strategy	An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:
QuickXplainStrategy	An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:
Xplain<T extends ISolver>	Explanation framework for SAT4J.

Package org.sat4j.tools.xplain Description

Implementation of an explanation engine in case of unsatisfiability.