always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix #977

Browse Source
This commit is contained in:
Laurent Perron
2018-12-17 13:56:56 +01:00
parent 0d93b2079c
commit e83e0b233a
1 changed files with 15 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

22
ortools/sat/cp_model_solver.cc
View File

@@ -1823,13 +1823,21 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto,
for (const ConstraintProto& ct : model_proto.constraints()) {
switch (ct.constraint_case()) {
case ConstraintProto::ConstraintCase::kBoolAnd: {
// a => b
const Literal not_a = get_literal(ct.enforcement_literal(0)).Negated();
for (const int ref : ct.bool_and().literals()) {
const Literal b = get_literal(ref);
solver->AddProblemClause({not_a, b});
if (drat_proof_handler != nullptr) {
drat_proof_handler->AddProblemClause({not_a, b});
if (ct.enforcement_literal_size() == 0) {
for (const int ref : ct.bool_and().literals()) {
const Literal b = get_literal(ref);
solver->AddUnitClause(b);
}
} else {
// a => b
const Literal not_a =
get_literal(ct.enforcement_literal(0)).Negated();
for (const int ref : ct.bool_and().literals()) {
const Literal b = get_literal(ref);
solver->AddProblemClause({not_a, b});
if (drat_proof_handler != nullptr) {
drat_proof_handler->AddProblemClause({not_a, b});
}
}
}
break;