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

[CP-SAT] support int_prod with arity > 2; fix a few bugs, mostly around unsat models; add parameters for lp tolerance; optimize the code on hot spot

Browse Source
This commit is contained in:
Laurent Perron
2023-10-18 15:47:37 +02:00
parent 02c993cebe
commit 01dd97f64e
26 changed files with 216 additions and 127 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
ortools/sat/simplification.cc
View File

@@ -1209,7 +1209,7 @@ void ProbeAndFindEquivalentLiteral(
const Literal true_lit = assignment.LiteralIsTrue(Literal(i))
? Literal(rep)
: Literal(rep).Negated();
solver->AddUnitClause(true_lit);
if (!solver->AddUnitClause(true_lit)) return;
if (drat_proof_handler != nullptr) {
drat_proof_handler->AddClause({true_lit});
}
@@ -1223,7 +1223,7 @@ void ProbeAndFindEquivalentLiteral(
const Literal true_lit = assignment.LiteralIsTrue(Literal(rep))
? Literal(i)
: Literal(i).Negated();
solver->AddUnitClause(true_lit);
if (!solver->AddUnitClause(true_lit)) return;
if (drat_proof_handler != nullptr) {
drat_proof_handler->AddClause({true_lit});
}
@@ -1233,7 +1233,7 @@ void ProbeAndFindEquivalentLiteral(
const Literal true_lit = assignment.LiteralIsTrue(Literal(i))
? Literal(rep)
: Literal(rep).Negated();
solver->AddUnitClause(true_lit);
if (!solver->AddUnitClause(true_lit)) return;
if (drat_proof_handler != nullptr) {
drat_proof_handler->AddClause({true_lit});
}