Package org.jacop.satwrapper
Class SatTranslation
java.lang.Object
org.jacop.satwrapper.SatTranslation
SatTranslation defines SAT clauses for typical logical constraints
- Version:
- 4.8
-
Field Summary
FieldsModifier and TypeFieldDescription(package private) SatWrapper
boolean
(package private) long
(package private) Store
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescription(package private) 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
-
Field Details
-
debug
public boolean debug -
clauses
SatWrapper clauses -
store
Store store -
numberClauses
long numberClauses
-
-
Constructor Details
-
SatTranslation
-
-
Method Details
-
generate_clause
-
generate_clause_reif
-
generate_or
-
generate_and
-
generate_xor
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
-
generate_xor
-
generate_xor
-
generate_eq
-
generate_le
-
generate_lt
-
generate_eq_reif
-
generate_neq_reif
-
generate_le_reif
-
generate_lt_reif
-
generate_not
-
generate_implication
-
generate_implication_reif
-
generate_allZero_reif
-
impose
public void impose() -
numberClauses
public long numberClauses() -
clauseToString
-