org.jacop.satwrapper

## Class SatTranslation

• public class SatTranslation
extends Object
SatTranslation defines SAT clauses for typical logical constraints
Version:
4.9
Author:
Krzysztof Kuchcinski
• ### Field Detail

• #### debug

public boolean debug
• ### Constructor Detail

• #### SatTranslation

public SatTranslation(Store store)
• ### Method Detail

• #### generate_clause

public void generate_clause(IntVar[] a1,
IntVar[] a2)
• #### generate_clause_reif

public void generate_clause_reif(IntVar[] a,
IntVar[] b,
IntVar r)
• #### generate_or

public void generate_or(IntVar[] a,
IntVar c)
• #### generate_and

public void generate_and(IntVar[] a,
IntVar c)
• #### 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'ed
c - result
• #### generate_xor

public void generate_xor(IntVar a,
IntVar b,
IntVar c)
• #### generate_eq

public void generate_eq(IntVar a,
IntVar b)
• #### generate_le

public void generate_le(IntVar a,
IntVar b)
• #### generate_lt

public void generate_lt(IntVar a,
IntVar b)
• #### generate_eq_reif

public void generate_eq_reif(IntVar a,
IntVar b,
IntVar c)
• #### generate_neq_reif

public void generate_neq_reif(IntVar a,
IntVar b,
IntVar c)
• #### generate_le_reif

public void generate_le_reif(IntVar a,
IntVar b,
IntVar c)
• #### generate_lt_reif

public void generate_lt_reif(IntVar a,
IntVar b,
IntVar c)
• #### generate_not

public void generate_not(IntVar a,
IntVar b)
• #### generate_implication

public void generate_implication(IntVar a,
IntVar b)
• #### generate_implication_reif

public void generate_implication_reif(IntVar a,
IntVar b,
IntVar c)
• #### generate_allZero_reif

public void generate_allZero_reif(IntVar[] as,
IntVar c)
• #### impose

public void impose()
• #### numberClauses

public long numberClauses()