Package org.jacop.satwrapper

Class SatTranslation

java.lang.Object
org.jacop.satwrapper.SatTranslation
public class SatTranslation extends Object
SatTranslation defines SAT clauses for typical logical constraints
Version:
4.10

  • Field Details

    • debug

      public boolean debug

    • clauses

      SatWrapper clauses

    • store

      Store store

    • numberClauses

      long numberClauses

  • Constructor Details

    • SatTranslation

      public SatTranslation(Store store)

  • Method Details

    • 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_xor

      public void generate_xor(IntVar a, IntVar b, IntVar c, IntVar d)

    • 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()

    • clauseToString

      String clauseToString(int[] clause)