org.sat4j.specs

Interface IGroupSolver

All Superinterfaces:

IProblem, ISolver, RandomAccessModel, Serializable

All Known Implementing Classes:

GroupClauseSelectorSolver, HighLevelXplain

public interface IGroupSolver
extends ISolver

Represents a CNF in which clauses are grouped into levels. It was first used to build a high level MUS solver for SAT 2011 competition.

Since:

2.3.3

Author:

leberre

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addClause(IVecInt literals, int desc)

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

Method Detail

addClause

IConstr addClause(IVecInt literals,
                int desc)
                  throws ContradictionException

Parameters:

literals - a clause

desc - the level of the clause set

Returns:

on object representing that clause in the solver.

Throws:

ContradictionException