Abstract Electoral control types are ways of trying to change the outcome of elections by altering aspects of their composition and structure [6]. We say two compatible (i.e., having the same input types) control types that are about the same election system $$\mathcal {E}$$ 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 (see the Preliminaries for a more formal definition) [31]. For each of the seven general (i.e., holding for all election systems) electoral control type collapsing pairs found by Hemaspaandra, Hemaspaandra, and Menton [31] and for each of the additional electoral control type collapsing pairs of Carleton et al. [10] 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 [31] and Carleton et al. [10], 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.

Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still several notable limitations. First, GKAT is completely agnostic with respect to the meaning of primitives, to keep equivalence decidable. Second, GKAT excludes non-local control flow such as goto, break , and return . To overcome these limitations, we introduce Control-Flow GKAT (CF-GKAT) , a system that allows reasoning about programs that include non-local control flow as well as hardcoded values. CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the nearly-linear efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT’s abilities, we validated the output of several highly non-trivial program transformations, such as Erosa and Hendren’s goto -elimination procedure and the output of Ghidra decompiler. CF-GKAT opens up the application of Kleene Algebra to a wider set of challenges, and provides an important verification tool that can be applied to the field of decompilation and control-flow transformation.

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.

Introductory assignments in CS Theory ask students to construct instances of various computational models (such as finite automata, regular expressions, context-free grammars, or push-down automata) for a given language. Verifying the correctness of their model instance is challenging for beginner CS Theory students since the concepts are abstract and there are infinitely many possible inputs. The popular JFLAP software allows students to visualize the running of their instance on a specific input. We recently developed a server extension to JFLAP which checks whether a student's instance is equivalent to the instructor's solution and, if not, it returns a "witness string,'' an input string on which the student's construction and the correct solution differ.

Computing theory is often perceived as challenging by students, and verifying the correctness of a student's automaton or grammar is time-consuming for instructors. Aiming to provide benefits to both students and instructors, we designed an automated feedback tool for assignments where students construct automata or grammars. Our tool, built as an extension to the widely popular JFLAP software, determines if a submission is correct, and for incorrect submissions it provides a "witness" string demonstrating the incorrectness.

Equivalence of deterministic finite automata (DFAs) has been researched for several decades, but equivalence of nondeterministic finite automata (NFAs) is not as studied. Equivalence of two NFAs is a PSPACE-complete problem. NFA equivalence is a challenging theoretical problem with practical applications such as lexical analysis. Quantified boolean formulas (QBFs) naturally encode PSPACE-complete problems, and we share our preliminary work towards determining NFA equivalence via QBFs.

Computing theory analyzes abstract computational models to rigorously study the computational difficulty of various problems. Introductory computing theory can be challenging for undergraduate students, and the overarching goal of our research is to help students learn these computational models. The most common pedagogical tool for interacting with these models is the Java Formal Languages and Automata Package (JFLAP). We developed a JFLAP server extension, which accepts homework submissions from students, evaluates the submission as correct or incorrect, and provides a witness string when the submission is incorrect. Our extension currently provides witness feedback for deterministic finite automata, nondeterministic finite automata, regular expressions, context-free grammars, and pushdown automata.

A backbone of a boolean formula F is a collection S of its variables for which there is a unique partial assignment aS such that F[aS] is satisfiable (Monasson et al. 1999; Williams, Gomes, and Selman 2003). This paper studies the nontransparency of backbones. We show that, under the widely believed assumption that integer factoring is hard, there exist sets of boolean formulas that have obvious, nontrivial backbones yet finding the values, aS, of those backbones is intractable. We also show that, under the same assumption, there exist sets of boolean formulas that obviously have large backbones yet producing such a backbone S is intractable. Further, we show that if integer factoring is not merely worst-case hard but is frequently hard, as is widely believed, then the frequency of hardness in our two results is not too much less than that frequency.

The purpose of this paper is to draw attention to a particular family of quantified Boolean formulas (QBFs) stemming from encodings of some vertex Folkman problems in extremal graph theory. We argue that this family of formulas is interesting for QSAT research because it is both conceptually simple and parametrized in a way that allows for a fine-grained diversity in the level of difficulty of its instances. Additionally, when coupled with symmetry breaking, the formulas in this family exhibit backbones (unique satisfying assignments) at the top-level existential variables. This benchmark is thus suitable for addressing questions regarding the connection between the existence of backbones and the hardness of QBFs.

Computing theory is an important part of computer science education, introducing students to computational models of increasing power to study possibilities and limitations of computation. The subject is, however, very abstract and mathematical, and students often struggle with it. Students must master various computational models, but there is often a lengthy delay from the time a model is introduced until a student gets feedback on their related assignment. During this time, the course has typically moved far ahead, and students become progressively more lost. To alleviate this problem, we developed a prototype of an automated feedback tool for CS theory, which extends the widely used JFLAP software. Our tool currently handles student submissions of deterministic and non-deterministic finite automata, regular expressions, context-free grammars, and push-down automata homework, where an instructor specifies the target language and the students receive immediate feedback on their submissions. Currently, for incorrect submissions, the feedback is in the form of a "witness'' string, specifying a string on which the submission fails. Beyond regular languages, our tool attempts to solve undecidable problems; fortunately, the undecidability does not occur on typical homework assignments. We are collecting preliminary evaluation data from students using the prototype tool in their course. In our future work, we will analyze the data, and we aim to produce automated partial credit (along with the witness feedback) using SAT and QBF solvers.

The last two decades have seen extraordinary advances in industrial applications of constraint satisfaction techniques, while combinatorial problems have been pushed to the sidelines. We propose a comprehensive analysis of the state of the art in constraint satisfaction problems when applied to combinatorial problems in areas such as graph theory, set theory, algebra, among others. We believe such a study will provide us with a deeper understanding about the limitations we still face in constraint satisfaction problems.

In the context of SAT solvers, Shatter is a popular tool for symmetry breaking on CNF formulas. Nevertheless, little has been said about its use in the context of AllSAT problems. AllSAT has gained much popularity in recent years due to its many applications in domains like model checking, data mining, etc. One example of a particularly transparent application of AllSAT to other fields of computer science is computational Ramsey theory. In this paper we study the effect of incorporating Shatter to the workflow of using Boolean formulas to generate all possible edge colorings of a graph avoiding prescribed monochromatic subgraphs. We identify two drawbacks in the naïve use of Shatter to break the symmetries of Boolean formulas encoding Ramsey-type problems for graphs.

A backbone of a boolean formula F is a collection S of its variables for which there is a unique partial assignment aS such that F[aS] is satisfiable (Monasson et al. 1999; Williams, Gomes, and Selman 2003). This paper studies the nontransparency of backbones. We show that, under the widely believed assumption that integer factoring is hard, there exist sets of boolean formulas that have obvious, nontrivial backbones yet finding the values, aS, of those backbones is intractable. We also show that, under the same assumption, there exist sets of boolean formulas that obviously have large backbones yet producing such a backbone S is intractable. Further, we show that if integer factoring is not merely worst-case hard but is frequently hard, as is widely believed, then the frequency of hardness in our two results is not too much less than that frequency.