potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
615 stars 81 forks source link

Understanding aggregates: restricting the number of ground rules. #351

Closed SeSodesa closed 2 years ago

SeSodesa commented 2 years ago

Hello.

I am in the process of trying to understand Clingo's aggregates via the following exercise:

Let us consider an election where n persons indicate top three among m candidates. Besides the parameters n and m, you may assume that persons and candidates have been defined in terms of predicates person/1 and candidate/1. Please define the following predicates using these:

  1. rank(P,R,C): person P chooses a rank R=1..3 to some unique candidate C.
  2. score(C,S): candidate C receives a point score S based on the rankings: a. each rank 1 is worth three points, b. each rank 2 is worth two points, and c. each rank 3 is worth one point.
  3. elected(C): candidate C is elected if (s)he received the highest score among all candidates.

In case of a draw, no candidate is elected.

I have implemented the first predicate as follows:

% Basic definitions.

#const n = 4.
#const m = 4.
person(1..n).
candidate(1..m).

% Person P chooses a (single) rank R ∈ 1..3 to a unique candidate C.

{ rank(P, R, C) : R=1..3 } = 1
:-
    person(P),
    candidate(C)
.

% Count the number of votes each person gave

votesperp(P, V)
:-
    person(P),
    V =
    % 3 <
    #count {
        C:
            candidate(C),
            rank(P, _, C)
    }
.

Now all is fine and good, as long as I don't comment out the line votesperp(P, V):

λ clingo -cn=5 -cm=3 round5.exercise5.lp
clingo version 5.4.0
Reading from round5.exercise5.lp
Solving...
Answer: 1
rank(1,2,1) rank(1,1,2) rank(1,1,3) votesperp(1,3) rank(2,1,1) rank(2,3,2)
rank(2,3,3) votesperp(2,3) rank(3,3,1) rank(3,3,2) rank(3,2,3)
votesperp(3,3) rank(4,1,1) rank(4,2,2) rank(4,3,3) votesperp(4,3)
rank(5,2,1) rank(5,3,2) rank(5,2,3) votesperp(5,3)
SATISFIABLE

Models       : 1+
Calls        : 1
Time         : 0.003s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.003s

Each person votes for all candidates exactly once, fulfilling the uniqueness condition. However, when I try to use the votesperp/2 construct to restrict the number of candidates each person votes for like this

:-
    person(P),
    3 < #count {
        C:
            candidate(C),
            rank(P, _, C)
    }
.

then the following happens:

λ clingo -cn=4 -cm=4 round5.exercise5.lp
clingo version 5.4.0
Reading from round5.exercise5.lp

Solving...
UNSATISFIABLE

Models       : 0
Calls        : 1
Time         : 0.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.002s

Why cannot I restrict the number of votes to 3 per person like this? Thanks for any assistance.

rkaminsk commented 2 years ago

I am not sure what you are after with the rank. For the votes per person rule you can simply project it out. Then, your encoding is equivalent to the following:

#const n = 4.
#const m = 4.
person(1..n).
candidate(1..m).

% Person P chooses a (single) rank R ∈ 1..3 to a unique candidate C.

rank(P,C) :- person(P), candidate(C).

% Count the number of votes each person gave

votesperp(P,V) :- person(P), V = #count { C: candidate(C), rank(P,C) }.

Maybe you want to use <= 1 as a guard for the aggregate when guessing the rank?

SeSodesa commented 2 years ago

I am not sure what you are after with the rank.

The idea is that we have a ranked-choice voting system, and the voter gives their preference per election candidate, with number 1 being the most preferrable and rank 3 signifying the least preferrable candidate. Therefore I need a numerical value stored in there somewhere.

I then reverse those later with

points(P, 3, C) :- rank(P, 1, C).
points(P, 2, C) :- rank(P, 2, C).
points(P, 1, C) :- rank(P, 3, C).

and calculate a score as the sum of the points per candidate:

score(C, S)
:-
    candidate(C),
    S = #sum {
        Poi, P:
            person(P),
            points(P, Poi, C)
    }
.

The person with the highest score is then elected, if there is no draw:

% If there is a draw, the candidates involved cannot get elected.

draw(C1, C2)
:-
    candidate(C1),
    candidate(C2),
    C1 != C2,
    score(C1, S1),
    score(C2, S2),
    S1 = S2
.

% The candidate with the highest score gets elected.

elected(C)
:-
    candidate(C),
    score(C, S),
    S = #max {
        Sco, Can:
            score(Can, Sco)
    },
    not draw(C, C2) : candidate(C2)
.

However, this does not seem to produce the exact results I want, possibly because a single person P is able to vote for more than 3 candidates C.

rkaminsk commented 2 years ago

Is the following what you intend?

rank(1..3).
{ rank(P,R,C) } :- person(P), rank(R), candidate(C).
% a person can give at most three votes
:- { rank(P,R,C) } > 3, person(P).
% a person can give at most one rank to a candidate
:- { rank(P,R,C) } > 1, person(P), candidate(C).
% a person can use each rank at most once
:- { rank(P,R,C) } > 1, person(P), rank(R).

This could also be written differently by first guessing a vote and then assigning a rank to the vote.

SeSodesa commented 2 years ago

Since I am trying to figure out aggregates, are those basically equivalent to

% a person can give at most three votes
:- 3 < #count { rank(P,R,C) }, person(P), candidate(C), rank(R).
% a person can give at most one rank to a candidate
:- 1 < #count { C : rank(P,R,C) }, person(P), candidate(C).
% a person can use each rank at most once
:- 1 < #count { R : rank(P,R,C) }, person(P), rank(R), candidate(C).

?

rkaminsk commented 2 years ago

It has to be

:- 3 < #count { R,C: rank(P,R,C) }, person(P).
% or equivalently
:- 3 < #count { R,C: rank(P,R,C), rank(R), candidate(C) }, person(P).

% a person can give at most one rank to a candidate
:- 1 < #count { R : rank(P,R,C) }, person(P), candidate(C).
% or equivalently
:- 1 < #count { R : rank(P,R,C), rank(R) }, person(P), candidate(C).

% a person can use each rank at most once
:- 1 < #count { C : rank(P,R,C) }, person(P), rank(R).
% or equivalently
:- 1 < #count { C : rank(P,R,C), candidate(C) }, person(P), rank(R).

I also like to write the bound on the right-hand-side because I find term relation constant easier to read. Except for assignments where I prefer variable equal term.

SeSodesa commented 2 years ago

Ah, alright. Reading the Potassco user manual somehow had me think that the lower bound always has to be on the left side, because of all the examples with

lower bound ⪯ α { tᵢ : 𝐋ᵢ } ⪯ upper bound

but it is somewhat of a relief if that is note the case.

rkaminsk commented 2 years ago

Historically, aggregates hat the form L { E } U without any relation symbols. The last revision of the guide is a bit dated and was still written with this mindset. Now, one can (and should) use relation symbols.

tortinator commented 2 years ago

Hi, just a remark from the off: This may have been a valuable discussion for our mailing list. @SeSodesa, in case you are interested feel free to subscribe here