Electoral control types are ways of trying to change the outcome of elections by altering aspects of their composition and structure [BTT92]. We say two compatible (i.e., having the same input types) control types that are about the same election system E form a collapsing pair if for every possible input (which typically consists of a candidate set, a vote set, a focus candidate, and sometimes other parameters related to the nature of the attempted alteration), either both or neither of the attempted attacks can be successfully carried out. For each of the seven general (i.e., holding for all election systems) electoral control type collapsing pairs found by Hemaspaandra, Hemaspaandra, and Menton [HHM20] and for each of the additional electoral control type collapsing pairs of Carleton et al. [CCH+ 22] for veto and approval (and many other election systems in light of that paper's Theorems 3.6 and 3.9), both members of the collapsing pair have the same complexity since as sets they are the same set. However, having the same complexity (as sets) is not enough to guarantee that as search problems they have the same complexity. In this paper, we explore the relationships between the search versions of collapsing pairs. For each of the collapsing pairs of Hemaspaandra, Hemaspaandra, and Menton [HHM20] and Carleton et al. [CCH+ 22], we prove that the pair's members' search-version complexities are polynomially related (given access, for cases when the winner problem itself is not in polynomial time, to an oracle for the winner problem). Beyond that, we give efficient reductions that from a solution to one compute a solution to the other. For the concrete systems plurality, veto, and approval, we completely determine which of their (due to our results) polynomially-related collapsing search-problem pairs are polynomial-time computable and which are NP-hard.
Electoral control refers to attacking elections by adding, deleting, or partitioning voters or candidates. Hemaspaandra, Hemaspaandra, and Menton recently discovered, for seven pairs (T, T′) of seemingly distinct standard electoral control types, that T and T′ are in practice identical: For each input I and each election system E, I is a “yes” instance of both T and T′ under E, or of neither. Surprisingly, this had previously gone undetected even as the field was score-carding how many standard control types various election systems were resistant to; various “different” cells on such score cards were, unknowingly, duplicate effort on the same issue. This naturally raises the worry that perhaps other pairs of control types are identical, and so work still is being needlessly duplicated. We completely determine, for all standard control types, which pairs are, for elections whose votes are linear orderings of the candidates, always identical. In particular, we prove that no identical control pairs exist beyond the known seven. We also for three central election systems completely determine which control pairs are identical (“collapse”) with respect to those particular election systems, and we also explore containment and incomparability relationships between control pairs. For approval voting, which has a different “type” for its votes, Hemaspaandra, Hemaspaandra, and Menton’s seven collapses still hold (since we observe that their argument applies to all election systems). However, we find 14 additional collapses that hold for approval voting but do not hold for some election systems whose votes are linear orderings of the candidates. We find one new collapse for veto elections and none for plurality. We prove that each of the three election systems mentioned have no collapses other than those inherited from Hemaspaandra, Hemaspaandra, and Menton or added in the present paper. We establish many new containment relationships between separating control pairs, and for each separating pair of standard control types classify its separation in terms of either containment (always, and strict on some inputs) or incomparability. Our work, for the general case and these three important election systems, clarifies the landscape of the 44 standard control types, for each pair collapsing or separating them, and also providing finer-grained information on the separations.
We present eMOP, a tool for incremental runtime verification (RV) of test executions during software evolution. We previously used RV to find hundreds of bugs in open-source projects by monitoring passing tests against formal specifications of Java APIs. We also proposed evolution-aware techniques to reduce RV ’s runtime overhead and human time to inspect specification violations. eMOP brings these benefits to developers in a tool that seamlessly integrates with the Maven build system. We describe eMOP ’s design, implementation, and usage. We evaluate eMOP on 676 versions of 21 projects, including those from our earlier prototypes’ evaluation. eMOP is up to 8.4 × faster and shows up to 31.3 × fewer violations, compared to running RV from scratch after each code change. eMOP also does not miss new violations in our evaluation, and it is open-sourced at https://github.com/SoftEngResearch/emop .
In this paper we critique Keum-Bae Cho's proof that $\mathrm{P} \subsetneq \mathrm{NP}$. This proof relates instances of 3-SAT to indistinguishable binomial decision trees and claims that no polynomial-time algorithm can solve 3-SAT instances represented by these trees. We argue that their proof fails to justify a crucial step, and so the proof does not establish that $\mathrm{P} \subsetneq \mathrm{NP}$.