opb_reader.h 4.49 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

#ifndef OR_TOOLS_SAT_OPB_READER_H_
#define OR_TOOLS_SAT_OPB_READER_H_

#include <algorithm>
#include <memory>
#include <string>
#include <vector>

#include "absl/strings/numbers.h"
#include "absl/strings/str_split.h"
#include "ortools/base/filelineiter.h"
#include "ortools/base/logging.h"
#include "ortools/base/macros.h"
#include "ortools/sat/boolean_problem.pb.h"

namespace operations_research {
namespace sat {

// This class loads a file in pbo file format into a LinearBooleanProblem.
// The format is described here:
//   http://www.cril.univ-artois.fr/PB12/format.pdf
class OpbReader {
 public:
  OpbReader() {}

  // Loads the given opb filename into the given problem.
  bool Load(const std::string& filename, LinearBooleanProblem* problem) {
    problem->Clear();
    problem->set_name(ExtractProblemName(filename));

    num_variables_ = 0;
    int num_lines = 0;
    for (const std::string& line : FileLines(filename)) {
      ++num_lines;
      ProcessNewLine(problem, line);
    }
    if (num_lines == 0) {
      LOG(FATAL) << "File '" << filename << "' is empty or can't be read.";
    }
    problem->set_num_variables(num_variables_);
    return true;
  }

 private:
  // Since the problem name is not stored in the cnf format, we infer it from
  // the file name.
  static std::string ExtractProblemName(const std::string& filename) {
    const int found = filename.find_last_of("/");
    const std::string problem_name =
        found != std::string::npos ? filename.substr(found + 1) : filename;
    return problem_name;
  }

  void ProcessNewLine(LinearBooleanProblem* problem, const std::string& line) {
    const std::vector<std::string> words =
        absl::StrSplit(line, absl::ByAnyChar(" ;"), absl::SkipEmpty());
    if (words.empty() || words[0].empty() || words[0][0] == '*') {
      return;
    }

    if (words[0] == "min:") {
      LinearObjective* objective = problem->mutable_objective();
      for (int i = 1; i < words.size(); ++i) {
        const std::string& word = words[i];
        if (word.empty() || word[0] == ';') continue;
        if (word[0] == 'x') {
          int literal;
          CHECK(absl::SimpleAtoi(word.substr(1), &literal));
          num_variables_ = std::max(num_variables_, literal);
          objective->add_literals(literal);
        } else {
          int64 value;
          CHECK(absl::SimpleAtoi(word, &value));
          objective->add_coefficients(value);
        }
      }
      if (objective->literals_size() != objective->coefficients_size()) {
        LOG(INFO) << "words.size() = " << words.size();
        LOG(FATAL) << "Failed to parse objective:\n " << line;
      }
      return;
    }
    LinearBooleanConstraint* constraint = problem->add_constraints();
    for (int i = 0; i < words.size(); ++i) {
      const std::string& word = words[i];
      CHECK(!word.empty());
      if (word == ">=") {
        CHECK_LT(i + 1, words.size());
        int64 value;
        CHECK(absl::SimpleAtoi(words[i + 1], &value));
        constraint->set_lower_bound(value);
        break;
      } else if (word == "=") {
        CHECK_LT(i + 1, words.size());
        int64 value;
        CHECK(absl::SimpleAtoi(words[i + 1], &value));
        constraint->set_upper_bound(value);
        constraint->set_lower_bound(value);
        break;
      } else {
        if (word[0] == 'x') {
          int literal;
          CHECK(absl::SimpleAtoi(word.substr(1), &literal));
          num_variables_ = std::max(num_variables_, literal);
          constraint->add_literals(literal);
        } else {
          int64 value;
          CHECK(absl::SimpleAtoi(words[i], &value));
          constraint->add_coefficients(value);
        }
      }
    }
    if (constraint->literals_size() != constraint->coefficients_size()) {
      LOG(FATAL) << "Failed to parse constraint:\n " << line;
    }
  }

  int num_variables_;
  DISALLOW_COPY_AND_ASSIGN(OpbReader);
};

}  // namespace sat
}  // namespace operations_research

#endif  // OR_TOOLS_SAT_OPB_READER_H_