(this file is automatically generated from Java source)
Back to book index.
Satisfiablity (SAT) semi-datastructures and semi-algorithms :)
The support for SAT is currently minimal (heck, we don't even know if it is working :). Therefore, we will only present the existing APIs in this tutorial...
Lets just state that we are no experts on this subject. We have added these packages just in case you happen to be a SAT-guru...
Basic data structures
Skip this part if you don't care about the internal structure of the CNF formulas in JDD.
|
Class jdd.sat.Lit
|
| return type | method | parameters |
|
java.lang.String |
toString |
|
jdd.sat.Lit |
negate |
|
void |
showDIMACS |
|
void |
showSupport |
| Field | type |
|
Field id | public int jdd.sat.Lit.id
|
|
Field index | public int jdd.sat.Lit.index
|
|
Field bdd | public int jdd.sat.Lit.bdd
|
|
Field occurnece | public int jdd.sat.Lit.occurnece
|
|
Field extra | public int jdd.sat.Lit.extra
|
|
Field neg | public boolean jdd.sat.Lit.neg
|
|
Field var | public jdd.sat.Var jdd.sat.Lit.var
|
|
Class jdd.sat.Var
|
| return type | method | parameters |
|
java.lang.String |
toString |
|
boolean |
greater_than |
(
jdd.util.Sortable ) |
|
void |
showSupport |
| Field | type |
|
Field index | public int jdd.sat.Var.index
|
|
Field offset | public int jdd.sat.Var.offset
|
|
Field extra | public int jdd.sat.Var.extra
|
|
Field activity | public double jdd.sat.Var.activity
|
|
Field var | public jdd.sat.Lit jdd.sat.Var.var
|
|
Field negvar | public jdd.sat.Lit jdd.sat.Var.negvar
|
|
Field occurs | public java.util.Vector jdd.sat.Var.occurs
|
|
Class jdd.sat.Clause
|
| return type | method | parameters |
|
boolean |
equals |
(
jdd.sat.Clause ) |
|
boolean |
remove |
(
jdd.sat.Var ) |
|
void |
remove |
(
int ) |
|
void |
insert |
(
jdd.sat.Lit ) |
|
jdd.sat.Lit |
first |
|
boolean |
removed |
(
jdd.sat.Var ) |
|
boolean |
removed |
(
jdd.sat.Lit ) |
|
boolean |
active |
(
jdd.sat.Var ) |
|
boolean |
simplify |
|
void |
internal_test |
|
boolean |
greater_than |
(
jdd.util.Sortable ) |
|
void |
showDIMACS |
|
void |
showClause |
|
boolean |
satisfies |
(
int, boolean ) |
|
boolean |
satisfies |
(
boolean[] ) |
|
void |
removeFromDatabase |
|
boolean |
largerOrEquals |
(
jdd.sat.Clause ) |
|
boolean |
isNull |
|
boolean |
isUnit |
|
int |
litsRemoved |
|
boolean |
used |
(
jdd.sat.Lit ) |
|
void |
reinsert |
(
int ) |
|
boolean |
reinsert |
(
jdd.sat.Var ) |
| Field | type |
|
Field lits | public jdd.sat.Lit[] jdd.sat.Clause.lits
|
|
Field curr | public int jdd.sat.Clause.curr
|
|
Field num_lits | public int jdd.sat.Clause.num_lits
|
|
Field index | public int jdd.sat.Clause.index
|
|
Field flag | public int jdd.sat.Clause.flag
|
|
Field offset | public int jdd.sat.Clause.offset
|
|
Field top | public int jdd.sat.Clause.top
|
|
Field heat | public double jdd.sat.Clause.heat
|
|
Class jdd.sat.CNF
|
| return type | method | parameters |
|
void |
check |
|
void |
insert |
(
jdd.sat.Clause ) |
|
void |
order |
|
void |
internal_test |
|
void |
showDIMACS |
|
int |
satisfies |
(
int, boolean ) |
|
boolean |
satisfies |
(
boolean[] ) |
|
jdd.sat.CNF |
parseDimacsText |
(
java.lang.String ) |
|
jdd.sat.CNF |
loadDimacs |
(
java.lang.String ) |
|
jdd.sat.Lit |
getSignedLit |
(
int ) |
|
jdd.sat.Lit |
getLit |
(
int, boolean ) |
|
jdd.sat.Clause |
findLargerOrEqualClause |
(
jdd.sat.Clause ) |
|
void |
adjustNumClauses |
|
int |
conflicts |
(
boolean[] ) |
|
jdd.sat.Clause |
findEqualClause |
(
jdd.sat.Clause ) |
| Field | type |
|
Field clauses | public jdd.sat.Clause[] jdd.sat.CNF.clauses
|
|
Field lits | public jdd.sat.Lit[] jdd.sat.CNF.lits
|
|
Field vars | public jdd.sat.Var[] jdd.sat.CNF.vars
|
|
Field curr | public int jdd.sat.CNF.curr
|
|
Field num_clauses | public int jdd.sat.CNF.num_clauses
|
|
Field num_lits | public int jdd.sat.CNF.num_lits
|
Basic SAT solvers
The class Solver is the base class for all CNF solvers:
|
Class jdd.sat.Solver
|
| return type | method | parameters |
|
void |
setFormula |
(
jdd.sat.CNF ) |
|
int[] |
solve |
A solution is returned as a vector of integers (int []), where an value of 0 for position i means that variable i is assigned false, 1 means true and -1 means dont care.
The current solvers are:
|
Class jdd.sat.bdd.BDDSolver
|
| return type | method | parameters |
|
void |
setFormula |
(
jdd.sat.CNF ) |
|
int[] |
solve |
The BDD solver is very inefficient. The GSAT solver are better implemented, but , as we all know, they have some algorithmic weaknesses...
|
Class jdd.sat.gsat.GSATSolver
|
| return type | method | parameters |
|
void |
setFormula |
(
jdd.sat.CNF ) |
|
int[] |
solve |
|
Class jdd.sat.gsat.GSAT2Solver
|
| return type | method | parameters |
|
int[] |
solve |
These two performs so bad, they are not worth using anywhere...
|
Class jdd.sat.gsat.WalkSATSolver
|
| return type | method | parameters |
|
int[] |
solve |
|
Class jdd.sat.gsat.WalkSATSKCSolver
|
| return type | method | parameters |
|
int[] |
solve |
We just got this to work: the Davis/(Putnam)/Logeman/Loveland algorithm. There are no heuristics at all (except for random choices :), so don't expect this solver to solve your DAC'05 benchmarks or anything even remotely hard...
|
Class jdd.sat.dpll.DPLLSolver
|
| return type | method | parameters |
|
void |
setFormula |
(
jdd.sat.CNF ) |
|
int[] |
solve |
(we migh add a DP or CalcRes solver soon)
Misc. SAT stuff
You would never guess what this class does ;)
|
Class jdd.sat.DimacsReader
|
| return type | method | parameters |
|
jdd.sat.CNF |
getFormula |
Back to book index.