Package | Description |
---|---|
org.sat4j.minisat.core |
Implementation of the MiniSAT solver skeleton.
|
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 . |
Modifier and Type | Method and Description |
---|---|
Lbool |
Solver.truthValue(int literal) |
Modifier and Type | Field and Description |
---|---|
static Lbool |
Lbool.FALSE |
static Lbool |
Lbool.TRUE |
static Lbool |
Lbool.UNDEFINED |
Modifier and Type | Method and Description |
---|---|
Lbool |
Lbool.not()
boolean negation.
|
Lbool |
ISolverService.truthValue(int literal)
To access the truth value of a specific literal under current assignment.
|
Modifier and Type | Method and Description |
---|---|
void |
SearchListener.end(Lbool result)
End the search.
|
Modifier and Type | Method and Description |
---|---|
void |
TextOutputTracing.end(Lbool result) |
void |
LearnedClauseSizeTracing.end(Lbool result) |
void |
DotSearchTracing.end(Lbool result) |
void |
SearchListenerAdapter.end(Lbool result) |
void |
DecisionTracing.end(Lbool result) |
void |
SpeedTracing.end(Lbool result) |
void |
SearchEnumeratorListener.end(Lbool result) |
void |
SearchMinOneListener.end(Lbool result) |
void |
LBDTracing.end(Lbool result) |
void |
RupSearchListener.end(Lbool result) |
void |
MultiTracing.end(Lbool result) |
void |
DecisionLevelTracing.end(Lbool result) |
void |
LearnedClausesSizeTracing.end(Lbool result) |
void |
ConflictDepthTracing.end(Lbool result) |
void |
ConflictLevelTracing.end(Lbool result) |
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.