Enable weak constraints

[AntoniusW]

Adds weak constraints to Alpha. The parser is able to read them and in their presence the solver switches to a branch-and-bound algorithm. Returned answer sets are adorned with a valuation (weights at different levels as specified by the weak constraints).

[AntoniusW]

This PR should be ready to be reviewed now.

[AntoniusW]

Now also with test passing. :-)

[madmike200590]

I'm not yet through with the complete review, but I think I found a bug in one my tests: The following program only has 4 answer sets with weak constraints:

{a; b; c}.

:~ a. [1]
:~ b. [2]
:~ c. [3]

Alpha output is:

michael@michael-laptop:~/asp_snippets/weak_constraints$ java -jar Alpha-bundled.jar -i wc-test.asp
  376 I lections.Reflections Reflections took 98 ms to scan 1 urls, producing 1 keys and 8 values  
Answer set 1:
{ a, c }
Optimization: [4@0]
Answer set 2:
{ c }
Optimization: [3@0]
Answer set 3:
{ a }
Optimization: [1@0]
Answer set 4:
{  }
Optimization: []
SATISFIABLE

Since I didn't specify any limit on answer sets computed, I'd expect to get all of them with their associated weigths. Is that a misunderstanding on my part?

The program without weak constraints, i.e. {a; b; c}. yields the expected 8 answer sets:

michael@michael-laptop:~/asp_snippets/weak_constraints$ java -jar Alpha-bundled.jar -i wc-test.asp
  399 I lections.Reflections Reflections took 110 ms to scan 1 urls, producing 1 keys and 8 values  
Answer set 1:
{ a, c }
Answer set 2:
{ c }
Answer set 3:
{ a }
Answer set 4:
{  }
Answer set 5:
{ a, b, c }
Answer set 6:
{ a, b }
Answer set 7:
{ b, c }
Answer set 8:
{ b }
SATISFIABLE

I haven't done any detailed analysis on this yet, but wanted to raise it anyway so you can take a look as well.

[AntoniusW]

To me that looks perfectly fine. The solver sees the weak constraints and switches over to optimisation using a branch-and-bound algorithm. That means branches whose valuation is higher than the currently-best-known valuation are cut off immediately and not expanded. So one usually expects a sequence of answer-sets with increasingly better valuation (i.e., less violations). Since the last answer-set has zero violated weak constraints (hence a valuation of 0 at all levels), it is the best answer-set and the solver stops there.

Note that this behaviour is similar to what other ASP solvers do. Enumerating all answer-sets is usually infeasible when optimization is enabled and by using optimization (i.e., weak constraints) one tells the solver that one is interested in good answers only.

[madmike200590]

To me that looks perfectly fine. The solver sees the weak constraints and switches over to optimisation using a branch-and-bound algorithm. That means branches whose valuation is higher than the currently-best-known valuation are cut off immediately and not expanded. So one usually expects a sequence of answer-sets with increasingly better valuation (i.e., less violations). Since the last answer-set has zero violated weak constraints (hence a valuation of 0 at all levels), it is the best answer-set and the solver stops there.

Note that this behaviour is similar to what other ASP solvers do. Enumerating all answer-sets is usually infeasible when optimization is enabled and by using optimization (i.e., weak constraints) one tells the solver that one is interested in good answers only.

As per our discussion last week, I think we need the following changes:

• default behavior when Alpha is called without a specific number of answer sets to compute: Same as for programs without weak constraints, this should enumerate all answer sets along with their respective weights (needed for development/debugging)
• manual initial bound for answer set search: Add a commandline flag "-mw"/"--maxWeight" that, when used in conjuction with "-n" (number of answer sets) instructs Alpha to find n answer sets where no answer set must exceed the given weight (i.e. use the value of mw as initial bound for branch&bound)
• bugfix: When Alpha finds an optimum solution, this should be reported textually (currently only says "SATISFIABLE", see above example)

[codecov[bot]]

Codecov Report

Base: 66.83% // Head: 67.32% // Increases project coverage by +0.49% :tada:

Coverage data is based on head (e7558d0) compared to base (3028684). Patch coverage: 73.55% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff              @@
##             master     #273      +/-   ##
============================================
+ Coverage     66.83%   67.32%   +0.49%     
- Complexity     2108     2286     +178     
============================================
  Files           184      195      +11     
  Lines          8379     8980     +601     
  Branches       1464     1583     +119     
============================================
+ Hits           5600     6046     +446     
- Misses         2411     2515     +104     
- Partials        368      419      +51     

Impacted Files	Coverage Δ
...-app/src/main/java/at/ac/tuwien/kr/alpha/Main.java	31.13% <0.00%> (-1.23%)	:arrow_down:
...kr/alpha/commons/programs/ASPCore2ProgramImpl.java	0.00% <0.00%> (ø)
...ien/kr/alpha/commons/programs/AbstractProgram.java	0.00% <0.00%> (ø)
...n/kr/alpha/commons/programs/NormalProgramImpl.java	0.00% <0.00%> (ø)
.../ac/tuwien/kr/alpha/commons/programs/Programs.java	0.00% <0.00%> (ø)
.../kr/alpha/commons/programs/atoms/AbstractAtom.java	33.33% <ø> (ø)
...r/alpha/commons/programs/rules/WeakConstraint.java	0.00% <0.00%> (ø)
...at/ac/tuwien/kr/alpha/core/solver/NaiveSolver.java	93.11% <0.00%> (-0.43%)	:arrow_down:
...uwien/kr/alpha/core/solver/WritableAssignment.java	76.92% <ø> (ø)
.../at/ac/tuwien/kr/alpha/commons/BasicAnswerSet.java	26.53% <33.33%> (+0.44%)	:arrow_up:
... and 32 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

:umbrella: View full report at Codecov.
:loudspeaker: Do you have feedback about the report comment? Let us know in this issue.

[madmike200590]

As per our discussion last week, I think we need the following changes:

• default behavior when Alpha is called without a specific number of answer sets to compute: Same as for programs without weak constraints, this should enumerate all answer sets along with their respective weights (needed for development/debugging)
• manual initial bound for answer set search: Add a commandline flag "-mw"/"--maxWeight" that, when used in conjuction with "-n" (number of answer sets) instructs Alpha to find n answer sets where no answer set must exceed the given weight (i.e. use the value of mw as initial bound for branch&bound)
• bugfix: When Alpha finds an optimum solution, this should be reported textually (currently only says "SATISFIABLE", see above example)

@AntoniusW I just noticed that this is still tagged as pending my review - have the aforementioned changes been made, i.e. can we move this forward?

[AntoniusW]

@AntoniusW I just noticed that this is still tagged as pending my review - have the aforementioned changes been made, i.e. can we move this forward?

@madmike200590, I think it is ready now. The functionality to not run optimization but still get valuations of answer sets should work now. An (exclusive) upper bound can also be set manually. Furthermore, current master has been merged and this branch now follows the modularization introduced in master. The code is ready for another round of reviews (and subsequent merging).