Modifier and Type | Class and Description |
---|---|
class |
BasicLauncher<T extends ISolver>
Very simple launcher, to be used during the SAT competition or the SAT race
for instance.
|
Modifier and Type | Field and Description |
---|---|
protected ISolver |
AbstractLauncher.solver |
Modifier and Type | Method and Description |
---|---|
protected <T extends ISolver> |
AbstractLauncher.showAvailableSolvers(ASolverFactory<T> afactory) |
protected <T extends ISolver> |
AbstractLauncher.showAvailableSolvers(ASolverFactory<T> afactory,
java.lang.String framework) |
Modifier and Type | Method and Description |
---|---|
protected abstract ISolver |
AbstractLauncher.configureSolver(java.lang.String[] args) |
protected ISolver |
BasicLauncher.configureSolver(java.lang.String[] args) |
protected ISolver |
MUSLauncher.configureSolver(java.lang.String[] args) |
ISolver |
LightFactory.defaultSolver() |
ISolver |
LightFactory.lightSolver() |
Modifier and Type | Method and Description |
---|---|
protected abstract Reader |
AbstractLauncher.createReader(ISolver theSolver,
java.lang.String problemname) |
protected Reader |
BasicLauncher.createReader(ISolver theSolver,
java.lang.String problemname) |
protected Reader |
MUSLauncher.createReader(ISolver theSolver,
java.lang.String problemname) |
void |
ILauncherMode.displayResult(ISolver solver,
IProblem problem,
ILogAble logger,
java.io.PrintWriter out,
Reader reader,
long beginTime,
boolean displaySolutionLine)
Output of the launcher when the solver stops
|
Modifier and Type | Class and Description |
---|---|
class |
ASolverFactory<T extends ISolver>
A solver factory is responsible for providing prebuilt solvers to the end
user.
|
Modifier and Type | Method and Description |
---|---|
void |
ConstrGroup.removeFrom(ISolver solver) |
Modifier and Type | Method and Description |
---|---|
ISolver |
SolverFactory.defaultSolver() |
ISolver |
SolverFactory.lightSolver() |
static ISolver |
SolverFactory.newDefault()
Default solver of the SolverFactory.
|
static ISolver |
SolverFactory.newDimacsOutput() |
static ISolver |
SolverFactory.newLight()
Small footprint SAT solver.
|
static ISolver |
SolverFactory.newMinOneSolver() |
static ISolver |
SolverFactory.newParallel() |
static ISolver |
SolverFactory.newSATUNSAT()
Two solvers are running in //: one for solving SAT instances, the other
one for solving unsat instances.
|
static ISolver |
SolverFactory.newStatistics() |
Modifier and Type | Interface and Description |
---|---|
interface |
ICDCL<D extends DataStructureFactory>
Abstraction for Conflict Driven Clause Learning Solver.
|
Modifier and Type | Class and Description |
---|---|
class |
Solver<D extends DataStructureFactory>
The backbone of the library providing the modular implementation of a MiniSAT
(Chaff) like solver.
|
Modifier and Type | Method and Description |
---|---|
ISolver |
Solver.getSolvingEngine() |
Modifier and Type | Class and Description |
---|---|
class |
AbstractSelectorVariablesDecorator
Abstract class which adds a new "selector" variable for each clause entered
in the solver.
|
class |
MaxSatDecorator
Computes a solution that satisfies the maximum of clauses.
|
class |
MinOneDecorator
Computes a solution with the smallest number of satisfied literals.
|
Constructor and Description |
---|
AbstractSelectorVariablesDecorator(ISolver solver) |
MaxSatDecorator(ISolver solver) |
MaxSatDecorator(ISolver solver,
boolean equivalence) |
MinOneDecorator(ISolver solver) |
Modifier and Type | Interface and Description |
---|---|
interface |
IPBSolver
A solver able to deal with pseudo boolean constraints.
|
Modifier and Type | Class and Description |
---|---|
class |
ConstraintRelaxingPseudoOptDecorator |
class |
LPStringSolver
Solver used to display in a string the pb-instance in OPB format.
|
class |
OPBStringSolver
Solver used to display in a string the pb-instance in OPB format.
|
class |
OptToPBSATAdapter
Utility class to use optimization solvers instead of simple SAT solvers in
code meant for SAT solvers.
|
class |
PBSolverDecorator
A decorator for the PB solvers.
|
class |
PseudoBitsAdderDecorator
A decorator that computes minimal pseudo boolean models.
|
class |
PseudoIteratorDecorator
A decorator that computes all pseudo boolean models.
|
class |
PseudoOptDecorator
A decorator that computes minimal pseudo boolean models.
|
class |
UserFriendlyPBStringSolver<T>
Solver to display SAT instances using domain objects names instead of Dimacs
numbers.
|
Modifier and Type | Method and Description |
---|---|
protected ISolver |
LanceurPseudo2005.configureSolver(java.lang.String[] args) |
protected ISolver |
LanceurPseudo2007Eclipse.configureSolver(java.lang.String[] args) |
Modifier and Type | Method and Description |
---|---|
java.math.BigInteger |
ObjectiveFunction.calculateDegreeImplicant(ISolver solver)
Compute the degree of the objective function using a prime implicant.
|
protected Reader |
LanceurPseudo2005.createReader(ISolver theSolver,
java.lang.String problemname) |
protected Reader |
LanceurPseudo2007.createReader(ISolver theSolver,
java.lang.String problemname) |
protected Reader |
LanceurPseudo2007Eclipse.createReader(ISolver theSolver,
java.lang.String problemname) |
Modifier and Type | Interface and Description |
---|---|
interface |
IPBCDCLSolver<D extends PBDataStructureFactory>
Abstraction for Conflict Driven Clause Learning PBSolver.
|
Modifier and Type | Class and Description |
---|---|
class |
ObjectiveReducerPBSolverDecorator |
class |
PBSolver |
class |
PBSolverCautious |
class |
PBSolverClause |
class |
PBSolverCP |
class |
PBSolverResCP |
class |
PBSolverResolution |
class |
PBSolverWithImpliedClause |
Modifier and Type | Method and Description |
---|---|
ISolver |
ObjectiveReducerPBSolverDecorator.getSolvingEngine() |
Modifier and Type | Class and Description |
---|---|
class |
ClausalConstraintsDecorator |
class |
LexicoDecoratorPB |
class |
ManyCorePB |
class |
PBAdapter
Allow to put a ISolver when an IPBSolver is required.
|
class |
SteppedTimeoutLexicoDecoratorPB |
class |
XplainPB |
Constructor and Description |
---|
PBAdapter(ISolver solver) |
Modifier and Type | Class and Description |
---|---|
class |
JSONReader<S extends ISolver>
Simple JSON reader for clauses and cardinality constraints.
|
Modifier and Type | Field and Description |
---|---|
protected ISolver |
DimacsReader.solver |
protected S |
JSONReader.solver |
Modifier and Type | Method and Description |
---|---|
protected ISolver |
DimacsReader.getSolver() |
ISolver |
JSONReader.parseString(java.lang.String json) |
Constructor and Description |
---|
DimacsReader(ISolver solver) |
DimacsReader(ISolver solver,
java.lang.String format) |
InstanceReader(ISolver solver) |
LecteurDimacs(ISolver s) |
Modifier and Type | Interface and Description |
---|---|
interface |
IGroupSolver
Represents a CNF in which clauses are grouped into levels.
|
Modifier and Type | Method and Description |
---|---|
ISolver |
ISolver.getSolvingEngine()
Retrieve the real engine in case the engine is decorated by one or
several decorator.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractClauseSelectorSolver<T extends ISolver> |
class |
ClausalCardinalitiesDecorator<T extends ISolver>
A decorator for clausal cardinalities constraints.
|
class |
FullClauseSelectorSolver<T extends ISolver> |
class |
GroupClauseSelectorSolver<T extends ISolver> |
class |
LexicoDecorator<T extends ISolver> |
class |
ManyCore<S extends ISolver>
A class allowing to run several solvers in parallel.
|
class |
NegationDecorator<T extends ISolver>
Negates the formula inside a solver.
|
class |
SolverDecorator<T extends ISolver>
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractClauseSelectorSolver<T extends ISolver> |
class |
AbstractMinimalModel |
class |
AbstractOutputSolver |
class |
ClausalCardinalitiesDecorator<T extends ISolver>
A decorator for clausal cardinalities constraints.
|
class |
DimacsOutputSolver
Solver used to display in a writer the CNF instance in Dimacs format.
|
class |
DimacsStringSolver
Solver used to write down a CNF into a String.
|
class |
FullClauseSelectorSolver<T extends ISolver> |
class |
GateTranslator
Utility class to easily feed a SAT solver using logical gates.
|
class |
GroupClauseSelectorSolver<T extends ISolver> |
class |
LexicoDecorator<T extends ISolver> |
class |
ManyCore<S extends ISolver>
A class allowing to run several solvers in parallel.
|
class |
Minimal4CardinalityModel
Computes models with a minimal number (with respect to cardinality) of
negative literals.
|
class |
Minimal4InclusionModel
Computes models with a minimal subset (with respect to set inclusion) of
negative literals.
|
class |
ModelIterator
That class allows to iterate through all the models (implicants) of a
formula.
|
class |
ModelIteratorToSATAdapter
This class allow to use the ModelIterator class as a solver.
|
class |
NegationDecorator<T extends ISolver>
Negates the formula inside a solver.
|
class |
OptToSatAdapter |
class |
SingleSolutionDetector
This solver decorator allows to detect whether or not the set of constraints
available in the solver has only one solution or not.
|
class |
SolutionCounter
Another solver decorator that counts the number of solutions.
|
class |
SolverDecorator<T extends ISolver>
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
class |
StatisticsSolver |
Modifier and Type | Field and Description |
---|---|
protected ISolver |
DimacsArrayReader.solver |
Modifier and Type | Method and Description |
---|---|
<T extends ISolver> |
AllMUSes.getSolverInstance()
Gets an instance of ISolver that can be used to compute all MUSes
|
Modifier and Type | Method and Description |
---|---|
protected ISolver |
DimacsArrayReader.getSolver() |
ISolver |
AbstractOutputSolver.getSolvingEngine() |
ISolver |
ManyCore.getSolvingEngine() |
ISolver |
SolverDecorator.getSolvingEngine() |
ISolver |
StatisticsSolver.getSolvingEngine() |
ISolver |
DimacsArrayReader.parseInstance(int[] gateType,
int[] outputs,
int[][] inputs,
int maxVar) |
Modifier and Type | Method and Description |
---|---|
static IVecInt |
RemiUtils.backbone(ISolver s)
Compute the set of literals common to all models of the formula.
|
static IVecInt |
Backbone.compute(ISolver solver)
Computes the backbone of a formula following the algorithm described in
João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of
Propositional Theories.
|
static IVecInt |
Backbone.compute(ISolver solver,
int[] implicant) |
static IVecInt |
Backbone.compute(ISolver solver,
int[] implicant,
IVecInt assumptions) |
static IVecInt |
Backbone.compute(ISolver solver,
IVecInt assumptions)
Computes the backbone of a formula following the algorithm described in
João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of
Propositional Theories.
|
static IVecInt |
AbstractMinimalModel.negativeLiterals(ISolver solver) |
static IVecInt |
AbstractMinimalModel.positiveLiterals(ISolver solver) |
Constructor and Description |
---|
AllMUSes(ASolverFactory<? extends ISolver> factory) |
AllMUSes(boolean group,
ASolverFactory<? extends ISolver> factory) |
CheckMUSSolutionListener(ASolverFactory<? extends ISolver> factory) |
Modifier and Type | Method and Description |
---|---|
IConstr |
EncodingStrategyAdapter.addAtLeast(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Policy.addAtLeast(ISolver solver,
IVecInt literals,
int n) |
IConstr |
EncodingStrategyAdapter.addAtLeastOne(ISolver solver,
IVecInt literals) |
IConstr |
Binary.addAtMost(ISolver solver,
IVecInt literals,
int k) |
IConstr |
Binomial.addAtMost(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Commander.addAtMost(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
EncodingStrategyAdapter.addAtMost(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Policy.addAtMost(ISolver solver,
IVecInt literals,
int k) |
IConstr |
Product.addAtMost(ISolver solver,
IVecInt literals,
int k) |
IConstr |
Sequential.addAtMost(ISolver solver,
IVecInt literals,
int k)
This encoding adds (n-1)*k variables (n is the number of variables in the
at most constraint and k is the degree of the constraint) and 2nk+n-3k-1
clauses.
|
IConstr |
Product.addAtMostNonOpt(ISolver solver,
IVecInt literals,
int k) |
IConstr |
Binary.addAtMostOne(ISolver solver,
IVecInt literals)
p being the smaller integer greater than log_2(n), this encoding adds p
variables and n*p clauses.
|
IConstr |
Binomial.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Commander.addAtMostOne(ISolver solver,
IVecInt literals)
In this encoding, variables are partitioned in groups.
|
IConstr |
EncodingStrategyAdapter.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Ladder.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Product.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Sequential.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Binary.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Binomial.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Commander.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
EncodingStrategyAdapter.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Policy.addExactly(ISolver solver,
IVecInt literals,
int n) |
IConstr |
Product.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Sequential.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Binary.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Binomial.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Commander.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
EncodingStrategyAdapter.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Ladder.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Product.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Sequential.addExactlyOne(ISolver solver,
IVecInt literals) |
Modifier and Type | Class and Description |
---|---|
class |
HighLevelXplain<T extends ISolver>
Computation of MUS in a structured CNF, i.e.
|
class |
Xplain<T extends ISolver>
Explanation framework for SAT4J.
|
Modifier and Type | Class and Description |
---|---|
class |
HighLevelXplain<T extends ISolver>
Computation of MUS in a structured CNF, i.e.
|
class |
Xplain<T extends ISolver>
Explanation framework for SAT4J.
|
Modifier and Type | Method and Description |
---|---|
IVecInt |
DeletionStrategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
IVecInt |
InsertionStrategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
IVecInt |
MinimizationStrategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
IVecInt |
QuickXplain2001Strategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
IVecInt |
QuickXplainStrategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |