arXiv subjects

Michael Codish

Publications and source records attributed to Michael Codish.

At least 19 recordsLinked to original sources

arXiv2025

Breaking Symmetries with Involutions

Symmetry breaking for graphs and other combinatorial objects is notoriously hard. On the one hand, complete symmetry breaks are exponential in size. On the other hand, current, state-of-the-art, partial symmetry breaks are often considered too weak to be of practical use. Recently, the concept of graph patterns has been introduced and provides a concise representation for (large) sets of non-canonical graphs, i.e.\ graphs that are not lex-leaders and can be excluded from search. In particular, four (specific) graph patterns apply to identify about 3/4 of the set of all non-canonical graphs. Taking this approach further we discover that graph patterns that derive from permutations that are involutions play an important role in the construction of symmetry breaks for graphs. We take advantage of this to guide the construction of partial and complete symmetry breaking constraints based on graph patterns. The resulting constraints are small in size and strong in the number of symmetries they break.

cs.LO↗

arXiv2025

Complete Symmetry Breaking for Finite Models

This paper introduces a SAT-based technique that calculates a compact and complete symmetry-break for finite model finding, with the focus on structures with a single binary operation (magmas). Classes of algebraic structures are typically described as first-order logic formulas and the concrete algebras are models of these formulas. Such models include an enormous number of isomorphic, i.e. symmetric, algebras. A complete symmetry-break is a formula that has as models, exactly one canonical representative from each equivalence class of algebras. Thus, we enable answering questions about properties of the models so that computation and search are restricted to the set of canonical representations. For instance, we can answer the question: How many non-isomorphic semigroups are there of size $n$? Such questions can be answered by counting the satisfying assignments of a SAT formula, which already filters out non-isomorphic models. The introduced technique enables us calculating numbers of algebraic structures not present in the literature and going beyond the possibilities of pure enumeration approaches.

cs.LO↗

arXiv2025

Breaking Symmetries from a Set-Covering Perspective

We formalize symmetry breaking as a set-covering problem. For the case of breaking symmetries on graphs, a permutation covers a graph if applying it to the graph yields a smaller graph in a given order. Canonical graphs are those that cannot be made smaller by any permutation. A complete symmetry break is then a set of permutations that covers all non-canonical graphs. A complete symmetry break with a minimal number of permutations can be obtained by solving an optimal set-covering problem. The challenge is in the sizes of the corresponding set-covering problems and in how these can be tamed. The set-covering perspective on symmetry breaking opens up a range of new opportunities deriving from decades of studies on both precise and approximate techniques for this problem. Application of our approach leads to optimal LexLeader symmetry breaks for graphs of order $n\leq 10$ as well as to partial symmetry breaks which improve on the state-of-the-art.

cs.LO↗

arXiv2025

SAT-Based Techniques for Lexicographically Smallest Finite Models

This paper proposes SAT-based techniques to calculate a specific normal form of a given finite mathematical structure (model). The normal form is obtained by permuting the domain elements so that the representation of the structure is lexicographically smallest possible. Such a normal form is of interest to mathematicians as it enables easy cataloging of algebraic structures. In particular, two structures are isomorphic precisely when their normal forms are the same. This form is also natural to inspect as mathematicians have been using it routinely for many decades. We develop a novel approach where a SAT solver is used in a black-box fashion to compute the smallest representative. The approach constructs the representative gradually and searches the space of possible isomorphisms, requiring a small number of variables. However, the approach may lead to a large number of SAT calls and therefore we devise propagation techniques to reduce this number. The paper focuses on finite structures with a single binary operation (encompassing groups, semigroups, etc.). However, the approach is generalizable to arbitrary finite structures. We provide an implementation of the proposed algorithm and evaluate it on a variety of algebraic structures.

cs.LO↗

arXiv2018

A SAT Encoding for the $n$-Fractions Problem

This note describes a SAT encoding for the $n$-fractions puzzle which is problem 041 of the CSPLib. Using a SAT solver we obtain a solution for two of the six remaining open instances of this problem.

cs.DM↗

arXiv2017

Graphs with girth at least 5 with orders between 20 and 32

We prove properties of extremal graphs of girth 5 and order 20 <=v <= 32. In each case we identify the possible minimum and maximum degrees, and in some cases prove the existence of (non-trivial) embedded stars. These proofs allow for tractable search for and identification of all non isomorphic cases.

math.CO↗

arXiv2016

Logic Programming with Graph Automorphism: Integrating naut with Prolog (Tool Description)

This paper presents the plnauty~library, a Prolog interface to the nauty graph-automorphism tool. Adding the capabilities of nauty to Prolog combines the strength of the "generate and prune" approach that is commonly used in logic programming and constraint solving, with the ability to reduce symmetries while reasoning over graph objects. Moreover, it enables the integration of nauty in existing tool-chains, such as SAT-solvers or finite domain constraints compilers which exist for Prolog. The implementation consists of two components: plnauty, an interface connecting \nauty's C library with Prolog, and plgtools, a Prolog framework integrating the software component of nauty, called gtools, with Prolog. The complete tool is available as a SWI-Prolog module. We provide a series of usage examples including two that apply to generate Ramsey graphs. This paper is under consideration for publication in TPLP.

cs.DS↗

arXiv2015

Breaking Symmetries in Graph Search with Canonizing Sets

There are many complex combinatorial problems which involve searching for an undirected graph satisfying given constraints. Such problems are often highly challenging because of the large number of isomorphic representations of their solutions. This paper introduces effective and compact, complete symmetry breaking constraints for small graph search. Enumerating with these symmetry breaks generates all and only non-isomorphic solutions. For small search problems, with up to $10$ vertices, we compute instance independent symmetry breaking constraints. For small search problems with a larger number of vertices we demonstrate the computation of instance dependent constraints which are complete. We illustrate the application of complete symmetry breaking constraints to extend two known sequences from the OEIS related to graph enumeration. We also demonstrate the application of a generalization of our approach to fully-interchangeable matrix search problems.

cs.AI↗

arXiv2015

Computing the Ramsey Number R(4,3,3) using Abstraction and Symmetry breaking

The number $R(4,3,3)$ is often presented as the unknown Ramsey number with the best chances of being found "soon". Yet, its precise value has remained unknown for almost 50 years. This paper presents a methodology based on \emph{abstraction} and \emph{symmetry breaking} that applies to solve hard graph edge-coloring problems. The utility of this methodology is demonstrated by using it to compute the value $R(4,3,3)=30$. Along the way it is required to first compute the previously unknown set ${\cal R}(3,3,3;13)$ consisting of 78{,}892 Ramsey colorings.

cs.AI↗

arXiv2015

When Six Gates are Not Enough

We apply the pigeonhole principle to show that there must exist Boolean functions on 7 inputs with a multiplicative complexity of at least 7, i.e., that cannot be computed with only 6 multiplications in the Galois field with two elements.

cs.CC↗

arXiv2015

Sorting Networks: to the End and Back Again

This paper studies new properties of the front and back ends of a sorting network, and illustrates the utility of these in the search for new bounds on optimal sorting networks. Search focuses first on the "outsides" of the network and then on the inner part. All previous works focus only on properties of the front end of networks and on how to apply these to break symmetries in the search. The new, out-side-in, properties help shed understanding on how sorting networks sort, and facilitate the computation of new bounds on optimal sorting networks. We present new parallel sorting networks for 17 to 20 inputs. For 17, 19, and 20 inputs these networks are faster than the previously known best networks. For 17 inputs, the new sorting network is shown optimal in the sense that no sorting network using less layers exists.

cs.DS↗

arXiv2015

Applying Sorting Networks to Synthesize Optimized Sorting Libraries

This paper shows an application of the theory of sorting networks to facilitate the synthesis of optimized general purpose sorting libraries. Standard sorting libraries are often based on combinations of the classic Quicksort algorithm with insertion sort applied as the base case for small fixed numbers of inputs. Unrolling the code for the base case by ignoring loop conditions eliminates branching and results in code which is equivalent to a sorting network. This enables the application of further program transformations based on sorting network optimizations, and eventually the synthesis of code from sorting networks. We show that if considering the number of comparisons and swaps then theory predicts no real advantage of this approach. However, significant speed-ups are obtained when taking advantage of instruction level parallelism and non-branching conditional assignment instructions, both of which are common in modern CPU architectures. We provide empirical evidence that using code synthesized from efficient sorting networks as the base case for Quicksort libraries results in significant real-world speed-ups.

cs.DS↗

arXiv2014

Optimal-Depth Sorting Networks

We solve a 40-year-old open problem on the depth optimality of sorting networks. In 1973, Donald E. Knuth detailed, in Volume 3 of "The Art of Computer Programming", sorting networks of the smallest depth known at the time for n =< 16 inputs, quoting optimality for n =< 8. In 1989, Parberry proved the optimality of the networks with 9 =< n =< 10 inputs. In this article, we present a general technique for obtaining such optimality results, and use it to prove the optimality of the remaining open cases of 11 =< n =< 16 inputs. We show how to exploit symmetry to construct a small set of two-layer networks on n inputs such that if there is a sorting network on n inputs of a given depth, then there is one whose first layers are in this set. For each network in the resulting set, we construct a propositional formula whose satisfiability is necessary for the existence of a sorting network of a given depth. Using an off-the-shelf SAT solver we show that the sorting networks listed by Knuth are optimal. For n =< 10 inputs, our algorithm is orders of magnitude faster than the prior ones.

cs.DS↗

arXiv2014

Sorting Networks: the End Game

This paper studies properties of the back end of a sorting network and illustrates the utility of these in the search for networks of optimal size or depth. All previous works focus on properties of the front end of networks and on how to apply these to break symmetries in the search. The new properties help shed understanding on how sorting networks sort and speed-up solvers for both optimal size and depth by an order of magnitude.

cs.DS↗

arXiv2014

Solving Graph Coloring Problems with Abstraction and Symmetry

This paper introduces a general methodology, based on abstraction and symmetry, that applies to solve hard graph edge-coloring problems and demonstrates its use to provide further evidence that the Ramsey number $R(4,3,3)=30$. The number $R(4,3,3)$ is often presented as the unknown Ramsey number with the best chances of being found "soon". Yet, its precise value has remained unknown for more than 50 years. We illustrate our approach by showing that: (1) there are precisely 78{,}892 $(3,3,3;13)$ Ramsey colorings; and (2) if there exists a $(4,3,3;30)$ Ramsey coloring then it is (13,8,8) regular. Specifically each node has 13 edges in the first color, 8 in the second, and 8 in the third. We conjecture that these two results will help provide a proof that no $(4,3,3;30)$ Ramsey coloring exists implying that $R(4,3,3)=30$.

cs.AI↗

arXiv2014

Twenty-Five Comparators is Optimal when Sorting Nine Inputs (and Twenty-Nine for Ten)

This paper describes a computer-assisted non-existence proof of nine-input sorting networks consisting of 24 comparators, hence showing that the 25-comparator sorting network found by Floyd in 1964 is optimal. As a corollary, we obtain that the 29-comparator network found by Waksman in 1969 is optimal when sorting ten inputs. This closes the two smallest open instances of the optimal size sorting network problem, which have been open since the results of Floyd and Knuth from 1966 proving optimality for sorting networks of up to eight inputs. The proof involves a combination of two methodologies: one based on exploiting the abundance of symmetries in sorting networks, and the other, based on an encoding of the problem to that of satisfiability of propositional logic. We illustrate that, while each of these can single handed solve smaller instances of the problem, it is their combination which leads to an efficient solution for nine inputs.

cs.DM↗

arXiv2014

The Quest for Optimal Sorting Networks: Efficient Generation of Two-Layer Prefixes

Previous work identifying depth-optimal $n$-channel sorting networks for $9\leq n \leq 16$ is based on exploiting symmetries of the first two layers. However, the naive generate-and-test approach typically applied does not scale. This paper revisits the problem of generating two-layer prefixes modulo symmetries. An improved notion of symmetry is provided and a novel technique based on regular languages and graph isomorphism is shown to generate the set of non-symmetric representations. An empirical evaluation demonstrates that the new method outperforms the generate-and-test approach by orders of magnitude and easily scales until $n=40$.

cs.DS↗

arXiv2014

Boolean Equi-propagation for Concise and Efficient SAT Encodings of Combinatorial Problems

We present an approach to propagation-based SAT encoding of combinatorial problems, Boolean equi-propagation, where constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. A key factor is that considering only a small fragment of a constraint model at one time enables us to apply stronger, and even complete, reasoning to detect equivalent literals in that fragment. Once detected, equivalences apply to simplify the entire constraint model and facilitate further reasoning on other fragments. Equi-propagation in combination with partial evaluation and constraint simplification provide the foundation for a powerful approach to SAT-based finite domain constraint solving. We introduce a tool called BEE (Ben-Gurion Equi-propagation Encoder) based on these ideas and demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.

cs.AI↗