org.clafer.compiler

Class ClaferUnsat

java.lang.Object

org.clafer.compiler.ClaferUnsat

public class ClaferUnsat
extends Object

Either call minUnsat() xor unsatCore() at most once. If you need to invoke both, you need to two ClaferUnsat objects.

Author:

jimmy

Method Summary

Methods

Modifier and Type	Method and Description
solver.Solver	getInternalSolver()
Pair<Set<AstConstraint>,InstanceModel>	minUnsat() Compute the minimal set of constraints that need to be removed before the model is satisfiable.
Set<AstConstraint>	unsatCore() Compute a small set of constraints that are mutually unsatisfiable.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

getInternalSolver

public solver.Solver getInternalSolver()

minUnsat

public Pair<Set<AstConstraint>,InstanceModel> minUnsat()

Compute the minimal set of constraints that need to be removed before the model is satisfiable. If the model is already satisfiable, then the set is empty. Guaranteed to be minimum.

Returns:

the Min-Unsat and the corresponding near-miss example or null if unknown

unsatCore

public Set<AstConstraint> unsatCore()

Compute a small set of constraints that are mutually unsatisfiable. Undefined behaviour if the model is satisfiable. This method is always slower to compute than minUnsat(). Not guaranteed to be minimum.

Returns:

the Unsat-Core or null if unknown