Abstract Nielsen transformations form the basis of a simple and widely used procedure for solving word equations. We make progress on the problem of determining when this procedure terminates in the presence of length constraints. To do this, we introduce extended word equations , a mathematical model of a word equation with partial information about length constraints. We then define extended Nielsen transformations , which adapt Nielsen transformations to the setting of extended word equations. We provide a partial characterization of when repeatedly applying extended Nielsen transformations to an extended word equation is guaranteed to terminate.

Abstract We consider the closure of three classical combination properties, namely, stable infiniteness, gentleness and shininess (or, equivalently for decidable theories, strong politeness), under intersection and combinability. We compute every possible intersection, and then compute the maximal set of theories that can be combined with each resulting intersection. We iterate this process until no new sets are identified. How many properties will we end up with?

We present several novel encodings for cardinality constraints, which use fewer clauses than previous encodings and, more importantly, introduce new generally applicable techniques for constructing compact encodings. First, we present a CNF encoding for the AtMostOne(x_1,…,x_n) constraint using 2n + 2 √{2n} + O(∛n) clauses, thus refuting the conjectured optimality of Chen’s product encoding. Our construction also yields a smaller monotone circuit for the threshold-2 function, improving on a 50-year-old construction of Adleman and incidentally solving a long-standing open problem in circuit complexity. On the other hand, we show that any encoding for this constraint requires at least 2n + √{n+1} - 2 clauses, which is the first nontrivial unconditional lower bound for this constraint and answers a question of Kučera, Savický, and Vorel. We then turn our attention to encodings of AtMost_k(x_1,…,x_n), where we introduce grid compression, a technique inspired by hash tables, to give encodings using 2n + o(n) clauses as long as k = o(∛{n}) and 4n + o(n) clauses as long as k = o(n). Previously, the smallest known encodings were of size (k+1)n + o(n) for k ≤ 5 and 7n - o(n) for k ≥ 6.

Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can be constructed by an idealized BVA algorithm. Based on this insight, we prove new results about the behavior and limitations of BVA and its interaction with other preprocessing techniques. We show that idealized BVA, plus some minor additional preprocessing (e.g., equivalent literal substitution), can reencode any 2-CNF formula with n variables into an equivalent 2-CNF formula with (lg(3)/4 + o(1)) n²/(lg n) clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from lg(3)/4 ≈ 0.396 to 1, and that no reencoding method can achieve a constant below 0.25. On the other hand, for the at-most-one constraint on n variables, we prove that idealized BVA cannot reencode this constraint using fewer than 3n-6 clauses, a bound that we prove is achieved by actual implementations. In particular, this shows that the product encoding for at-most-one, which uses 2n+o(n) clauses, cannot be constructed by BVA regardless of the heuristics used. Finally, our graph-theoretic characterization of BVA allows us to leverage recent work in algorithmic graph theory to develop a drastically more efficient implementation of BVA that achieves a comparable clause reduction on random monotone 2-CNF formulas.

We study the problem of partitioning the edges of a d-uniform hypergraph H into a family F of complete d-partite hypergraphs (d-cliques). We show that there is a partition F in which every vertex v ∈ V(H) belongs to at most (1/d! + od(1))nd−1/lgn members of F. This settles the central question of a line of research initiated by Erdős and Pyber (1997) for graphs, and more recently by Csirmaz, Ligeti, and Tardos (2014) for hypergraphs. The d=2 case of this theorem answers a 40-year-old question of Chung, Erdős, and Spencer (1983). An immediate corollary of our result is an improved upper bound for the maximum share size for binary secret sharing schemes on uniform hypergraphs.

We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describe a Galois connection between sets of decidable theories, which picks out the largest set of decidable theories that can be combined with a given set of decidable theories. Using this, we exactly characterize the sets of decidable theories that can be combined with those satisfying well-known theory combination properties. This strengthens previous results and answers in the negative several long-standing open questions about the possibility of improving existing theory combination methods to apply to larger sets of theories. Additionally, the Galois connection gives rise to a complete lattice of theory combination properties, which allows one to generate new theory combination methods by taking meets and joins of elements of this lattice. We provide examples of this process, introducing new combination theorems. We situate both new and old combination methods within this lattice.

Abstract In the Nelson–Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and the other has to satisfy a similar yet weaker property; in shiny combination, only one has to be shiny (smooth, with a computable minimal model function and the finite model property); and for polite combination, only one has to be strongly polite (smooth and strongly finitely witnessable). For each combination method, we prove that if any of its assumptions are removed, then there is no general method to combine an arbitrary pair of theories satisfying the remaining assumptions. We also prove new theory combination results that weaken the assumptions of gentle and shiny combination.

Abstract Stable infiniteness, strong finite witnessability, and smoothness are model-theoretic properties relevant to theory combination in satisfiability modulo theories. Theories that are strongly finitely witnessable and smooth are called strongly polite and can be effectively combined with other theories. Toledo, Zohar, and Barrett conjectured that stably infinite and strongly finitely witnessable theories are smooth and therefore strongly polite. They called counterexamples to this conjecture unicorn theories, as their existence seemed unlikely. We prove that, indeed, unicorns do not exist. We also prove versions of the Löwenheim–Skolem theorem and the Łoś–Vaught test for many-sorted logic.