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

[FZ] downgrade nosets.mzn to 2.1.7; [SAT] polish presolve, expand code of previous commits; add more presolve on circuit

Browse Source
This commit is contained in:
Laurent Perron
2018-09-03 16:15:13 +02:00
parent beb05f0079
commit b7c97377cf
5 changed files with 207 additions and 207 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
ortools/flatzinc/cp_model_fz_solver.cc
View File

@@ -234,7 +234,7 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct, ct);
} else if (fz_ct.type == "bool_lin_eq") {
auto* arg = ct->mutable_linear();
std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
for (int i = 0; i < vars.size(); ++i) {
arg->add_vars(vars[i]);
arg->add_coeffs(fz_ct.arguments[0].values[i]);

226
ortools/flatzinc/mznlib_sat/nosets.mzn
View File

@@ -3,13 +3,9 @@
% Guido Tack <guido.tack@monash.edu>
% Gleb Belov <gleb.belov@monash.edu>
%
% Set comparisons are often used just to avoid symmetries. For that, lex cmp of direct set2bools
% would be much cheaper than the actual set_le++ below TODO
include "lex_less.mzn";
include "lex_lesseq.mzn";
predicate mzn_reverse_map_var(var set of int: x) = let {
array[int] of var bool: b = set2bools(x)
} in true;
function var set of int: reverse_map(array[int] of var bool: b);
function set of int: reverse_map(array[int] of bool: b) ::promise_total =
@@ -18,8 +14,8 @@ function set of int: reverse_map(array[int] of bool: b) ::promise_total =
array[int] of var bool: set2bools(var set of int: x) ::promise_total =
if is_fixed(x) then set2bools(fix(x)) else
let {
array[int] of var bool: b = array1d( min(ub(x))..max(ub(x)),
[ set2bools_bit( x, i ) | i in min(ub(x))..max(ub(x)) ] );
array[min(ub(x))..max(ub(x))] of var bool: b =
[ set2bools_bit( x, i ) | i in min(ub(x))..max(ub(x)) ];
constraint (x = reverse_map(b)) :: is_reverse_map;
} in b
endif;
@@ -27,9 +23,9 @@ array[int] of var bool: set2bools(var set of int: x, set of int: ubx) ::promise_
if is_fixed(x) then set2bools(fix(x), ubx) else
let {
array[int] of var bool: b0 = set2bools( x ); %% Call in any case ?? TODO
array[int] of var bool: b = array1d( min(ubx)..max(ubx),
array[min(ubx)..max(ubx)] of var bool: b =
[ if i in ubx then set2bools_bit( x, i ) else false endif
| i in min(ubx)..max(ubx) ] );
| i in min(ubx)..max(ubx) ];
%% Not again: constraint (x = reverse_map(b)) :: is_reverse_map;
} in b
endif;
@@ -45,17 +41,13 @@ function var bool: set2bools_bit( var set of int: x, int: i ) ::promise_total =
else false endif;
predicate set_eq(var set of int: x, var set of int: y) ::promise_total =
predicate set_eq(var set of int: x, var set of int: y) =
if not has_ub_set(x) /\ not has_ub_set(y) then
assert(false, "set_eq: cannot determine bounds of set variables")
assert(false, "Cannot determine bounds of set variables")
elseif not has_ub_set(x) then set_eq(y,x)
else
let {
set of int: uby = if has_ub_set(y) then ub(y) else
let {
constraint y subset x,
} in ub(x)
endif;
set of int: uby = if has_ub_set(y) then ub(y) else ub(x) endif;
array[int] of var bool: bx = set2bools(x);
array[int] of var bool: by = set2bools(y,uby);
} in forall (i in index_set(bx) union index_set(by)) (
@@ -65,7 +57,7 @@ predicate set_eq(var set of int: x, var set of int: y) ::promise_total =
)
endif;
predicate set_eq_reif(var set of int: x, var set of int: y, var bool: b) ::promise_total =
predicate set_eq_reif(var set of int: x, var set of int: y, var bool: b) =
if is_fixed(b) then
if true==fix(b) then x==y else x!=y endif
else
@@ -79,7 +71,7 @@ predicate set_eq_reif(var set of int: x, var set of int: y, var bool: b) ::promi
)
endif;
predicate set_ne(var set of int: x, var set of int: y) ::promise_total =
predicate set_ne(var set of int: x, var set of int: y) =
let {
array[int] of var bool: bx = set2bools(x);
array[int] of var bool: by = set2bools(y);
@@ -89,30 +81,84 @@ predicate set_ne(var set of int: x, var set of int: y) ::promise_total =
else bx[i]!=by[i] endif
);
predicate set_ne_reif(var set of int: x, var set of int: y, var bool: b) ::promise_total =
predicate set_ne_reif(var set of int: x, var set of int: y, var bool: b) =
set_eq_reif( x, y, not b );
% Set comparisons are often used just to avoid symmetries.
% Reifs/imps are done automatically from these templates
predicate set_le(var set of int: x, var set of int: y) ::promise_total =
%%% lex cmp of the sparse vectors
predicate set_le_lt_base__(var set of int: x, var set of int: y,
var bool: fValReif, bool: fStrict) ::promise_total =
let { %% DOES NOT HELP in -Glinear globals_alldiff_set_nosets.mzn ....
array[int] of var bool: bx0 = set2bools(x); %% just to call reverse_map
array[int] of var bool: by0 = set2bools(y);
} in
if not has_ub_set(x) \/ not has_ub_set(y) then
assert(false, "set_le_lt_base__: cannot determine bounds of set variables")
elseif {}==ub(x) /\ {}==ub(y) then
fValReif==not fStrict
elseif {}!=ub(x) /\ {}!=ub(y) /\ max(ub(x))<min(ub(y)) /\ not fStrict then
fValReif
elseif {}!=ub(x) /\ {}!=ub(y) /\ min(ub(x))>max(ub(y)) /\ fStrict then
not fValReif
else
let {
set of int: ubxy = ub(x) union ub(y),
set of int: ubxy = ub(x) union ub(y);
array[int] of var bool: bx = set2bools(x, ubxy);
array[int] of var bool: by = set2bools(y, ubxy);
int: i0 = min( ubxy );
array[i0..i0+length(bx)] of var bool: bOkFrom;
array[int] of var bool: bXMaxFrom = getMaxRearBools( set2bools( x ), i0+1..max(ubxy)+1 );
array[int] of var bool: bYMaxFrom = getMaxRearBools( set2bools( y ), i0+1..max(ubxy)+1 );
} in
lex_lesseq( by, bx );
% trace( "set_le_lt_base__: " ++ show(ub(x)) ++ ", " ++ show(ub(y)) ++ "\n") /\
(bOkFrom[i0] == fValReif)
/\
(bOkFrom[i0+length(bx)] == not fStrict)
/\
forall(i in ubxy) ( %% Can linearize stronger? TODO
bOkFrom[i] <-> (
( (bx[i] == by[i]) /\ bOkFrom[i+1] )
\/
( (bx[i] < by[i]) /\ not bXMaxFrom[i+1] )
\/
( (bx[i] > by[i]) /\ bYMaxFrom[i+1] )
)
)
endif;
function var bool: getMaxRearBools_bit( array[int] of var bool: b, int: i ) =
if {}==index_set( b ) \/ i>max( index_set( b ) ) then
false
elseif i in index_set( b ) then
b[i] \/ getMaxRearBools_bit( b, i+1 )
else
getMaxRearBools_bit( b, min( index_set( b ) ) )
endif;
%% Returns an array of bools each is the max of b[i] and the later elements
function array[int] of var bool: getMaxRearBools( array[int] of var bool: b ) =
array1d( index_set(b), [ getMaxRearBools_bit( b, i )
| i in index_set( b ) ] );
%% Generalizes getMaxRearBools to a sub/superset of the array's indexes
function array[int] of var bool: getMaxRearBools(
array[int] of var bool: b, set of int: ubb ) =
array1d( min(ubb)..max(ubb), [ getMaxRearBools_bit( b, i )
| i in min(ubb)..max(ubb) ] );
predicate set_le(var set of int: x, var set of int: y) ::promise_total =
set_le_lt_base__(x, y, true, false);
predicate set_le_reif(var set of int: x, var set of int: y, var bool: p) ::promise_total =
set_le_lt_base__(x, y, p, false);
predicate set_lt(var set of int: x, var set of int: y) ::promise_total =
let {
set of int: ubxy = ub(x) union ub(y),
array[int] of var bool: bx = set2bools(x, ubxy);
array[int] of var bool: by = set2bools(y, ubxy);
} in
lex_less( by, bx );
set_le_lt_base__(x, y, true, true);
predicate set_lt_reif(var set of int: x, var set of int: y, var bool: p) ::promise_total =
set_le_lt_base__(x, y, p, true);
predicate set_subset(var set of int: x, var set of int: y) ::promise_total =
predicate set_subset(var set of int: x, var set of int: y) =
let {
array[int] of var bool: bx = set2bools(x);
array[int] of var bool: by = set2bools(y);
@@ -121,7 +167,7 @@ predicate set_subset(var set of int: x, var set of int: y) ::promise_total =
else bx[i] -> by[i] endif
);
predicate set_subset_reif(var set of int: x, var set of int: y, var bool: b) ::promise_total =
predicate set_subset_reif(var set of int: x, var set of int: y, var bool: b) =
let {
array[int] of var bool: bx = set2bools(x);
array[int] of var bool: by = set2bools(y);
@@ -130,11 +176,6 @@ predicate set_subset_reif(var set of int: x, var set of int: y, var bool: b) ::p
else bx[i] -> by[i] endif
);
%%% Map the subset operation to superset
predicate set_superset(var set of int: x, var set of int: y) ::promise_total = set_subset( y, x );
predicate set_superset_reif(var set of int: x, var set of int: y, var bool: b) ::promise_total =
set_subset_reif( y, x, b );
function var set of int: set_intersect(var set of int: x, var set of int: y) ::promise_total =
let {
array[int] of var bool: bx = set2bools(x);
@@ -169,9 +210,9 @@ function var set of int: set_diff(var set of int: x, var set of int: y) ::promis
let {
array[int] of var bool: bx = set2bools(x);
array[int] of var bool: by = set2bools(y);
var set of ub(x) diff lb(y): z;
var set of (index_set(bx) diff index_set(by)): z;
array[int] of var bool: bz = set2bools(z);
constraint forall (i in ub(z)) (
constraint forall (i in index_set(bz)) (
bz[i] = (bx[i] /\ (not by[i]))
);
} in z;
@@ -180,9 +221,9 @@ function var set of int: set_symdiff(var set of int: x, var set of int: y) ::pro
let {
array[int] of var bool: bx = set2bools(x);
array[int] of var bool: by = set2bools(y);
var set of (ub(x) diff lb(y)) union (ub(y) diff lb(x)): z;
var set of (index_set(bx) diff index_set(by)): z;
array[int] of var bool: bz = set2bools(z);
constraint forall (i in ub(z)) (
constraint forall (i in index_set(bz)) (
bz[i] = (bx[i] xor by[i])
);
} in z;
@@ -191,26 +232,18 @@ function var int: card(var set of int: x) ::promise_total =
let {
array[int] of var bool: bx = set2bools(x);
var 0..length(bx) : c;
constraint bool_lin_eq([1 | i in index_set(bx)],[bx[i] | i in index_set(bx)],c);
constraint bool_lin_eq([1 | i in index_set(bx)],bx,c);
} in c;
predicate set_in(int: x, var set of int: y) ::promise_total =
let {
array[int] of var bool: by = set2bools(y);
} in by[x];
predicate set_in(var int: x, var set of int: y) ::promise_total =
predicate set_in(var int: x, var set of int: y) =
let {
array[int] of var bool: by = set2bools(y);
} in by[x];
predicate set_in_reif(int: x, var set of int: y, var bool: b) ::promise_total =
if x in ub(y) then
b <-> set2bools(y)[x]
else
not b
endif;
predicate set_in_reif(var int: x, var set of int: y, var bool: b) ::promise_total =
b <-> ( x in ub(y) /\ set2bools(y)[x] );
predicate set_in_reif(var int: x, var set of int: y, var bool: b) =
let {
array[int] of var bool: by = set2bools(y);
} in b <-> by[x];
function array[int] of var bool: setarray2bools(array[int] of var set of int: x) =
if length(x)=0 then [] else
@@ -218,82 +251,5 @@ function array[int] of var bool: setarray2bools(array[int] of var set of int: x)
endif;
%% Par version no sense
predicate array_var_set_element(var int: x, array[int] of var set of int: y, var set of int: z) ::promise_total =
let {
constraint x in { i | i in index_set( y ) where
lb(y[i]) subset ub(z) /\ lb(z) subset ub(y[i])
};
set of int: sUB = array_union( [ ub(y[i]) | i in dom(x) ] );
set of int: sLB = array_intersect( [ lb(y[i]) | i in dom(x) ] );
constraint z subset sUB,
constraint sLB subset z,
} in
forall (k in ub(z)) (
set2bools(z)[k] ==
if k in sUB then
if k in sLB then
true
else
array1d( lb(x)..ub(x),
[ if k in ub(y[i]) then set2bools(y[i])[k] else false endif | i in dom(x) ] )[x]
endif
else
false
endif
) /\
forall (k in sUB diff ub(z))(
if k in sLB then
false %% fail the constraint
else
not array1d( lb(x)..ub(x),
[ if k in ub(y[i]) then set2bools(y[i])[k] else false endif | i in dom(x) ] )[x]
endif
);
predicate array_set_element(var int: x, array[int] of set of int: y, var set of int: z) ::promise_total =
let {
constraint x in { i | i in index_set( y ) where
y[i] subset ub(z) /\ lb(z) subset y[i]
};
set of int: sUB = array_union( [ y[i] | i in dom(x) ] );
set of int: sLB = array_intersect( [ y[i] | i in dom(x) ] );
constraint z subset sUB,
constraint sLB subset z,
} in
forall (k in ub(z)) (
set2bools(z)[k] ==
if k in sUB then
if k in sLB then
true
else
array1d( lb(x)..ub(x),
[ if k in ub(y[i]) then set2bools(y[i])[k] else false endif | i in dom(x) ] )[x]
endif
else
false
endif
) /\
forall (k in sUB diff ub(z))(
if k in sLB then
false %% fail the constraint
else
not array1d( lb(x)..ub(x),
[ if k in ub(y[i]) then set2bools(y[i])[k] else false endif | i in dom(x) ] )[x]
endif
);
annotation set_search(array[int] of var set of int: x, ann: a1, ann: a2, ann: a3) =
seq_search( [ bool_search(set2bools(x[i]),a1,a2,a3) | i in index_set(x) ] );
annotation warm_start( array[int] of var set of int: x, array[int] of set of int: v ) =
warm_start_array( [
let {
array[int] of var bool: xb = set2bools(x[i]),
set of int: is_var = ub(x[i]) diff lb(x[i]),
int: iV = i - min(index_set(x)) + if 0<length(v) then min(index_set(v)) else 0 endif,
} in
warm_start( [ xb[k] | k in is_var ],
if iV in index_set(v) then [ k in v[iV] | k in is_var ] else [] endif )
| i in index_set(x) ] ); %% ignoring v[i] diff ub(x[i]) and lb(x[i]) diff v[i]
bool_search(setarray2bools(x),a1,a2,a3);

7
ortools/sat/cp_model_checker.cc
View File

@@ -358,13 +358,6 @@ class ConstraintChecker {
for (int i = 0; i < num_variables; ++i) {
sum += Value(ct.linear().vars(i)) * ct.linear().coeffs(i);
}
if (!DomainInProtoContains(ct.linear(), sum)) {
for (int i = 0; i < num_variables; ++i) {
const int var = ct.linear().vars(i);
LOG(INFO) << "var#" << var << " = " << Value(var);
}
LOG(INFO) << ct.DebugString();
}
return DomainInProtoContains(ct.linear(), sum);
}

50
ortools/sat/cp_model_expand.cc
View File

@@ -334,6 +334,53 @@ void ExpandIntMod(ConstraintProto* ct, ExpansionHelper* helper) {
helper->statistics["kIntMod"]++;
}
void ExpandIntProdWithBoolean(int bool_ref, int int_ref, int product_ref,
ExpansionHelper* helper) {
ConstraintProto* const one = helper->expanded_proto.add_constraints();
one->add_enforcement_literal(bool_ref);
one->mutable_linear()->add_vars(int_ref);
one->mutable_linear()->add_coeffs(1);
one->mutable_linear()->add_vars(product_ref);
one->mutable_linear()->add_coeffs(-1);
one->mutable_linear()->add_domain(0);
one->mutable_linear()->add_domain(0);
ConstraintProto* const zero = helper->expanded_proto.add_constraints();
zero->add_enforcement_literal(NegatedRef(bool_ref));
zero->mutable_linear()->add_vars(product_ref);
zero->mutable_linear()->add_coeffs(1);
zero->mutable_linear()->add_domain(0);
zero->mutable_linear()->add_domain(0);
}
void ExpandIntProd(ConstraintProto* ct, ExpansionHelper* helper) {
const IntegerArgumentProto& int_prod = ct->int_prod();
if (int_prod.vars_size() != 2) return;
const int a = int_prod.vars(0);
const int b = int_prod.vars(1);
const IntegerVariableProto& a_proto =
helper->expanded_proto.variables(PositiveRef(a));
const IntegerVariableProto& b_proto =
helper->expanded_proto.variables(PositiveRef(b));
const int p = int_prod.target();
const bool a_is_boolean = RefIsPositive(a) && a_proto.domain_size() == 2 &&
a_proto.domain(0) == 0 && a_proto.domain(1) == 1;
const bool b_is_boolean = RefIsPositive(b) && b_proto.domain_size() == 2 &&
b_proto.domain(0) == 0 && b_proto.domain(1) == 1;
// We expand if exactly one of {a, b} is Boolean. If both are Boolean, it
// will be presolved into a better version.
if (a_is_boolean && !b_is_boolean) {
ExpandIntProdWithBoolean(a, b, p, helper);
ct->Clear();
helper->statistics["kIntProd"]++;
} else if (b_is_boolean && !a_is_boolean) {
ExpandIntProdWithBoolean(b, a, p, helper);
ct->Clear();
helper->statistics["kIntProd"]++;
}
}
} // namespace
CpModelProto ExpandCpModel(const CpModelProto& initial_model) {
@@ -349,6 +396,9 @@ CpModelProto ExpandCpModel(const CpModelProto& initial_model) {
case ConstraintProto::ConstraintCase::kIntMod:
ExpandIntMod(ct, &helper);
break;
case ConstraintProto::ConstraintCase::kIntProd:
ExpandIntProd(ct, &helper);
break;
default:
break;
}

129
ortools/sat/cp_model_presolve.cc
View File

@@ -200,6 +200,24 @@ struct PresolveContext {
}
}
// Because we always replace equivalent literals before preprocessing a
// constraint, we should never run into a case where one of the literal is
// fixed but the other is not updated. So this can be called without the need
// to keep around the constraints that detected this relation.
void AddBooleanEqualityRelation(int ref_a, int ref_b) {
if (ref_a == ref_b) return;
if (ref_a == NegatedRef(ref_b)) {
is_unsat = true;
return;
}
if (RefIsPositive(ref_a) == RefIsPositive(ref_b)) {
affine_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), 1, 0);
var_equiv_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), 1, 0);
} else {
affine_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), -1, 1);
}
}
// This makes sure that the affine relation only uses one of the
// representative from the var_equiv_relations.
AffineRelation::Relation GetAffineRelation(int var) {
@@ -557,13 +575,12 @@ bool PresolveIntProd(ConstraintProto* ct, PresolveContext* context) {
if (HasEnforcementLiteral(*ct)) return false;
if (ct->int_prod().vars_size() == 2) {
const int a = ct->int_prod().vars(0);
const int b = ct->int_prod().vars(1);
int a = ct->int_prod().vars(0);
int b = ct->int_prod().vars(1);
const int p = ct->int_prod().target();
const bool a_is_boolean = context->MinOf(a) == 0 && context->MaxOf(a) == 1;
const bool b_is_boolean = context->MinOf(b) == 0 && context->MaxOf(b) == 1;
if (context->MinOf(a) == context->MaxOf(a)) {
if (context->IsFixed(b)) std::swap(a, b);
if (context->IsFixed(a)) {
ConstraintProto* const lin = context->working_model->add_constraints();
lin->mutable_linear()->add_vars(b);
lin->mutable_linear()->add_coeffs(context->MinOf(a));
@@ -574,57 +591,6 @@ bool PresolveIntProd(ConstraintProto* ct, PresolveContext* context) {
context->UpdateRuleStats("int_prod: linearize product by constant.");
return RemoveConstraint(ct, context);
} else if (context->MinOf(b) == context->MaxOf(b)) {
ConstraintProto* const lin = context->working_model->add_constraints();
lin->mutable_linear()->add_vars(a);
lin->mutable_linear()->add_coeffs(context->MinOf(b));
lin->mutable_linear()->add_vars(p);
lin->mutable_linear()->add_coeffs(-1);
lin->mutable_linear()->add_domain(0);
lin->mutable_linear()->add_domain(0);
context->UpdateRuleStats("int_prod: linearize product by constant.");
return RemoveConstraint(ct, context);
}
if (a_is_boolean && !b_is_boolean) {
ConstraintProto* const one = context->working_model->add_constraints();
one->add_enforcement_literal(a);
one->mutable_linear()->add_vars(b);
one->mutable_linear()->add_coeffs(1);
one->mutable_linear()->add_vars(p);
one->mutable_linear()->add_coeffs(-1);
one->mutable_linear()->add_domain(0);
one->mutable_linear()->add_domain(0);
ConstraintProto* const zero = context->working_model->add_constraints();
zero->add_enforcement_literal(NegatedRef(a));
zero->mutable_linear()->add_vars(p);
zero->mutable_linear()->add_coeffs(1);
zero->mutable_linear()->add_domain(0);
zero->mutable_linear()->add_domain(0);
context->UpdateRuleStats("int_prod: expand product by boolean.");
return RemoveConstraint(ct, context);
} else if (b_is_boolean && !a_is_boolean) {
ConstraintProto* const one = context->working_model->add_constraints();
one->add_enforcement_literal(b);
one->mutable_linear()->add_vars(a);
one->mutable_linear()->add_coeffs(1);
one->mutable_linear()->add_vars(p);
one->mutable_linear()->add_coeffs(-1);
one->mutable_linear()->add_domain(0);
one->mutable_linear()->add_domain(0);
ConstraintProto* const zero = context->working_model->add_constraints();
zero->add_enforcement_literal(NegatedRef(b));
zero->mutable_linear()->add_vars(p);
zero->mutable_linear()->add_coeffs(1);
zero->mutable_linear()->add_domain(0);
zero->mutable_linear()->add_domain(0);
context->UpdateRuleStats("int_prod: expand product by boolean.");
return RemoveConstraint(ct, context);
}
}
@@ -852,6 +818,9 @@ bool PresolveLinear(ConstraintProto* ct, PresolveContext* context) {
rhs = AdditionOfSortedDisjointIntervals(
rhs, {{-sum_of_fixed_terms, -sum_of_fixed_terms}});
}
if (gcd > 1) {
rhs = InverseMultiplicationOfSortedDisjointIntervals(rhs, gcd);
}
ct->mutable_linear()->clear_vars();
ct->mutable_linear()->clear_coeffs();
for (const auto entry : var_to_coeff) {
@@ -859,14 +828,6 @@ bool PresolveLinear(ConstraintProto* ct, PresolveContext* context) {
ct->mutable_linear()->add_vars(entry.first);
ct->mutable_linear()->add_coeffs(entry.second / gcd);
}
if (gcd > 1) {
rhs = InverseMultiplicationOfSortedDisjointIntervals(rhs, gcd);
ct->mutable_linear()->clear_domain();
for (const auto& i : rhs) {
ct->mutable_linear()->add_domain(i.start);
ct->mutable_linear()->add_domain(i.end);
}
}
// Empty constraint?
if (ct->linear().vars().empty()) {
@@ -1511,6 +1472,46 @@ bool PresolveCircuit(ConstraintProto* ct, PresolveContext* context) {
++new_size;
}
// Look for in/out-degree of two, this will imply that one of the indicator
// Boolean is equal to the negation of the other.
for (int i = 0; i < num_nodes; ++i) {
if (new_in_degree[i] == 2) {
std::vector<int> literals;
for (const int ref : incoming_arcs[i]) {
if (context->LiteralIsFalse(ref)) continue;
if (context->LiteralIsTrue(ref)) {
literals.clear();
break;
}
literals.push_back(ref);
}
if (literals.size() == 2) {
if (PositiveRef(literals[0]) != PositiveRef(literals[1])) {
context->UpdateRuleStats("circuit: degree 2");
}
context->AddBooleanEqualityRelation(literals[0],
NegatedRef(literals[1]));
}
}
if (new_out_degree[i] == 2) {
std::vector<int> literals;
for (const int ref : outgoing_arcs[i]) {
if (context->LiteralIsFalse(ref)) continue;
if (context->LiteralIsTrue(ref)) {
literals.clear();
break;
}
}
if (literals.size() == 2) {
if (PositiveRef(literals[0]) != PositiveRef(literals[1])) {
context->UpdateRuleStats("circuit: degree 2");
}
context->AddBooleanEqualityRelation(literals[0],
NegatedRef(literals[1]));
}
}
}
// Detect infeasibility due to a node having no more incoming or outgoing arc.
// This is a bit tricky because for now the meaning of the constraint says
// that all nodes that appear in at least one of the arcs must be in the