Additional constraint generated during transformation of choice rules

[rtaupe]

In addition to the two normal rules encoding a choice rule, ChoiceHeadToNormal now 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 (with gtc >= 2 since the body of the constraint contains two literals more than the body of the choice rule).

[rtaupe]

I´ve marked this pull request as draft because I still want to do some performance tests.

[codecov[bot]]

Codecov Report

Merging #282 (fff5c36) into master (ae5280d) will increase coverage by 0.01%. The diff coverage is 100.00%.

@@             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              

Impacted Files	Coverage Δ	Complexity Δ
...ha/grounder/transformation/ChoiceHeadToNormal.java	86.36% <100.00%> (+1.36%)	7.00 <0.00> (ø)

---

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update ae5280d...fff5c36. Read the comment docs.

[rtaupe]

This feature does not seem to achieve the expected performance benefits (at least in some cases). For example, a pup instance is solved within ~11 seconds (15k backjumps) without this feature and within ~30s (44k backjumps) with this feature.

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?

[AntoniusW]

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.

[rtaupe]

What is the status on this PR and #284 ?

The status has not changed since Dec 16, 2020, I have not done any additional performance analysis since then.