Package org.jacop.satwrapper
Class SatTranslation
- java.lang.Object
-
- org.jacop.satwrapper.SatTranslation
-
public class SatTranslation extends java.lang.Object
SatTranslation defines SAT clauses for typical logical constraints- Version:
- 4.7
-
-
Field Summary
Fields Modifier and Type Field Description (package private) SatWrapper
clauses
boolean
debug
(package private) long
numberClauses
(package private) Store
store
-
Constructor Summary
Constructors Constructor Description SatTranslation(Store store)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description (package private) java.lang.String
clauseToString(int[] clause)
void
generate_allZero_reif(IntVar[] as, IntVar c)
void
generate_and(IntVar[] a, IntVar c)
void
generate_clause(IntVar[] a1, IntVar[] a2)
void
generate_clause_reif(IntVar[] a, IntVar[] b, IntVar r)
void
generate_eq(IntVar a, IntVar b)
void
generate_eq_reif(IntVar a, IntVar b, IntVar c)
void
generate_implication(IntVar a, IntVar b)
void
generate_implication_reif(IntVar a, IntVar b, IntVar c)
void
generate_le(IntVar a, IntVar b)
void
generate_le_reif(IntVar a, IntVar b, IntVar c)
void
generate_lt(IntVar a, IntVar b)
void
generate_lt_reif(IntVar a, IntVar b, IntVar c)
void
generate_neq_reif(IntVar a, IntVar b, IntVar c)
void
generate_not(IntVar a, IntVar b)
void
generate_or(IntVar[] a, IntVar c)
void
generate_xor(IntVar[] a, IntVar c)
To represent XOR function in CNF one needs to have 2^{n-1} clauses, where n is the size of your XOR function :( Our method cuts list to 3 or 2 element parts, generates XOR for them and composesd them back to the original XOR.void
generate_xor(IntVar a, IntVar b, IntVar c)
void
generate_xor(IntVar a, IntVar b, IntVar c, IntVar d)
void
impose()
long
numberClauses()
-
-
-
Field Detail
-
debug
public boolean debug
-
clauses
SatWrapper clauses
-
store
Store store
-
numberClauses
long numberClauses
-
-
Constructor Detail
-
SatTranslation
public SatTranslation(Store store)
-
-
Method Detail
-
generate_xor
public void generate_xor(IntVar[] a, IntVar c)
To represent XOR function in CNF one needs to have 2^{n-1} clauses, where n is the size of your XOR function :( Our method cuts list to 3 or 2 element parts, generates XOR for them and composesd them back to the original XOR. Further improvements possible, if using 4-7 decompositions.- Parameters:
a
- parameters to be xor'edc
- result
-
impose
public void impose()
-
numberClauses
public long numberClauses()
-
clauseToString
java.lang.String clauseToString(int[] clause)
-
-