Package org.sat4j.tools.xplain

Implementation of an explanation engine in case of unsatisfiability.

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:
Pair  
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.



Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.