  Multiwinner voting rules can be used to select a fixed-size committee from a
larger set of candidates. We consider approval-based committee rules, which
allow voters to approve or disapprove candidates. In this setting, several
voting rules such as Proportional Approval Voting (PAV) and Phragm\'en's rules
have been shown to produce committees that are proportional, in the sense that
they proportionally represent voters' preferences; all of these rules are
strategically manipulable by voters. On the other hand, a generalisation of
Approval Voting gives a non-proportional but strategyproof voting rule. We show
that there is a fundamental tradeoff between these two properties: we prove
that no multiwinner voting rule can simultaneously satisfy a weak form of
proportionality (a weakening of justified representation) and a weak form of
strategyproofness. Our impossibility is obtained using a formulation of the
problem in propositional logic and applying SAT solvers; a human-readable
version of the computer-generated proof is obtained by extracting a minimal
unsatisfiable set (MUS). We also discuss several related axiomatic questions in
the domain of committee elections.
