Google OR-Tools: ortools/sat/sat_cnf

Google OR-Tools: ortools/sat/sat_cnf_reader.h Source File

39 public:

47 problem_->set_num_variables(num_variables + num_slacks);

48 problem_->set_original_num_variables(num_variables);

49 for (const int c : to_postprocess_) {

50 auto* literals = problem_->mutable_constraints(c)->mutable_literals();

51 const int last_index = literals->size() - 1;

52 const int last = (*literals)[last_index];

53 (*literals)[last_index] =

54 last >= 0 ? last + num_variables : last - num_variables;

55 }

56 }

61 void AddConstraint(absl::Span<const int> clause, bool last_is_slack = false) {

62 if (last_is_slack)

63 to_postprocess_.push_back(problem_->constraints().size());

68 for (const int literal : clause) {

71 }

72 }

75 CHECK_GE(literal, 0) << "Negative literal not supported.";

76 problem_->mutable_objective()->add_literals(literal);

77 problem_->mutable_objective()->add_coefficients(value);

78 }

81 problem_->mutable_objective()->set_offset(offset);

82 }

84 private:

86 std::vector<int> to_postprocess_;

87};

91 public:

95 for (int i = 0; i < num_variables + num_slacks; ++i) {

99 }

100 for (const int c : to_postprocess_) {

101 auto* literals = problem_->mutable_constraints(c)

102 ->mutable_bool_or()

103 ->mutable_literals();

104 const int last_index = literals->size() - 1;

105 const int last = (*literals)[last_index];

106 (*literals)[last_index] =

107 last >= 0 ? last + num_variables : last - num_variables;

108 }

109 }

110

112 return signed_value > 0 ? signed_value - 1 : signed_value;

113 }

114

115 void AddConstraint(absl::Span<const int> clause, bool last_is_slack = false) {

116 if (last_is_slack)

117 to_postprocess_.push_back(problem_->constraints().size());

118 auto* constraint = problem_->add_constraints()->mutable_bool_or();

119 constraint->mutable_literals()->Reserve(clause.size());

120 for (const int literal : clause) {

121 constraint->add_literals(LiteralToRef(literal));

122 }

123 }

124

126 CHECK_GE(literal, 0) << "Negative literal not supported.";

127 problem_->mutable_objective()->add_vars(LiteralToRef(literal));

128 problem_->mutable_objective()->add_coeffs(value);

129 }

130

132 problem_->mutable_objective()->set_offset(offset);

133 }

134

135 private:

137 std::vector<int> to_postprocess_;

138};

146 public:

148 : interpret_cnf_as_max_sat_(false),

149 wcnf_use_strong_slack_(wcnf_use_strong_slack) {}

150

151

154

155

156

158

159

161 problem->Clear();

162 problem->set_name(ExtractProblemName(filename));

164 return LoadInternal(filename, &wrapper);

165 }

167 problem->Clear();

168 problem->set_name(ExtractProblemName(filename));

170 return LoadInternal(filename, &wrapper);

171 }

172

173 private:

174 template <class Problem>

175 bool LoadInternal(const std::string& filename, Problem* problem) {

176 is_wcnf_ = false;

177 objective_offset_ = 0;

178 positive_literal_to_weight_.clear();

179

180 end_marker_seen_ = false;

181 hard_weight_ = 0;

182 num_skipped_soft_clauses_ = 0;

183 num_singleton_soft_clauses_ = 0;

184 num_added_clauses_ = 0;

185 num_slack_variables_ = 0;

186

187 num_variables_ = 0;

188 num_clauses_ = 0;

189 actual_num_variables_ = 0;

190

191 int num_lines = 0;

192 for (const std::string& line : FileLines(filename)) {

193 ++num_lines;

194 ProcessNewLine(line, problem);

195 }

196 if (num_lines == 0) {

197 LOG(FATAL) << "File '" << filename << "' is empty or can't be read.";

198 }

199

200 if (num_variables_ > 0 && num_variables_ != actual_num_variables_) {

201 LOG(ERROR) << "Wrong number of variables ! Expected:" << num_variables_

202 << " Seen:" << actual_num_variables_;

203 }

204

205 problem->SetSizeAndPostprocess(actual_num_variables_, num_slack_variables_);

206

207

208 if (!positive_literal_to_weight_.empty() ||

209 !slack_literal_to_weight_.empty()) {

210 for (const std::pair<int, int64_t> p : positive_literal_to_weight_) {

211 if (p.second != 0) {

212 problem->AddObjectiveTerm(p.first, p.second);

213 }

214 }

215 for (const std::pair<int, int64_t> p : slack_literal_to_weight_) {

216 if (p.second != 0) {

217 problem->AddObjectiveTerm(actual_num_variables_ + p.first, p.second);

218 }

219 }

220 problem->SetObjectiveOffset(objective_offset_);

221 }

222

223

224

225 const int total_seen = num_added_clauses_ + num_singleton_soft_clauses_ +

226 num_skipped_soft_clauses_;

227 if (num_clauses_ > 0 && num_clauses_ != total_seen) {

228 LOG(ERROR) << "Wrong number of clauses ! Expected:" << num_clauses_

229 << " Seen:" << total_seen;

230 }

231 return true;

232 }

233

234

235

236 static std::string ExtractProblemName(const std::string& filename) {

237 const int found = filename.find_last_of('/');

238 const std::string problem_name =

239 found != std::string::npos ? filename.substr(found + 1) : filename;

240 return problem_name;

241 }

242

243 void ProcessHeader(const std::string& line) {

244 static const char kWordDelimiters[] = " ";

245 words_ = absl::StrSplit(line, kWordDelimiters, absl::SkipEmpty());

246

247 CHECK_EQ(words_[0], "p");

248 if (words_[1] == "cnf" || words_[1] == "wcnf") {

249 CHECK(absl::SimpleAtoi(words_[2], &num_variables_));

250 CHECK(absl::SimpleAtoi(words_[3], &num_clauses_));

251 if (words_[1] == "wcnf") {

252 is_wcnf_ = true;

253 hard_weight_ = 0;

254 if (words_.size() > 4) {

255 CHECK(absl::SimpleAtoi(words_[4], &hard_weight_));

256 }

257 }

258 } else {

259 LOG(FATAL) << "Unknown file type: " << words_[1];

260 }

261 }

262

263 template <class Problem>

264 void ProcessNewLine(const std::string& line, Problem* problem) {

265 if (line.empty() || end_marker_seen_) return;

266 if (line[0] == 'c') return;

267 if (line[0] == '%') {

268 end_marker_seen_ = true;

269 return;

270 }

271 if (line[0] == 'p') {

272 ProcessHeader(line);

273 return;

274 }

275

276

277 if (num_variables_ == 0) {

278 is_wcnf_ = true;

279 }

280

281 static const char kWordDelimiters[] = " ";

282 auto splitter = absl::StrSplit(line, kWordDelimiters, absl::SkipEmpty());

283

284 tmp_clause_.clear();

285 int64_t weight =

286 (!is_wcnf_ && interpret_cnf_as_max_sat_) ? 1 : hard_weight_;

287 bool first = true;

288 bool end_marker_seen = false;

289 for (const absl::string_view word : splitter) {

290 if (first && is_wcnf_) {

291 first = false;

292 if (word == "h") {

293

294

295 weight = hard_weight_;

296 } else {

297 CHECK(absl::SimpleAtoi(word, &weight));

298 CHECK_GE(weight, 0);

299

300

301 if (weight == 0) {

302 ++num_skipped_soft_clauses_;

303 return;

304 }

305 }

306 continue;

307 }

308

309 int signed_value;

310 CHECK(absl::SimpleAtoi(word, &signed_value));

311 if (signed_value == 0) {

312 end_marker_seen = true;

313 break;

314 }

315

316 actual_num_variables_ = std::max(actual_num_variables_,

317 std::max(signed_value, -signed_value));

318 tmp_clause_.push_back(signed_value);

319 }

320 if (!end_marker_seen) return;

321

322 if (weight == hard_weight_) {

323 ++num_added_clauses_;

324 problem->AddConstraint(tmp_clause_);

325 } else {

326 if (tmp_clause_.size() == 1) {

327

328

329

330

331 ++num_singleton_soft_clauses_;

332 const int literal = -tmp_clause_[0];

333 if (literal > 0) {

334 positive_literal_to_weight_[literal] += weight;

335 } else {

336 positive_literal_to_weight_[-literal] -= weight;

337 objective_offset_ += weight;

338 }

339 } else {

340

341

342 const int slack_literal = ++num_slack_variables_;

343

344 slack_literal_to_weight_[slack_literal] += weight;

345 tmp_clause_.push_back(slack_literal);

346

347 ++num_added_clauses_;

348 problem->AddConstraint(tmp_clause_, true);

349

350 if (wcnf_use_strong_slack_) {

351

352

353 for (int i = 0; i + 1 < tmp_clause_.size(); ++i) {

354 problem->AddConstraint({-tmp_clause_[i], -slack_literal},

355 true);

356 }

357 }

358 }

359 }

360 }

361

362 bool interpret_cnf_as_max_sat_;

363 const bool wcnf_use_strong_slack_;

364

365 int num_clauses_ = 0;

366 int num_variables_ = 0;

367 int actual_num_variables_ = 0;

368

369

370 std::vector<absl::string_view> words_;

371

372

373

374 int64_t objective_offset_;

375 absl::btree_map<int, int64_t> positive_literal_to_weight_;

376 absl::btree_map<int, int64_t> slack_literal_to_weight_;

377

378

379 bool is_wcnf_;

380

381 bool end_marker_seen_;

382 int64_t hard_weight_ = 0;

383

384 int num_slack_variables_;

385 int num_skipped_soft_clauses_;

386 int num_singleton_soft_clauses_;

387 int num_added_clauses_;

388

389 std::vector<int> tmp_clause_;

390};