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 constraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal constraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
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 intended for users dealing with SAT solvers as black boxes.
org.sat4j.tools	Tools to be used on top of an ISolver.
org.sat4j.tools.encoding	Implementation of different encodings.
org.sat4j.tools.xplain	Implementation of an explanation engine in case of unsatisfiability.

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

IConstr
The most general abstraction for handling a constraint.

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.

ISolverService
The aim on that interface is to allow power users to communicate with the SAT solver using Dimacs format.

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

ISolverService
The aim on that interface is to allow power users to communicate with the SAT solver using Dimacs format.

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.

ISolverService
The aim on that interface is to allow power users to communicate with the SAT solver using Dimacs format.

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.encoding

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

IConstr
The most general abstraction for handling a constraint.

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