This is more of a research issue, but I noticed the following:
If we have a constraint of the form
new_var_177 * (cmp_result_1 + cmp_result_2 - cmp_result_1 * cmp_result_2) - cmp_result_4 = 0
where new_var_177 only occurs here and cmp_result_* are all binary, then we can replace this constraint with an equivalent constraint that does not need new_var_177.
More general:
If we have a constraint of the form
where F only occurs in that constraint, then this is equivalent to
If A is binary, this condition can be written as
Maybe this can be generalized to other types of constraints.
For the constraint above, the main challenge for implementing this in the rule system is to correctly determine the range constraint of (cmp_result_1 + cmp_result_2 - cmp_result_1 * cmp_result_2).
We could do a structural analysis for exactly this structure, or we could detect that it only contains boolean variables and perform an exhaustive evaluation of the possible values. Maybe the latter could also be useful for replacing the exhaustive search altogether.
This is more of a research issue, but I noticed the following:
If we have a constraint of the form
where
new_var_177only occurs here andcmp_result_*are all binary, then we can replace this constraint with an equivalent constraint that does not neednew_var_177.More general:
If we have a constraint of the form
where
Fonly occurs in that constraint, then this is equivalent toIf
Ais binary, this condition can be written asMaybe this can be generalized to other types of constraints.
For the constraint above, the main challenge for implementing this in the rule system is to correctly determine the range constraint of
(cmp_result_1 + cmp_result_2 - cmp_result_1 * cmp_result_2).We could do a structural analysis for exactly this structure, or we could detect that it only contains boolean variables and perform an exhaustive evaluation of the possible values. Maybe the latter could also be useful for replacing the exhaustive search altogether.