|
||||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | |||||||||
See:
Description
| Interface Summary | |
|---|---|
| Explainer | |
| MinimizationStrategy | Minimization technique used to reduce an unsatisfiable set of constraints into a minimally unsatisfiable subformula (MUS). |
| Class Summary | |
|---|---|
| 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. |
Implementation of an explanation engine in case of unsatisfiability.
|
||||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | |||||||||