47 public:

49

52

53

55

56

57

59

60

61

103

104 private:

105

106

107

108

109 struct PbTerm {

110 int64_t coeff;

111 std::vector<int> literals;

112 };

113

114 enum PbConstraintType {

115 UNDEFINED_OPERATION,

116 GE_OPERATION,

117 EQ_OPERATION,

118 };

119

120 struct PbConstraint {

121 std::vector<PbTerm> terms;

122 PbConstraintType type = UNDEFINED_OPERATION;

123 int64_t rhs = std::numeric_limits<int64_t>::min();

124 int64_t soft_cost = std::numeric_limits<int64_t>::max();

125 };

126

127

128

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

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

131 const std::string problem_name =

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

133 return problem_name;

134 }

135

136 void ProcessNewLine(const std::string& line) {

137 const std::vector<std::string> words =

138 absl::StrSplit(line, absl::ByAnyChar(" ;"), absl::SkipEmpty());

139 if (words.empty() || words[0].empty() || words[0][0] == '*') return;

140

141 if (words[0] == "soft:") {

142 if (words.size() == 1) return;

143 int64_t top_cost;

144 if (!ParseInt64Into(words[1], &top_cost)) return;

145 top_cost_ = top_cost;

146 return;

147 }

148

149 if (words[0] == "min:") {

150 for (int i = 1; i < words.size(); ++i) {

151 const std::string& word = words[i];

152 if (word.empty() || word[0] == ';') continue;

153 if (word[0] == 'x') {

154 const int index = ParseIndex(word.substr(1));

155 num_variables_ = std::max(num_variables_, index);

156 objective_.back().literals.push_back(

157 PbLiteralToCpModelLiteral(index));

158 } else if (word[0] == '~' && word[1] == 'x') {

159 const int index = ParseIndex(word.substr(2));

160 num_variables_ = std::max(num_variables_, index);

161 objective_.back().literals.push_back(

162 NegatedRef(PbLiteralToCpModelLiteral(index)));

163 } else {

164

165 PbTerm term;

166 if (!ParseInt64Into(word, &term.coeff)) return;

167 objective_.emplace_back(std::move(term));

168 }

169 }

170

171

172 for (PbTerm& term : objective_) {

173 if (term.literals.size() <= 1) continue;

175 CHECK_GT(term.literals.size(), 1);

176 }

177

178 return;

179 }

180

181 PbConstraint constraint;

182 for (int i = 0; i < words.size(); ++i) {

183 const std::string& word = words[i];

184 CHECK(!word.empty());

185 if (word[0] == '[') {

186 if (!ParseInt64Into(word.substr(1, word.size() - 2),

187 &constraint.soft_cost)) {

188 return;

189 }

190 } else if (word == ">=") {

191 CHECK_LT(i + 1, words.size());

192 constraint.type = GE_OPERATION;

193 if (!ParseInt64Into(words[i + 1], &constraint.rhs)) return;

194 break;

195 } else if (word == "=") {

196 CHECK_LT(i + 1, words.size());

197 constraint.type = EQ_OPERATION;

198 if (!ParseInt64Into(words[i + 1], &constraint.rhs)) return;

199 break;

200 } else if (word[0] == 'x') {

201 const int index = ParseIndex(word.substr(1));

202 num_variables_ = std::max(num_variables_, index);

203 constraint.terms.back().literals.push_back(

204 PbLiteralToCpModelLiteral(index));

205 } else if (word[0] == '~' && word[1] == 'x') {

206 const int index = ParseIndex(word.substr(2));

207 num_variables_ = std::max(num_variables_, index);

208 constraint.terms.back().literals.push_back(

209 NegatedRef(PbLiteralToCpModelLiteral(index)));

210 } else {

211

212 PbTerm term;

213 if (!ParseInt64Into(word, &term.coeff)) return;

214 constraint.terms.emplace_back(std::move(term));

215 }

216 }

217

218

219 for (PbTerm& term : constraint.terms) {

220 if (term.literals.size() <= 1) continue;

222 CHECK_GT(term.literals.size(), 1);

223 }

224

225 constraints_.push_back(std::move(constraint));

226 }

227

228 std::string ValidateModel() {

229

230 for (const PbConstraint& constraint : constraints_) {

231 if (constraint.rhs == std::numeric_limits<int64_t>::min()) {

232 return "constraint error: undefined rhs";

233 }

234

235 if (constraint.type == UNDEFINED_OPERATION) {

236 return "constraint error: undefined operation";

237 }

238

239 for (const PbTerm& term : constraint.terms) {

240 if (term.coeff == 0) {

241 return "constraint error: coefficient cannot be zero";

242 }

243 if (term.literals.empty()) return "constraint error: empty literals";

244 if (term.literals.size() == 1) {

246 return "constraint error: linear terms must use positive literals";

247 }

248 }

249 }

250 }

251

252

253 if (objective_.empty()) return "";

254

255 for (const PbTerm& term : objective_) {

256 if (term.coeff == 0) return "objective error: coefficient cannot be zero";

257 if (term.literals.empty()) return "objective error: empty literals";

258 if (term.literals.size() == 1) {

260 return "objective error: linear terms must use positive literals";

261 }

262 return "";

263 }

264 }

265

266 return "";

267 }

268

269 static int PbLiteralToCpModelLiteral(int pb_literal) {

270 return pb_literal > 0 ? pb_literal - 1 : -pb_literal;

271 }

272

273 bool ParseInt64Into(const std::string& word, int64_t* value) {

274 if (!absl::SimpleAtoi(word, value)) {

275 VLOG(1) << "Failed to parse int64_t: " << word;

276 model_is_supported_ = false;

277 return false;

278 }

279 return true;

280 }

281

282 static int ParseIndex(absl::string_view word) {

283 int index;

284 CHECK(absl::SimpleAtoi(word, &index));

285 return index;

286 }

287

288 int GetVariable(const PbTerm& term, CpModelProto* model) {

289 CHECK(!term.literals.empty());

290 if (term.literals.size() == 1) {

292 return term.literals[0];

293 }

294

295 const auto it = product_to_var_.find(term.literals);

296 if (it != product_to_var_.end()) {

297 return it->second;

298 }

299

300 const int var_index = model->variables_size();

301 IntegerVariableProto* var_proto = model->add_variables();

302 var_proto->add_domain(0);

303 var_proto->add_domain(1);

304

305 product_to_var_[term.literals] = var_index;

306

307

308

309 ConstraintProto* var_to_literals = model->add_constraints();

310 var_to_literals->add_enforcement_literal(var_index);

311

312

313 ConstraintProto* literals_to_var = model->add_constraints();

314 literals_to_var->mutable_bool_and()->add_literals(var_index);

315

316 for (const int proto_literal : term.literals) {

317 var_to_literals->mutable_bool_and()->add_literals(proto_literal);

318 literals_to_var->add_enforcement_literal(proto_literal);

319 }

320

321 return var_index;

322 }

323

324 void BuildModel(CpModelProto* model) {

325

326 for (int i = 0; i < num_variables_; ++i) {

327 IntegerVariableProto* var = model->add_variables();

328 var->add_domain(0);

329 var->add_domain(1);

330 }

331

332 for (const PbConstraint& constraint : constraints_) {

333 ConstraintProto* ct = model->add_constraints();

334 LinearConstraintProto* lin = ct->mutable_linear();

335 for (const PbTerm& term : constraint.terms) {

336 lin->add_vars(GetVariable(term, model));

337 lin->add_coeffs(term.coeff);

338 }

339 if (constraint.type == GE_OPERATION) {

340 lin->add_domain(constraint.rhs);

341 lin->add_domain(std::numeric_limits<int64_t>::max());

342 } else if (constraint.type == EQ_OPERATION) {

343 lin->add_domain(constraint.rhs);

344 lin->add_domain(constraint.rhs);

345 } else {

346 LOG(FATAL) << "Unsupported operation: " << constraint.type;

347 }

348

349 if (constraint.soft_cost != std::numeric_limits<int64_t>::max()) {

350 const int violation_var_index = model->variables_size();

351 IntegerVariableProto* violation_var = model->add_variables();

352 violation_var->add_domain(0);

353 violation_var->add_domain(1);

354

355

356 model->mutable_objective()->add_vars(violation_var_index);

357 model->mutable_objective()->add_coeffs(constraint.soft_cost);

358

359

360 ct->add_enforcement_literal(NegatedRef(violation_var_index));

361 }

362 }

363

364 if (!objective_.empty()) {

365 CpObjectiveProto* obj = model->mutable_objective();

366 for (const PbTerm& term : objective_) {

367 obj->add_vars(GetVariable(term, model));

368 obj->add_coeffs(term.coeff);

369 }

370 }

371

372 if (top_cost_.has_value()) {

373 CpObjectiveProto* obj = model->mutable_objective();

374 obj->add_domain(std::numeric_limits<int64_t>::min());

375 obj->add_domain(top_cost_.value());

376 }

377 }

378

379 int num_variables_;

380 std::vector<PbTerm> objective_;

381 std::vector<PbConstraint> constraints_;

382 absl::flat_hash_map<absl::Span<const int>, int> product_to_var_;

383 bool model_is_supported_ = true;

384 std::optional<int64_t> top_cost_;

385};