Searcharxiv⌕ Search

arXiv subjects

Curtis Bright

Publications and source records attributed to Curtis Bright.

At least 19 recordsLinked to original sources
arXiv2026

SMTpip: Interpreter-Aware SMT-Based Dependency Conflict Resolution for Restoring Python Source-Code Executability

Software developers rely on packages to reuse existing functionality instead of implementing everything from scratch. Python developers commonly provide package and interpreter dependencies using configuration files, such as requirements.txt or setup.py. Package managers in Python, such as pip, can install packages according to dependency and interpreter version constraints specified in configuration files. However, Python dependency resolution remains challenging: (1) different packages may require incompatible versions of the same dependency; (2) dependencies may require a Python interpreter version that is incompatible with the interpreter used for the project, making a valid environment impossible; and (3) pip, the most popular Python package manager, resolves conflicts via backtracking, repeatedly trying candidate versions without knowing whether a valid execution environment exists or not. To address these challenges, we present SMTpip, an interpreter-aware environment inference technique for improving the executability of Python source-code artifacts. SMTpip constructs a dependency knowledge graph using metadata stored in the Python Package Index (PyPI) that hosts millions of package releases, encodes both package version constraints and interpreter compatibility constraints specified in configuration files into Satisfiability Modulo Theories (SMT) formulas. Solving these formulas identifies a set of package versions and an interpreter version that jointly satisfy all declared constraints. Empirical evaluation on multiple datasets from open-source Python projects shows that SMTpip achieves substantial speedups -- $6.9\times$ over pip, $9.6\times$ over Conda, $3.2\times$ over smartPip, and $4\times$ over PyEGo -- while consistently producing constraint-consistent environments.

cs.SE↗
arXiv2026

Improving SAT Solvers on Orthogonal Latin Square Problems

Latin squares are $n\times n$ matrices containing $n$ symbols, where each symbol appears exactly once in each row and column. They were studied by Euler, later popularized through Sudoku, and remain a rich source of difficult combinatorial search problems. Two Latin squares are orthogonal mates if, when overlaid, no ordered pair of symbols repeats. Pairs of orthogonal Latin squares exist for every order except 2 and 6, but finding orthogonal Latin squares computationally can be challenging. Satisfiability (SAT) solvers are strong at combinatorial search and have been used to resolve a number of various kinds of orthogonal Latin square problems. On the other hand, SAT solvers lack domain knowledge about Latin squares, such as the Euler-Parker algorithm for orthogonal mate construction. In this paper, we propose a hybrid method combining a SAT solver with the Euler-Parker algorithm (implemented using a Diophantine system solver) and show that the resulting solver is effective at finding certain kinds of orthogonal Latin squares. For example, certain pairs of $10\times10$ orthogonal Latin squares whose existence was unknown for over 25 years were recently found by Bright, Keita, and Stevens using a SAT solver. The hardest cases could not be solved by the SAT solver CaDiCaL within seven days, but CaDiCaL augmented with an external Euler-Parker algorithm solves these cases in a median of around 5,100 seconds.

cs.DM↗
arXiv2026

SAT + NAUTY: Orderly Generation of Small Kochen-Specker Sets Containing the Smallest State-independent Contextuality Set

We present a search for small Kochen-Specker (KS) sets in dimension 3, specifically targeting extensions of the 13-ray Yu-Oh set, which has been proven to be the minimal witness to state-independent contextuality. To enable this search, we introduce a novel SAT-based orderly generation framework integrating recursive canonical labeling (RCL) with the graph isomorphism tool NAUTY. We demonstrate that previous SAT approaches relying on lexicographical canonicity suffer from exponential scaling on canonical graphs. This limitation renders them intractable on the large instances (25 to 33 vertices) encountered in our search, whereas our RCL check maintains consistent millisecond-level performance, effectively eliminating the bottleneck. Overcoming this bottleneck allows us to perform the first exhaustive enumeration of all KS sets with up to 33 rays containing the complete 25-ray state-independent contextuality (SI-C) set obtained by rigid extensions of the Yu-Oh set in 1,641 CPU hours. We found and verified that the 33-ray set discovered by Sch\"utte is the smallest three-dimensional KS set containing the complete 25-ray SI-C set. All non-existence results are backed by independently verifiable proof certificates via an extension of the DRAT proof format.

cs.LO↗
arXiv2026

Quaternionic Perfect Sequences and Hadamard Matrices

A finite sequence of numbers is perfect if it has zero periodic autocorrelation after a nontrivial cyclic shift. In this work, we study quaternionic perfect sequences having a one-to-one correspondence with the binary sequences arising in Williamson's construction of quaternion-type Hadamard matrices. Using this correspondence, we devise an enumeration algorithm that is significantly faster than previously used algorithms and does not require the sequences to be symmetric. We implement our algorithm and use it to enumerate all circulant and possibly non-symmetric Williamson-type matrices of orders up to 21; previously, the largest order exhaustively enumerated was 13. We prove that when the blocks of a quaternion-type Hadamard matrix are circulant, the blocks are necessarily pairwise amicable. This dramatically improves the filtering power of our algorithm: in order 20, the number of block pairs needing consideration is reduced by a factor of over 25,000. We use our results to construct quaternionic Hadamard matrices of interest in quantum communication and prove they are not equivalent to those constructed by other means. We also study the properties of quaternionic Hadamard matrices analytically, and demonstrate the feasibility of characterizing quaternionic Hadamard matrices with a fixed pattern of entries. These results indicate a richer set of properties and suggest an abundance of quaternionic Hadamard matrices for sufficiently large orders.

math.CO↗
arXiv2025

North-East Lattice Paths Avoiding $k$ Collinear Points via Satisfiability

We investigate the Gerver-Ramsey collinearity problem of determining the maximum number of points in a north-east lattice path without $k$ collinear points. Using a satisfiability solver, up to isomorphism we enumerate all north-east lattice paths avoiding $k$ collinear points for $k \leq 6$. We also find a north-east lattice path avoiding $k = 7$ collinear points with 327 steps, improving on the previous best length of 260 steps found by Shallit.

math.CO↗
arXiv2025

Orthogonal Latin Squares of Order Ten with Two Relations: A SAT Investigation

A $k$-net($n$) is a combinatorial design equivalent to $k-2$ mutually orthogonal Latin squares of order $n$. A relation in a net is a linear dependency over $\mathbb{F}_2$ in the incidence matrix of the net. A computational enumeration of all orthogonal pairs of Latin squares of order 10 whose corresponding nets have at least two nontrivial relations was achieved by Delisle in 2010 and verified by an independent search of Myrvold. In this paper, we confirm the correctness of their exhaustive enumerations with a satisfiability (SAT) solver approach instead of using custom-written backtracking code. Performing the enumeration using a SAT solver has at least three advantages. First, it reduces the amount of trust necessary, as SAT solvers produce independently-verifiable certificates that their enumerations are complete. These certificates can be checked by formal proof verifiers that are relatively simple pieces of software, and therefore easier to trust. Second, it is typically more straightforward and less error-prone to use a SAT solver over writing search code. Third, it can be more efficient to use a SAT-based approach, as SAT solvers are highly optimized pieces of software incorporating backtracking-with-learning for improving the efficiency of the backtracking search. For example, the SAT solver completely enumerates all orthogonal pairs of Latin squares of order ten with two nontrivial relations in under 2 hours on a desktop machine, while Delisle's 2010 search used 11,700 CPU hours. Although computer hardware was slower in 2010, this alone cannot explain the improvement in the efficiency of our SAT-based search.

math.CO↗
arXiv2025

Queen Domination by SAT Solving

The queen domination problem asks for the minimum number of queens required to attack all squares on an $n \times n$ chessboard. Once this optimal number is known, determining the number of distinct solutions up to isomorphism has also attracted considerable attention. Previous work has introduced specialized and highly optimized search procedures to address open instances of the problem. While efficient in terms of runtime, confidence in their computational results ultimately depends on the correctness of these specialized implementations, motivating approaches that additionally provide independently verifiable correctness certificates. To this end, we present a proof-producing SAT framework for the queen domination problem based on an encoding that introduces auxiliary variables representing whether rows, columns, diagonals, and anti-diagonals contain queens, thereby exposing the geometric structure of the problem to the SAT solver. The framework is further strengthened through a novel literal-ordering strategy, symmetry breaking, a modern Cube-and-Conquer framework, and a unified proof-generation and verification pipeline. Together, these techniques yield both high performance and independently verifiable correctness. Our results uncover and correct a discrepancy in the previously reported enumeration for $n=16$ and resolve the previously open case $n=19$.

cs.LO↗
arXiv2025

Symbolic Sets for Proving Bounds on Rado Numbers

Given a linear equation $\cal E$ of the form $ax + by = cz$ where $a$, $b$, $c$ are positive integers, the $k$-colour Rado number $R_k({\cal E})$ is the smallest positive integer $n$, if it exists, such that every $k$-colouring of the positive integers $\{1, 2, \dotsc, n\}$ contains a monochromatic solution to $\cal E$. In this paper, we consider $k = 3$ and the linear equations $ax + by = bz$ and $ax + ay = bz$. Using SAT solvers, we compute a number of previously unknown Rado numbers corresponding to these equations. We prove new general bounds on Rado numbers inspired by the satisfying assignments discovered by the SAT solver. Our proofs require extensive case-based analyses that are difficult to check for correctness by hand, so we automate checking the correctness of our proofs via an approach which makes use of a new tool we developed with support for operations on symbolically-defined sets -- e.g., unions or intersections of sets of the form $\{f(1), f(2), \dotsc, f(a)\}$ where $a$ is a symbolic variable and $f$ is a function possibly dependent on $a$. No computer algebra system that we are aware of currently has sufficiently capable support for symbolic sets, leading us to develop a tool supporting symbolic sets using the Python symbolic computation library SymPy coupled with the Satisfiability Modulo Theories solver Z3.

math.CO↗
arXiv2025

Myrvold's Results on Orthogonal Triples of $10 \times 10$ Latin Squares: A SAT Investigation

Ever since E. T. Parker constructed an orthogonal pair of $10\times10$ Latin squares in 1959, an orthogonal triple of $10\times10$ Latin squares has been one of the most sought-after combinatorial designs. Despite extensive work, the existence of such an orthogonal triple remains an open problem, though some negative results are known. In 1999, W. Myrvold derived some highly restrictive constraints in the special case in which one of the Latin squares in the triple contains a $4\times4$ Latin subsquare. In particular, Myrvold showed there were twenty-eight possible cases for an orthogonal pair in such a triple, twenty of which were removed from consideration. We implement a computational approach that quickly verifies all of Myrvold's nonexistence results and in the remaining eight cases finds explicit examples of orthogonal pairs -- thus explaining for the first time why Myrvold's approach left eight cases unsolved. As a consequence, the eight remaining cases cannot be removed by a strategy of focusing on the existence of an orthogonal pair; the third square in the triple must necessarily be considered as well. Our approach uses a Boolean satisfiability (SAT) solver to derive the nonexistence of twenty of the orthogonal pair types and find explicit examples of orthogonal pairs in the eight remaining cases. To reduce the existence problem into Boolean logic we use a duality between the concepts of transversal representation and orthogonal pair and we provide a formulation of this duality in terms of a composition operation on Latin squares. Using our SAT encoding, we find transversal representations (and equivalently orthogonal pairs) in the remaining eight cases in under two hours of computing on a large computing cluster.

math.CO↗
arXiv2025

Verified Certificates via SAT and Computer Algebra Systems for the Ramsey $R(3, 8)$ and $R(3, 9)$ Problems

The Ramsey problem $R(3, k)$ seeks to determine the smallest value of $n$ such that any red/blue edge coloring of the complete graph on $n$ vertices must either contain a blue triangle (3-clique) or a red clique of size $k$. Despite its significance, many previous computational results for the Ramsey $R(3, k)$ problem such as $R(3, 8)$ and $R(3, 9)$ lack formal verification. To address this issue, we use the software MathCheck to generate certificates for Ramsey problems $R(3, 8)$ and $R(3, 9)$ (and symmetrically $R(8, 3)$ and $R(9, 3)$) by integrating a Boolean satisfiability (SAT) solver with a computer algebra system (CAS). Our SAT+CAS approach significantly outperforms traditional SAT-only methods, demonstrating an improvement of several orders of magnitude in runtime. For instance, our SAT+CAS approach solves $R(3, 8)$ (resp., $R(8, 3)$) sequentially in 59 hours (resp., in 11 hours), while a SAT-only approach using state-of-the-art CaDiCaL solver times out after 7 days. Additionally, in order to be able to scale to harder Ramsey problems $R(3, 9)$ and $R(9, 3)$ we further optimized our SAT+CAS tool using a parallelized cube-and-conquer approach. Our results provide the first independently verifiable certificates for these Ramsey numbers, ensuring both correctness and completeness of the exhaustive search process of our SAT+CAS tool.

cs.LO↗
arXiv2024

New Results on Periodic Golay Pairs

In this paper, we provide algorithmic methods for conducting exhaustive searches for periodic Golay pairs. Our methods enumerate several lengths beyond the currently known state-of-the-art available searches: we conducted exhaustive searches for periodic Golay pairs of all lengths $v \leq 72$ using our methods, while only lengths $v \leq 34$ had previously been exhaustively enumerated. Our methods are applicable to periodic complementary sequences in general. We utilize sequence compression, a method of sequence generation derived in 2013 by Djokovi\'c and Kotsireas. We also introduce and implement a new method of "multi-level" compression, where sequences are uncompressed in several steps. This method allowed us to exhaustively search all lengths $v \leq 72$ using less than 10 CPU years. For cases of complementary sequences where uncompression is not possible, we introduce some new methods of sequence generation inspired by the isomorph-free exhaustive generation algorithm of orderly generation. Finally, we pose a conjecture regarding the structure of periodic Golay pairs and prove it holds in many lengths, including all lengths $v \lt 100$. We demonstrate the usefulness of our algorithms by providing the first ever examples of periodic Golay pairs of length $v = 90$. The smallest length for which the existence of periodic Golay pairs is undecided is now $106$.

cs.DM↗
arXiv2024

SHA-256 Collision Attack with Programmatic SAT

Cryptographic hash functions play a crucial role in ensuring data security, generating fixed-length hashes from variable-length inputs. The hash function SHA-256 is trusted for data security due to its resilience after over twenty years of intense scrutiny. One of its critical properties is collision resistance, meaning that it is infeasible to find two different inputs with the same hash. Currently, the best SHA-256 collision attacks use differential cryptanalysis to find collisions in simplified versions of SHA-256 that are reduced to have fewer steps, making it feasible to find collisions. In this paper, we use a satisfiability (SAT) solver as a tool to search for step-reduced SHA-256 collisions, and dynamically guide the solver with the aid of a computer algebra system (CAS) used to detect inconsistencies and deduce information that the solver would otherwise not detect on its own. Our hybrid SAT + CAS solver significantly outperformed a pure SAT approach, enabling us to find collisions in step-reduced SHA-256 with significantly more steps. Using SAT + CAS, we find a 38-step collision of SHA-256 with a modified initialization vector -- something first found by a highly sophisticated search tool of Mendel, Nad, and Schl\"affer. Conversely, a pure SAT approach could find collisions for no more than 28 steps. However, our work only uses the SAT solver CaDiCaL and its programmatic interface IPASIR-UP.

cs.CR↗
arXiv2024

SAT and Lattice Reduction for Integer Factorization

The difficulty of factoring large integers into primes is the basis for cryptosystems such as RSA. Due to the widespread popularity of RSA, there have been many proposed attacks on the factorization problem such as side-channel attacks where some bits of the prime factors are available. When enough bits of the prime factors are known, two methods that are effective at solving the factorization problem are satisfiability (SAT) solvers and Coppersmith's method. The SAT approach reduces the factorization problem to a Boolean satisfiability problem, while Coppersmith's approach uses lattice basis reduction. Both methods have their advantages, but they also have their limitations: Coppersmith's method does not apply when the known bit positions are randomized, while SAT-based methods can take advantage of known bits in arbitrary locations, but have no knowledge of the algebraic structure exploited by Coppersmith's method. In this paper we describe a new hybrid SAT and computer algebra approach to efficiently solve random leaked-bit factorization problems. Specifically, Coppersmith's method is invoked by a SAT solver to determine whether a partial bit assignment can be extended to a complete assignment. Our hybrid implementation solves random leaked-bit factorization problems significantly faster than either a pure SAT or pure computer algebra approach.

cs.CR↗
arXiv2024

AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems

This paper introduces AlphaMapleSAT, a Cube-and-Conquer (CnC) parallel SAT solver that integrates Monte Carlo Tree Search (MCTS) with deductive feedback to efficiently solve challenging combinatorial SAT problems. Traditional lookahead cubing methods, used by solvers such as March, limit their search depth to reduce overhead often resulting in suboptimal partitions. By contrast, AlphaMapleSAT performs a deeper MCTS search guided by deductive rewards from SAT solvers. This approach enables informed exploration of the cubing space while keeping cubing costs low. We demonstrate the efficacy of our technique via extensive evaluations against the widely used and established March cubing solver on three well-known challenging combinatorial benchmarks, including the minimum Kochen-Specker (KS) problem from quantum mechanics, the Murty-Simon Conjecture, and the Ramsey problems from extremal graph theory. We compare AlphaMapleSAT against March using different types of conquering solvers such as SAT Modulo Symmetries (SMS) and SAT+CAS, both built on top of the CaDiCaL SAT solver. We show that in all cases, there is a speedup in elapsed real time (wall clock time) ranging from 1.61x to 7.57x on a 128 core machine for the above-mentioned problems. We also perform cube-level and parallel scaling analysis over 32, 64, and 128 cores, which shows that AlphaMapleSAT outperforms March on all these settings. Our results show that deductively-guided MCTS search technique for cubing in CnC solvers can significantly outperform March on hard combinatorial problems.

cs.AI↗
arXiv2023

A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem

One of the fundamental results in quantum foundations is the Kochen-Specker (KS) theorem, which states that any theory whose predictions agree with quantum mechanics must be contextual, i.e., a quantum observation cannot be understood as revealing a pre-existing value. The theorem hinges on the existence of a mathematical object called a KS vector system. While many KS vector systems are known, the problem of finding the minimum KS vector system in three dimensions (3D) has remained stubbornly open for over 55 years. To address the minimum KS problem, we present a new verifiable proof-producing method based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS) that uses an isomorph-free orderly generation technique that is very effective in pruning away large parts of the search space. Our method shows that a KS system in 3D must contain at least 24 vectors. We show that our sequential and parallel Cube-and-Conquer (CnC) SAT+CAS methods are significantly faster than SAT-only, CAS-only, and a prior CAS-based method of Uijlen and Westerbaan. Further, while our parallel pipeline is somewhat slower than the parallel CnC version of the recently introduced Satisfiability Modulo Theories (SMS) method, this is in part due to the overhead of proof generation. Finally, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a size of 40.3 TiB in order 23.

quant-ph↗
arXiv2023

A New Lower Bound in the $abc$ Conjecture

We prove that there exist infinitely many coprime numbers $a$, $b$, $c$ with $a+b=c$ and $c>\operatorname{rad}(abc)\exp(6.563\sqrt{\log c}/\log\log c)$. These are the most extremal examples currently known in the $abc$ conjecture, thereby providing a new lower bound on the tightest possible form of the conjecture. This builds on work of van Frankenhuysen (1999) who proved the existence of examples satisfying the above bound with the constant $6.068$ in place of $6.563$. We show that the constant $6.563$ may be replaced by $4\sqrt{2\delta/e}$ where $\delta$ is a constant such that all full-rank unimodular lattices of sufficiently large dimension $n$ contain a nonzero vector with $\ell_1$ norm at most $n/\delta$.

math.NT↗
arXiv2021

Integer and Constraint Programming Revisited for Mutually Orthogonal Latin Squares

In this paper we provide results on using integer programming (IP) and constraint programming (CP) to search for sets of mutually orthogonal latin squares (MOLS). Both programming paradigms have previously successfully been used to search for MOLS, but solvers for IP and CP solvers have significantly improved in recent years and data on how modern IP and CP solvers perform on the MOLS problem is lacking. Using state-of-the-art solvers as black boxes we were able to quickly find pairs of MOLS (or prove their nonexistence) in all orders up to ten. Moreover, we improve the effectiveness of the solvers by formulating an extended symmetry breaking method as well as an improvement to the straightforward CP encoding. We also analyze the effectiveness of using CP and IP solvers to search for triples of MOLS, compare our timings to those which have been previously published, and estimate the running time of using this approach to resolve the longstanding open problem of determining the existence of a triple of MOLS of order ten.

cs.DM↗