Additional constraint generated during transformation of choice rules #282
Conversation
... that is grounded at the same time as the choice rule itself, helps propagation and thus potentially improves solving performance.
|
I´ve marked this pull request as draft because I still want to do some performance tests. |
Codecov Report
@@ Coverage Diff @@
## master #282 +/- ##
============================================
+ Coverage 77.46% 77.47% +0.01%
Complexity 2312 2312
============================================
Files 178 178
Lines 7782 7786 +4
Branches 1352 1352
============================================
+ Hits 6028 6032 +4
Misses 1334 1334
Partials 420 420
Continue to review full report at Codecov.
|
|
This feature does not seem to achieve the expected performance benefits (at least in some cases). The alternative approach #284 to solve this issue, however, shows benefits on this instance: ~7s (5k backjumps). Maybe further performance analysis is in order before either of the two approaches is fully implemented and merged? |
|
What is the status on this PR and #284 ? From my current understanding, it feels a bit like the additional nogood/constraint might be superfluous. At least in cases where completion nogoods are added (i.e., currently only if the head contains all variables of the body and no other rule can derive the head predicate), the added constraint is already implied via the completion. |
The status has not changed since Dec 16, 2020, I have not done any additional performance analysis since then. |
In addition to the two normal rules encoding a choice rule,
ChoiceHeadToNormalnow also generates a constraint that forbids the two complementary head literals to be true at the same time. The constraint helps propagation and thus potentially improves solving performance. It can be grounded at the same time as the choice rule itself if constraints are grounded permissively (withgtc >= 2since the body of the constraint contains two literals more than the body of the choice rule).