Package org.sat4j.specs

Examples of org.sat4j.specs.IVecInt.clear()

178
179
180
181
182
183
184
185
186
187
188
        }
        solver.addClause(literals);

        /* Second term. */
        for (int i = 0; i < numberOfVertices; i++) {
          literals.clear();
          literals.push(-(i * colors + k));
          literals.push(numberOfVertices * colors + k);
          solver.addClause(literals);
        }
      }
View Full Code Here
195
196
197
198
199
200
201
202
203
204
205
        literals.push(-(numberOfVertices * colors + k));
        for (int i = 1; i < k; i++) {
          literals.push(numberOfVertices * colors + i);
          solver.addClause(literals);
        }
        literals.clear();
      }

      /* Objective function. */
      literals = new VecInt(colors);
      IVec<BigInteger> coefficients = new Vec<BigInteger>(colors);
View Full Code Here
276
277
278
279
280
281
282
283
284
285
286
    /* Precolor vertex v with maximum degree with first color. */
    V v = Collections.max(vertices, c);
    IVecInt literals = new VecInt(1);
    literals.push(vertices.indexOf(v) * colors + 1);
    solver.addClause(literals);
    literals.clear();

    /* Precolor neighbor of v with maximum degree with second color. */
    Collection<V> neighbors = graph.getNeighbors(v);
    if (!neighbors.isEmpty()) {
      v = Collections.max(neighbors, c);
View Full Code Here
105
106
107
108
109
110
111
112
113
114
115
                token = stk.nextToken();

                if ("<=".equals(token) || ">=".equals(token)) {
                    // on est sur une contrainte de cardinalit?
                    readCardinalityConstr(token, stk, literals);
                    literals.clear();
                    realNbOfClauses++;
                } else {
                    lit = Integer.parseInt(token);
                    if (lit == 0) {
                        if (literals.size() > 0) {
View Full Code Here
112
113
114
115
116
117
118
119
120
121
122
                } else {
                    lit = Integer.parseInt(token);
                    if (lit == 0) {
                        if (literals.size() > 0) {
                            solver.addClause(literals);
                            literals.clear();
                            realNbOfClauses++;
                        }
                    } else {
                        literals.push(lit);
                    }
View Full Code Here
170
171
172
173
174
175
176
177
178
179
180
                val = (val * 10) + car - '0';
                car = (char) in.read();
            }
            if (val == 0) { // on a lu toute la clause
                s.addClause(lit);
                lit.clear();
            } else {
                /* on ajoute le literal au vecteur */
                // s.newVar(val-1);
                lit.push(neg ? -val : val);
                neg = false;
View Full Code Here
85
86
87
88
89
90
91
92
93
94
95
        IVecInt clause = new VecInt(5);
        // y <=> (x1 -> x2) and (not x1 -> x3)
        // y -> (x1 -> x2) and (not x1 -> x3)
        clause.push(-y).push(-x1).push(x2);
        processClause(clause);
        clause.clear();
        clause.push(-y).push(x1).push(x3);
        processClause(clause);
        // y <- (x1 -> x2) and (not x1 -> x3)
        // not(x1 -> x2) or not(not x1 -> x3) or y
        // x1 and not x2 or not x1 and not x3 or y
View Full Code Here
95
96
97
98
99
100
101
102
103
104
105
        // x1 and not x2 or not x1 and not x3 or y
        // (x1 and not x2) or ((not x1 or y) and (not x3 or y))
        // (x1 or not x1 or y) and (not x2 or not x1 or y) and (x1 or not x3 or
        // y) and (not x2 or not x3 or y)
        // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
        clause.clear();
        clause.push(-x1).push(-x2).push(y);
        processClause(clause);
        clause.clear();
        clause.push(x1).push(-x3).push(y);
        processClause(clause);
View Full Code Here
98
99
100
101
102
103
104
105
106
107
108
        // y) and (not x2 or not x3 or y)
        // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
        clause.clear();
        clause.push(-x1).push(-x2).push(y);
        processClause(clause);
        clause.clear();
        clause.push(x1).push(-x3).push(y);
        processClause(clause);
        clause.clear();
        clause.push(-x2).push(-x3).push(y);
        processClause(clause);
View Full Code Here
101
102
103
104
105
106
107
108
109
110
111
        clause.push(-x1).push(-x2).push(y);
        processClause(clause);
        clause.clear();
        clause.push(x1).push(-x3).push(y);
        processClause(clause);
        clause.clear();
        clause.push(-x2).push(-x3).push(y);
        processClause(clause);
        // taken from Niklas Een et al SAT 2007 paper
        // Adding the following redundant clause will improve unit propagation
        // y -> x2 or x3
View Full Code Here
TOP
Copyright © 2018 www.massapi.com. All rights reserved.
All source code are property of their respective owners. Java is a trademark of Sun Microsystems, Inc and owned by ORACLE Inc. Contact coftware#gmail.com.