Package org.sat4j.pb

Examples of org.sat4j.pb.IPBSolver


    long deadline = Longs.saturatedAdd(System.currentTimeMillis(),
        TimeUnit.MILLISECONDS.convert(timeout, unit));

    /* Create solver. */
    IPBSolver solver = new PseudoOptDecorator(SolverFactory.newDefault());

    try {
      List<V> vertices = new ArrayList<V>(graph.vertexSet());
      Collections.sort(vertices);
      int numberOfVertices = vertices.size();

      /* Indicator variables and variables for tracking used colors. */
      int indicatorVars = numberOfVertices * colors;
      solver.newVar(indicatorVars + colors);

      /* PB constraints to enforce assignment of exactly one color. */
      for (int i = 0; i < numberOfVertices; i++) {
        IVecInt literals = new VecInt(colors);
        IVec<BigInteger> coefficients = new Vec<BigInteger>(colors);
        for (int j = 1; j <= colors; j++) {
          literals.push(i * colors + j);
          coefficients.push(BigInteger.ONE);
        }
        solver.addPseudoBoolean(literals, coefficients, false,
            BigInteger.ONE);
        solver.addPseudoBoolean(literals, coefficients, true,
            BigInteger.ONE);
      }

      /*
       * CNF constraints enforcing that no adjacent vertices have the same
       * color.
       */
      for (int i = 0; i < vertices.size(); i++) {
        V u = vertices.get(i);
        for (int j = 0; j < vertices.size(); j++) {
          V v = vertices.get(j);
          if (graph.containsEdge(u, v)) {
            for (int k = 1; k <= colors; k++) {
              IVecInt literals = new VecInt(2);
              literals.push(-(i * colors + k));
              literals.push(-(j * colors + k));
              solver.addClause(literals);
            }
          }
        }
      }

      /*
       * CNF constraints (derived from propositional logic expression) to
       * set track variable, if a color has been assigned to one of the
       * indicator variables for a given bundle.
       */
      for (int k = 1; k <= colors; k++) {
        /* First term. */
        IVecInt literals = new VecInt(numberOfVertices + 1);
        literals.push(-(numberOfVertices * colors + k));
        for (int i = 0; i < numberOfVertices; i++) {
          literals.push(i * colors + k);
        }
        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);
        }
      }

      /* Symmetry breaking. */
      selectiveColoring(colors, solver, vertices);

      IVecInt literals = new VecInt(2);
      for (int k = 1; k <= colors; k++) {
        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);
      for (int k = 1; k <= colors; k++) {
        literals.push(numberOfVertices * colors + k);
        coefficients.push(BigInteger.ONE);
      }
      ObjectiveFunction objFunc = new ObjectiveFunction(literals,
          coefficients);
      solver.setObjectiveFunction(objFunc);

      /* Solve */
      IOptimizationProblem op = (IOptimizationProblem) solver;
      int[] model = null;
      try {
        if (deadline != Long.MAX_VALUE) {
          solver.setTimeoutMs(deadline - System.currentTimeMillis());
        }
        long stepref = System.nanoTime();
        while (System.currentTimeMillis() < deadline
            && !Thread.currentThread().isInterrupted()
            && op.admitABetterSolution()) {
          model = solver.model();
          GraphColoring<V, E> coloring = this.getColoring(colors,
              vertices, numberOfVertices, model);
          long now = System.nanoTime();
          LOGGER.debug(
              "solution found with {} colors and objective value {} in {}/{} ns",
              new Object[] { coloring.getNumberOfColors(),
                  op.getObjectiveValue(), now - stepref,
                  now - baseref });
          if (listener != null) {
            listener.handle(this, coloring);
          }
          op.discardCurrentSolution();
          stepref = System.nanoTime();
          long nextTO = Math.max(0,
              deadline - System.currentTimeMillis());
          solver.setTimeoutMs(nextTO);
          LOGGER.debug("timeout set to {} ms", nextTO);
        }
      } catch (ContradictionException ce) {
        /*
         * Raised by discardCurrentSolution, but we may have found a
View Full Code Here

TOP

Related Classes of org.sat4j.pb.IPBSolver

Copyright © 2018 www.massapicom. 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.