Uses of Package
org.sat4j.specs

Packages that use org.sat4j.specs

org.sat4j	Contains a command line launcher for the SAT solvers.
org.sat4j.core	Implementation of the data structures available in org.sat4j.specs.
org.sat4j.minisat	Implementation of the MiniSAT specification in Java.
org.sat4j.minisat.constraints	Implementations of various constraints for MiniSAT.
org.sat4j.minisat.constraints.card	Implementations of cardinality contraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal contraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.uip	Various ways to compute an asserting clause (containing one Unique Implication Point).
org.sat4j.opt	Built-in optimization framework.
org.sat4j.reader	Some utility classes to read problems from plain text files.
org.sat4j.specs	Those classes are intented for users dealing with SAT solvers as blackboxes.
org.sat4j.tools	Tools to be used on top of an ISolver.
org.sat4j.tools.xplain

Classes in org.sat4j.specs used by org.sat4j

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IProblem
Access to the information related to a given problem instance.

ISolver
This interface contains all services provided by a SAT solver.

TimeoutException
Exception launched when the solver cannot solve a problem within its allowed time.

Classes in org.sat4j.specs used by org.sat4j.core

ISolver
This interface contains all services provided by a SAT solver.

IteratorInt
Iterator interface to avoid boxing int into Integer.

IVec
An abstraction on the type of vector used in the library.

IVecInt
An abstraction for the vector of int used on the library.

Classes in org.sat4j.specs used by org.sat4j.minisat

ISolver
This interface contains all services provided by a SAT solver.

Classes in org.sat4j.specs used by org.sat4j.minisat.constraints

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IVec
An abstraction on the type of vector used in the library.

IVecInt
An abstraction for the vector of int used on the library.

Classes in org.sat4j.specs used by org.sat4j.minisat.constraints.card

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IConstr
The most general abstraction for handling a constraint.

IVecInt
An abstraction for the vector of int used on the library.

Classes in org.sat4j.specs used by org.sat4j.minisat.constraints.cnf

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IConstr
The most general abstraction for handling a constraint.

IVec
An abstraction on the type of vector used in the library.

IVecInt
An abstraction for the vector of int used on the library.

Classes in org.sat4j.specs used by org.sat4j.minisat.core

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IConstr
The most general abstraction for handling a constraint.

IProblem
Access to the information related to a given problem instance.

ISolver
This interface contains all services provided by a SAT solver.

IVec
An abstraction on the type of vector used in the library.

IVecInt
An abstraction for the vector of int used on the library.

Lbool
That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.

SearchListener
Interface to the solver main steps.

TimeoutException
Exception launched when the solver cannot solve a problem within its allowed time.

Classes in org.sat4j.specs used by org.sat4j.minisat.uip

IConstr
The most general abstraction for handling a constraint.

Classes in org.sat4j.specs used by org.sat4j.opt

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IConstr
The most general abstraction for handling a constraint.

IOptimizationProblem
Represents an optimization problem.

IProblem
Access to the information related to a given problem instance.

ISolver
This interface contains all services provided by a SAT solver.

IVecInt
An abstraction for the vector of int used on the library.

TimeoutException
Exception launched when the solver cannot solve a problem within its allowed time.

Classes in org.sat4j.specs used by org.sat4j.reader

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IProblem
Access to the information related to a given problem instance.

ISolver
This interface contains all services provided by a SAT solver.

IVecInt
An abstraction for the vector of int used on the library.

Classes in org.sat4j.specs used by org.sat4j.specs

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IConstr
The most general abstraction for handling a constraint.

IProblem
Access to the information related to a given problem instance.

IteratorInt
Iterator interface to avoid boxing int into Integer.

IVec
An abstraction on the type of vector used in the library.

IVecInt
An abstraction for the vector of int used on the library.

Lbool
That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.

SearchListener
Interface to the solver main steps.

TimeoutException
Exception launched when the solver cannot solve a problem within its allowed time.

Classes in org.sat4j.specs used by org.sat4j.tools

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IConstr
The most general abstraction for handling a constraint.

IOptimizationProblem
Represents an optimization problem.

IProblem
Access to the information related to a given problem instance.

ISolver
This interface contains all services provided by a SAT solver.

IVec
An abstraction on the type of vector used in the library.

IVecInt
An abstraction for the vector of int used on the library.

SearchListener
Interface to the solver main steps.

TimeoutException
Exception launched when the solver cannot solve a problem within its allowed time.

Classes in org.sat4j.specs used by org.sat4j.tools.xplain

ContradictionException
That exception is launched whenever a trivial contradiction is found (e.g.

IConstr
The most general abstraction for handling a constraint.

IProblem
Access to the information related to a given problem instance.

ISolver
This interface contains all services provided by a SAT solver.

IVecInt
An abstraction for the vector of int used on the library.

TimeoutException
Exception launched when the solver cannot solve a problem within its allowed time.