Formal methods in computer science aim to increase reliability and robustness of software or hardware designs. Unfortunately, formal methods are typically only accessible to specialized professionals. One of the reasons of this limited accessibility is the lack of exposure to formal methods in undergraduate education, even for computer science majors. We aim to rectify this by developing self-contained, turnkey Jupyter notebooks that will introduce students to SMT solvers, an important tool in formal methods, to solve problems related to their courses. This allows students to explore formal methods while not distracting from their coursework. In this work, we report on four Jupyter notebooks that we developed and deployed for this purpose.

Approval-Based Committee (ABC) rules are an important tool for choosing a fair set of candidates when given the preferences of a collection of voters. Though finding a winning committee for many ABC rules is NP-hard, natural variations for these rules with polynomial-time algorithms exist. The recently introduced Method of Equal Shares, an important ABC rule with desirable properties, is also computable in polynomial time. However, when working with very large elections, polynomial time is not enough and parallelization may be necessary. We show that computing a winning committee using these polynomial-time ABC rules (including the Method of Equal Shares) is P-hard, thus showing they cannot be parallelized. In contrast, we show that finding a winning committee can be parallelized when the votes are single-peaked or single-crossing for the important ABC rule Chamberlin-Courant.

Determining the complexity of election attack problems is a major research direction in the computational study of voting problems. The paper “Towards completing the puzzle: complexity of control by replacing, adding, and deleting candidates or voters” by Erdélyi et al. (JAAMAS 2021) provides a comprehensive study of the complexity of control problems. The sole open problem is constructive control by replacing voters for 2-Approval. We show that this case is in P, strengthening the recent RP (randomized polynomial-time) upper bound due to Fitzsimmons and Hemaspaandra (IJCAI 2022). We show this by transforming 2-Approval CCRV to weighted matching. We also use this approach to show that priced bribery for 2-Veto elections is in P. With this result, and the accompanying (unsurprising) result that priced bribery for 3-Veto elections is NP-complete, this settles the complexity for k-Approval and k-Veto standard control and bribery cases.

The first step in classifying the complexity of an NP problem is typically showing the problem in P or NP-complete. This has been a successful first step for many problems, including voting problems. However, in this paper we show that this may not always be the best first step. We consider the problem of constructive control by replacing voters (CCRV) introduced by Loreggia et al. [2015, https://dl.acm.org/doi/10.5555/2772879.2773411] for the scoring rule First-Last, which is defined by (1, 0, ..., 0, -1). We show that this problem is equivalent to Exact Perfect Bipartite Matching, and so CCRV for First-Last can be determined in random polynomial time. So on the one hand, if CCRV for First-Last is NP-complete then RP = NP, which is extremely unlikely. On the other hand, showing that CCRV for First-Last is in P would also show that Exact Perfect Bipartite Matching is in P, which would solve a well-studied 40-year-old open problem. Considering RP as an option for classifying problems can also help classify problems that until now had escaped classification. For example, the sole open problem in the comprehensive table from Erdélyi et al. [2021, https://doi.org/10.1007/s10458-021-09523-9] is CCRV for 2-Approval. We show that this problem is in RP, and thus easy since it is widely assumed that P = RP.

We study a model of proxy voting where the candidates, voters, and proxies are all located on the real line, and instead of voting directly, each voter delegates its vote to the closest proxy. The goal is to find a set of proxies that is theta-representative, which entails that for any voter located anywhere on the line, its favorite candidate is within a distance theta of the favorite candidate of its closest proxy. This property guarantees a strong form of representation as the set of voters is not required to be fixed in advance, or even be finite. We show that for candidates located on a line, an optimal proxy arrangement can be computed in polynomial time. Moreover, we provide upper and lower bounds on the number of proxies required to form a theta-representative set, thus showing that a relatively small number of proxies is enough to capture the preferences of any set of voters. An additional beneficial property of a theta-representative proxy arrangement is that for strict-Condorcet voting rules, the outcome of proxy voting is similarly close to the outcome of direct voting.

The computational study of election problems generally focuses on questions related to the winner or set of winners of an election. But social preference functions such as Kemeny rule output a full ranking of the candidates (a consensus). We study the complexity of consensus-related questions, with a particular focus on Kemeny and its qualitative version Slater. The simplest of these questions is the problem of determining whether a ranking is a consensus, and we show that this problem is coNP-complete. We also study the natural question of the complexity of manipulative actions that have a specific consensus as a goal. Though determining whether a ranking is a Kemeny consensus is hard, the optimal action for manipulators is to simply vote their desired consensus. We provide evidence that this simplicity is caused by the combination of election system (Kemeny), manipulative action (manipulation), and manipulative goal (consensus). In the process we provide the first completeness results at the second level of the polynomial hierarchy for electoral manipulation and for optimal solution recognition.

Voting rules based on scores generally determine the winner by computing the score of each candidate and the winner is the candidate with the best score. It would be natural to expect that computing the winner of an election is at least as hard as computing the score of a candidate. We show that this is not always the case. In particular, we show that for Young elections for dichotomous preferences the winner problem is easy, while determining the score of a candidate is hard. This complexity behavior has not been seen before and is unusual. The easiness of the winner problem for dichotomous Young crucially uses the fact that dichotomous preferences guarantee the transitivity of the majority relation. In addition to dichotomous preferences we also look at single-peaked preferences, the most well-studied domain restriction that guarantees the transitivity of the majority relation. We show that for the three major hard voting rules and their natural variants, dichotomous Young is the only case where winner is easy and score is hard. This also solves an open question from Lackner and Peters (AAAI 2017), by providing a polynomial-time algorithm for Dodgson score for single-peaked electorates.

While manipulative attacks on elections have been well-studied, only recently has attention turned to attacks that account for geographic information, which are extremely common in the real world. The most well known in the media is gerrymandering, in which district border-lines are changed to increase a party's chance to win, but a different geographical manipulation involves influencing the election by selecting the location of polling places, as many people are not willing to go to any distance to vote. In this paper we initiate the study of this manipulation. We find that while it is easy to manipulate the selection of polling places on the line, it becomes difficult already on the plane or in the case of more than two candidates. Moreover, we show that for more than two candidates the problem is inapproximable. However, we find a few restricted cases on the plane where some algorithms perform well. Finally, we discuss how existing results for standard control actions hold in the geographic setting, consider additional control actions in the geographic setting, and suggest directions for future study.

Incomplete preferences are likely to arise in real-world preference aggregation scenarios. This paper deals with determining whether an incomplete preference profile is single-peaked. This is valuable information since many intractable voting problems become tractable given singlepeaked preferences. We prove that the problem of recognizing single-peakedness is NP-complete for incomplete profiles consisting of partial orders. Despite this intractability result, we find several polynomial-time algorithms for reasonably restricted settings. In particular, we give polynomial-time recognition algorithms for weak orders, which can be viewed as preferences with indifference.

The computational study of elections generally assumes that the preferences of the electorate come in as a list of votes. Depending on the context, it may be much more natural to represent the preferences of the electorate succinctly, as the distinct votes and their counts. Though the succinct representation may be exponentially smaller than the nonsuccinct, we find only one natural case where the complexity increases, in sharp contrast to the case where each voter has a weight, where the complexity usually increases.