Modifier and Type | Method and Description |
---|---|
Domain |
domain()
Return the domain of the evaluable.
|
void |
toClause(org.sat4j.specs.ISolver solver)
Translates a variable over a domain into a set a clauses enforcing that
exactly one value must be chosen in the domain.
|
int |
translate(int key)
Translates a value from the domain into a SAT variable in Dimacs format.
|
Domain domain()
int translate(int key)
key
- a value from domain()void toClause(org.sat4j.specs.ISolver solver) throws org.sat4j.specs.ContradictionException
solver
- a solver to feed with the clauses.org.sat4j.specs.ContradictionException
- if a trivial inconsistency is met.Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.