  In party-approval multiwinner elections the goal is to allocate the seats of
a fixed-size committee to parties based on the approval ballots of the voters
over the parties. In particular, each voter can approve multiple parties and
each party can be assigned multiple seats. Two central requirements in this
setting are proportional representation and strategyproofness. Intuitively,
proportional representation requires that every sufficiently large group of
voters with similar preferences is represented in the committee.
Strategyproofness demands that no voter can benefit by misreporting her true
preferences. We show that these two axioms are incompatible for anonymous
party-approval multiwinner voting rules, thus proving a far-reaching
impossibility theorem. The proof of this result is obtained by formulating the
problem in propositional logic and then letting a SAT solver show that the
formula is unsatisfiable. Additionally, we demonstrate how to circumvent this
impossibility by considering a weakening of strategy\-proofness which requires
that only voters who do not approve any elected party cannot manipulate. While
most common voting rules fail even this weak notion of strategyproofness, we
characterize Chamberlin--Courant approval voting within the class of Thiele
rules based on this strategyproofness notion.
