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.csp	Classes needed for CSP to SAT translation.
org.sat4j.csp.constraints	Classes needed for CSP to SAT translation.
org.sat4j.csp.encodings
org.sat4j.maxsat	MAXSAT and Weighted Max SAT framework.
org.sat4j.maxsat.reader	Some utility classes to read problems from plain text files.
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.opt	Built-in optimization framework.
org.sat4j.pb
org.sat4j.pb.constraints
org.sat4j.pb.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.pb.core
org.sat4j.pb.reader
org.sat4j.pb.tools
org.sat4j.reader	Some utility classes to read problems from plain text files.
org.sat4j.sat
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.encoding
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.csp

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

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.

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

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

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

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

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

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

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

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

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

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.

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

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

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

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.

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

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.

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

Classes in org.sat4j.specs used by org.sat4j.pb.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.pb.constraints.pb

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

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

Classes in org.sat4j.specs used by org.sat4j.pb.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.

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

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

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.

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.

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.