| Package | Description |
|---|---|
| org.sat4j |
Contains a command line launcher for the SAT solvers.
|
| org.sat4j.maxsat |
MAXSAT and Weighted Max SAT framework.
|
| org.sat4j.opt |
Built-in optimization framework.
|
| org.sat4j.pb |
Implementations of pseudo boolean solvers
|
| org.sat4j.pb.tools |
Implementation of different tools for pseudo boolean solvers
|
| org.sat4j.sat.visu |
Implementation of different visualization for the remote control.
|
| org.sat4j.tools |
Tools to be used on top of an
ISolver. |
| org.sat4j.tools.xplain |
Implementation of an explanation engine in case of unsatisfiability.
|
| Class and Description |
|---|
| SolutionFoundListener
Allows the end user to react when a new solution is found.
|
| Class and Description |
|---|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| AbstractOutputSolver |
| DimacsStringSolver
Solver used to write down a CNF into a String.
|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| AbstractClauseSelectorSolver |
| ClausalCardinalitiesDecorator
A decorator for clausal cardinalities constraints.
|
| FullClauseSelectorSolver |
| LexicoDecorator |
| ManyCore
A class allowing to run several solvers in parallel.
|
| OutcomeListener
Simple interface to check the outcome of running a solver in parallel.
|
| SearchListenerAdapter |
| SolutionFoundListener
Allows the end user to react when a new solution is found.
|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| IVisualizationTool |
| Class and Description |
|---|
| AbstractClauseSelectorSolver |
| AbstractMinimalModel |
| AbstractOutputSolver |
| DimacsArrayReader
Very simple Dimacs array reader.
|
| IVisualizationTool |
| ModelIterator
That class allows to iterate through all the models (implicants) of a
formula.
|
| OutcomeListener
Simple interface to check the outcome of running a solver in parallel.
|
| SearchListenerAdapter |
| SolutionFoundListener
Allows the end user to react when a new solution is found.
|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| AbstractClauseSelectorSolver |
| FullClauseSelectorSolver |
| GroupClauseSelectorSolver |
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.