Class SatTranslation


  • public class SatTranslation
    extends java.lang.Object
    SatTranslation defines SAT clauses for typical logical constraints
    Version:
    4.7
    • Field Detail

      • debug

        public boolean debug
      • numberClauses

        long numberClauses
    • 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_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_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

        java.lang.String clauseToString​(int[] clause)