-
A Unified Mathematical Framework for Distributed Data Fabrics: Categorical Hypergraph Models
Authors:
T. Shaska,
I. Kotsireas
Abstract:
Current distributed data fabrics lack a rigorous mathematical foundation, often relying on ad-hoc architectures that struggle with consistency, lineage, and scale. We propose a mathematical framework for data fabrics, unifying heterogeneous data management in distributed systems through a hypergraph-based structure \( \mathcal{F} = (D, M, G, T, P, A) \). Datasets, metadata, transformations, polici…
▽ More
Current distributed data fabrics lack a rigorous mathematical foundation, often relying on ad-hoc architectures that struggle with consistency, lineage, and scale. We propose a mathematical framework for data fabrics, unifying heterogeneous data management in distributed systems through a hypergraph-based structure \( \mathcal{F} = (D, M, G, T, P, A) \). Datasets, metadata, transformations, policies, and analytics are modeled over a distributed system \( Σ= (N, C) \), with multi-way relationships encoded in a hypergraph \( G = (V, E) \). A categorical approach, with datasets as objects and transformations as morphisms, supports operations like data integration and federated learning. The hypergraph is embedded into a modular tensor category, capturing relational symmetries via braided monoidal structures, with geometric analogies to Hurwitz spaces enriching the algebraic modeling. We prove the NP-hardness of critical tasks, such as schema matching and dynamic partitioning, and propose spectral methods and symmetry-based alignments for scalable solutions. The framework ensures consistency, completeness, and causality under CAP and CAL theorems, leveraging sparse incidence matrices and braiding actions for fault-tolerant operations.
△ Less
Submitted 16 February, 2026;
originally announced February 2026.
-
A Neurosymbolic Framework for Geometric Reduction of Binary Forms
Authors:
Ilias Kotsireas,
Tony Shaska
Abstract:
This paper compares Julia reduction and hyperbolic reduction with the aim of finding equivalent binary forms with minimal coefficients. We demonstrate that hyperbolic reduction generally outperforms Julia reduction, particularly in the cases of sextics and decimics, though neither method guarantees achieving the minimal form. We further propose an additional shift and scaling to approximate the mi…
▽ More
This paper compares Julia reduction and hyperbolic reduction with the aim of finding equivalent binary forms with minimal coefficients. We demonstrate that hyperbolic reduction generally outperforms Julia reduction, particularly in the cases of sextics and decimics, though neither method guarantees achieving the minimal form. We further propose an additional shift and scaling to approximate the minimal form more closely. Finally, we introduce a machine learning framework to identify optimal transformations that minimize the heights of binary forms. This study provides new insights into the geometry and algebra of binary forms and highlights the potential of AI in advancing symbolic computation and reduction techniques. The findings, supported by extensive computational experiments, lay the groundwork for hybrid approaches that integrate traditional reduction methods with data-driven techniques.
△ Less
Submitted 3 July, 2025; v1 submitted 26 January, 2025;
originally announced January 2025.
-
New Results on Periodic Golay Pairs
Authors:
Tyler Lumsden,
Ilias Kotsireas,
Curtis Bright
Abstract:
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…
▽ More
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ć 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$.
△ Less
Submitted 16 March, 2025; v1 submitted 28 August, 2024;
originally announced August 2024.
-
Survey of Methods for Solving Systems of Nonlinear Equations, Part II: Optimization Based Approaches
Authors:
Ilias S. Kotsireas,
Panos M. Pardalos,
Alexander Semenov,
William T. Trevena,
Michael N. Vrahatis
Abstract:
This paper presents a comprehensive survey of methods which can be utilized to search for solutions to systems of nonlinear equations (SNEs). Our objectives with this survey are to synthesize pertinent literature in this field by presenting a thorough description and analysis of the known methods capable of finding one or many solutions to SNEs, and to assist interested readers seeking to identify…
▽ More
This paper presents a comprehensive survey of methods which can be utilized to search for solutions to systems of nonlinear equations (SNEs). Our objectives with this survey are to synthesize pertinent literature in this field by presenting a thorough description and analysis of the known methods capable of finding one or many solutions to SNEs, and to assist interested readers seeking to identify solution techniques which are well suited for solving the various classes of SNEs which one may encounter in real world applications.
To accomplish these objectives, we present a multi-part survey. In part one, we focused on root-finding approaches which can be used to search for solutions to a SNE without transforming it into an optimization problem. In part two, we introduce the various transformations which have been utilized to transform a SNE into an optimization problem, and we discuss optimization algorithms which can then be used to search for solutions. We emphasize the important characteristics of each method, and we discuss promising directions for future research. In part three, we will present a robust quantitative comparative analysis of methods capable of searching for solutions to SNEs.
△ Less
Submitted 17 August, 2022;
originally announced August 2022.
-
Survey of Methods for Solving Systems of Nonlinear Equations, Part I: Root-finding Approaches
Authors:
Ilias S. Kotsireas,
Panos M. Pardalos,
Alexander Semenov,
William T. Trevena,
Michael N. Vrahatis
Abstract:
This paper presents a comprehensive survey of methods which can be utilized to search for solutions to systems of nonlinear equations (SNEs). Our objectives with this survey are to synthesize pertinent literature in this field by presenting a thorough description and analysis of the known methods capable of finding one or many solutions to SNEs, and to assist interested readers seeking to identify…
▽ More
This paper presents a comprehensive survey of methods which can be utilized to search for solutions to systems of nonlinear equations (SNEs). Our objectives with this survey are to synthesize pertinent literature in this field by presenting a thorough description and analysis of the known methods capable of finding one or many solutions to SNEs, and to assist interested readers seeking to identify solution techniques which are well suited for solving the various classes of SNEs which one may encounter in real world applications.
To accomplish these objectives, we present a multi-part survey. In part one, we focus on root-finding approaches which can be used to search for solutions to a SNE without transforming it into an optimization problem. In part two, we will introduce the various transformations which have been utilized to transform a SNE into an optimization problem, and we discuss optimization algorithms which can then be used to search for solutions. In part three, we will present a robust quantitative comparative analysis of methods capable of searching for solutions to SNEs.
△ Less
Submitted 17 August, 2022;
originally announced August 2022.
-
A SAT-based Resolution of Lam's Problem
Authors:
Curtis Bright,
Kevin K. H. Cheung,
Brett Stevens,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
In 1989, computer searches by Lam, Thiel, and Swiercz experimentally resolved Lam's problem from projective geometry$\unicode{x2014}$the long-standing problem of determining if a projective plane of order ten exists. Both the original search and an independent verification in 2011 discovered no such projective plane. However, these searches were each performed using highly specialized custom-writt…
▽ More
In 1989, computer searches by Lam, Thiel, and Swiercz experimentally resolved Lam's problem from projective geometry$\unicode{x2014}$the long-standing problem of determining if a projective plane of order ten exists. Both the original search and an independent verification in 2011 discovered no such projective plane. However, these searches were each performed using highly specialized custom-written code and did not produce nonexistence certificates. In this paper, we resolve Lam's problem by translating the problem into Boolean logic and use satisfiability (SAT) solvers to produce nonexistence certificates that can be verified by a third party. Our work uncovered consistency issues in both previous searches$\unicode{x2014}$highlighting the difficulty of relying on special-purpose search code for nonexistence results.
△ Less
Submitted 8 December, 2020;
originally announced December 2020.
-
Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
Authors:
Curtis Bright,
Kevin K. H. Cheung,
Brett Stevens,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
In 1983, a computer search was performed for ovals in a projective plane of order ten. The search was exhaustive and negative, implying that such ovals do not exist. However, no nonexistence certificates were produced by this search, and to the best of our knowledge the search has never been independently verified. In this paper, we rerun the search for ovals in a projective plane of order ten and…
▽ More
In 1983, a computer search was performed for ovals in a projective plane of order ten. The search was exhaustive and negative, implying that such ovals do not exist. However, no nonexistence certificates were produced by this search, and to the best of our knowledge the search has never been independently verified. In this paper, we rerun the search for ovals in a projective plane of order ten and produce a collection of nonexistence certificates that, when taken together, imply that such ovals do not exist. Our search program uses the cube-and-conquer paradigm from the field of satisfiability (SAT) checking, coupled with a programmatic SAT solver and the nauty symbolic computation library for removing symmetries from the search.
△ Less
Submitted 30 May, 2020; v1 submitted 31 January, 2020;
originally announced January 2020.
-
Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem
Authors:
Curtis Bright,
Kevin K. H. Cheung,
Brett Stevens,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
In the 1970s and 1980s, searches performed by L. Carter, C. Lam, L. Thiel, and S. Swiercz showed that projective planes of order ten with weight 16 codewords do not exist. These searches required highly specialized and optimized computer programs and required about 2,000 hours of computing time on mainframe and supermini computers. In 2011, these searches were verified by D. Roy using an optimized…
▽ More
In the 1970s and 1980s, searches performed by L. Carter, C. Lam, L. Thiel, and S. Swiercz showed that projective planes of order ten with weight 16 codewords do not exist. These searches required highly specialized and optimized computer programs and required about 2,000 hours of computing time on mainframe and supermini computers. In 2011, these searches were verified by D. Roy using an optimized C program and 16,000 hours on a cluster of desktop machines. We performed a verification of these searches by reducing the problem to the Boolean satisfiability problem (SAT). Our verification uses the cube-and-conquer SAT solving paradigm, symmetry breaking techniques using the computer algebra system Maple, and a result of Carter that there are ten nonisomorphic cases to check. Our searches completed in about 30 hours on a desktop machine and produced nonexistence proofs of about 1 terabyte in the DRAT (deletion resolution asymmetric tautology) format.
△ Less
Submitted 1 May, 2020; v1 submitted 31 January, 2020;
originally announced January 2020.
-
A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords
Authors:
Curtis Bright,
Kevin Cheung,
Brett Stevens,
Dominique Roy,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
Using techniques from the fields of symbolic computation and satisfiability checking we verify one of the cases used in the landmark result that projective planes of order ten do not exist. In particular, we show that there exist no projective planes of order ten that generate codewords of weight fifteen, a result first shown in 1973 via an exhaustive computer search. We provide a simple satisfiab…
▽ More
Using techniques from the fields of symbolic computation and satisfiability checking we verify one of the cases used in the landmark result that projective planes of order ten do not exist. In particular, we show that there exist no projective planes of order ten that generate codewords of weight fifteen, a result first shown in 1973 via an exhaustive computer search. We provide a simple satisfiability (SAT) instance and a certificate of unsatisfiability that can be used to automatically verify this result for the first time. All previous demonstrations of this result have relied on search programs that are difficult or impossible to verify---in fact, our search found partial projective planes that were missed by previous searches due to previously undiscovered bugs. Furthermore, we show how the performance of the SAT solver can be dramatically increased by employing functionality from a computer algebra system (CAS). Our SAT+CAS search runs significantly faster than all other published searches verifying this result.
△ Less
Submitted 25 March, 2020; v1 submitted 10 November, 2019;
originally announced November 2019.
-
Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
Authors:
Curtis Bright,
Ilias Kotsireas,
Albert Heinle,
Vijay Ganesh
Abstract:
We use techniques from the fields of computer algebra and satisfiability checking to develop a new algorithm to search for complex Golay pairs. We implement this algorithm and use it to perform a complete search for complex Golay pairs of lengths up to 28. In doing so, we find that complex Golay pairs exist in the lengths 24 and 26 but do not exist in the lengths 23, 25, 27, and 28. This independe…
▽ More
We use techniques from the fields of computer algebra and satisfiability checking to develop a new algorithm to search for complex Golay pairs. We implement this algorithm and use it to perform a complete search for complex Golay pairs of lengths up to 28. In doing so, we find that complex Golay pairs exist in the lengths 24 and 26 but do not exist in the lengths 23, 25, 27, and 28. This independently verifies work done by F. Fiedler in 2013 and confirms the 2002 conjecture of Craigen, Holzmann, and Kharaghani that complex Golay pairs of length 23 don't exist. Our algorithm is based on the recently proposed SAT+CAS paradigm of combining SAT solvers with computer algebra systems to efficiently search large spaces specified by both algebraic and logical constraints. The algorithm has two stages: first, a fine-tuned computer program uses functionality from computer algebra systems and numerical libraries to construct a list containing every sequence which could appear as the first sequence in a complex Golay pair up to equivalence. Second, a programmatic SAT solver constructs every sequence (if any) that pair off with the sequences constructed in the first stage to form a complex Golay pair. This extends work originally presented at the International Symposium on Symbolic and Algebraic Computation (ISSAC) in 2018; we discuss and implement several improvements to our algorithm that enabled us to improve the efficiency of the search and increase the maximum length we search from length 25 to 28.
△ Less
Submitted 27 July, 2019;
originally announced July 2019.
-
The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
Authors:
Curtis Bright,
Dragomir Ž. Đoković,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
In this paper, we provide an overview of the SAT+CAS method that combines satisfiability checkers (SAT solvers) and computer algebra systems (CAS) to resolve combinatorial conjectures, and present new results vis-à-vis best matrices. The SAT+CAS method is a variant of the Davis$\unicode{8211}$Putnam$\unicode{8211}$Logemann$\unicode{8211}$Loveland $\operatorname{DPLL}(T)$ architecture, where the…
▽ More
In this paper, we provide an overview of the SAT+CAS method that combines satisfiability checkers (SAT solvers) and computer algebra systems (CAS) to resolve combinatorial conjectures, and present new results vis-à-vis best matrices. The SAT+CAS method is a variant of the Davis$\unicode{8211}$Putnam$\unicode{8211}$Logemann$\unicode{8211}$Loveland $\operatorname{DPLL}(T)$ architecture, where the $T$ solver is replaced by a CAS. We describe how the SAT+CAS method has been previously used to resolve many open problems from graph theory, combinatorial design theory, and number theory, showing that the method has broad applications across a variety of fields. Additionally, we apply the method to construct the largest best matrices yet known and present new skew Hadamard matrices constructed from best matrices. We show the best matrix conjecture (that best matrices exist in all orders of the form $r^2+r+1$) which was previously known to hold for $r\leq6$ also holds for $r=7$. We also confirmed the results of the exhaustive searches that have been previously completed for $r\leq6$.
△ Less
Submitted 17 November, 2019; v1 submitted 10 July, 2019;
originally announced July 2019.
-
SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
Authors:
Curtis Bright,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
Over the last few decades, many distinct lines of research aimed at automating mathematics have been developed, including computer algebra systems (CASs) for mathematical modelling, automated theorem provers for first-order logic, SAT/SMT solvers aimed at program verification, and higher-order proof assistants for checking mathematical proofs. More recently, some of these lines of research have st…
▽ More
Over the last few decades, many distinct lines of research aimed at automating mathematics have been developed, including computer algebra systems (CASs) for mathematical modelling, automated theorem provers for first-order logic, SAT/SMT solvers aimed at program verification, and higher-order proof assistants for checking mathematical proofs. More recently, some of these lines of research have started to converge in complementary ways. One success story is the combination of SAT solvers and CASs (SAT+CAS) aimed at resolving mathematical conjectures.
Many conjectures in pure and applied mathematics are not amenable to traditional proof methods. Instead, they are best addressed via computational methods that involve very large combinatorial search spaces. SAT solvers are powerful methods to search through such large combinatorial spaces---consequently, many problems from a variety of mathematical domains have been reduced to SAT in an attempt to resolve them. However, solvers traditionally lack deep repositories of mathematical domain knowledge that can be crucial to pruning such large search spaces. By contrast, CASs are deep repositories of mathematical knowledge but lack efficient general search capabilities. By combining the search power of SAT with the deep mathematical knowledge in CASs we can solve many problems in mathematics that no other known methods seem capable of solving.
We demonstrate the success of the SAT+CAS paradigm by highlighting many conjectures that have been disproven, verified, or partially verified using our tool MathCheck. These successes indicate that the paradigm is positioned to become a standard method for solving problems requiring both a significant amount of search and deep mathematical reasoning. For example, the SAT+CAS paradigm has recently been used by Heule, Kauers, and Seidl to find many new algorithms for $3\times3$ matrix multiplication.
△ Less
Submitted 16 September, 2019; v1 submitted 9 July, 2019;
originally announced July 2019.
-
Effective problem solving using SAT solvers
Authors:
Curtis Bright,
Jürgen Gerhard,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
In this article we demonstrate how to solve a variety of problems and puzzles using the built-in SAT solver of the computer algebra system Maple. Once the problems have been encoded into Boolean logic, solutions can be found (or shown to not exist) automatically, without the need to implement any search algorithm. In particular, we describe how to solve the $n$-queens problem, how to generate and…
▽ More
In this article we demonstrate how to solve a variety of problems and puzzles using the built-in SAT solver of the computer algebra system Maple. Once the problems have been encoded into Boolean logic, solutions can be found (or shown to not exist) automatically, without the need to implement any search algorithm. In particular, we describe how to solve the $n$-queens problem, how to generate and solve Sudoku puzzles, how to solve logic puzzles like the Einstein riddle, how to solve the 15-puzzle, how to solve the maximum clique problem, and finding Graeco-Latin squares.
△ Less
Submitted 16 September, 2019; v1 submitted 14 June, 2019;
originally announced June 2019.
-
New Infinite Families of Perfect Quaternion Sequences and Williamson Sequences
Authors:
Curtis Bright,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
We present new constructions for perfect and odd perfect sequences over the quaternion group $Q_8$. In particular, we show for the first time that perfect and odd perfect quaternion sequences exist in all lengths $2^t$ for $t\geq0$. In doing so we disprove the quaternionic form of Mow's conjecture that the longest perfect $Q_8$-sequence that can be constructed from an orthogonal array construction…
▽ More
We present new constructions for perfect and odd perfect sequences over the quaternion group $Q_8$. In particular, we show for the first time that perfect and odd perfect quaternion sequences exist in all lengths $2^t$ for $t\geq0$. In doing so we disprove the quaternionic form of Mow's conjecture that the longest perfect $Q_8$-sequence that can be constructed from an orthogonal array construction is of length 64. Furthermore, we use a connection to combinatorial design theory to prove the existence of a new infinite class of Williamson sequences, showing that Williamson sequences of length $2^t n$ exist for all $t\geq0$ when Williamson sequences of odd length $n$ exist. Our constructions explain the abundance of Williamson sequences in lengths that are multiples of a large power of two.
△ Less
Submitted 25 November, 2020; v1 submitted 1 May, 2019;
originally announced May 2019.
-
A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples
Authors:
Curtis Bright,
Dragomir Z. Djokovic,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
We enumerate all circulant good matrices with odd orders divisible by 3 up to order 70. As a consequence of this we find a previously overlooked set of good matrices of order 27 and a new set of good matrices of order 57. We also find that circulant good matrices do not exist in the orders 51, 63, and 69, thereby finding three new counterexamples to the conjecture that such matrices exist in all o…
▽ More
We enumerate all circulant good matrices with odd orders divisible by 3 up to order 70. As a consequence of this we find a previously overlooked set of good matrices of order 27 and a new set of good matrices of order 57. We also find that circulant good matrices do not exist in the orders 51, 63, and 69, thereby finding three new counterexamples to the conjecture that such matrices exist in all odd orders. Additionally, we prove a new relationship between the entries of good matrices and exploit this relationship in our enumeration algorithm. Our method applies the SAT+CAS paradigm of combining computer algebra functionality with modern SAT solvers to efficiently search large spaces which are specified by both algebraic and logical constraints.
△ Less
Submitted 12 November, 2018;
originally announced November 2018.
-
Enumeration of Complex Golay Pairs via Programmatic SAT
Authors:
Curtis Bright,
Ilias Kotsireas,
Albert Heinle,
Vijay Ganesh
Abstract:
We provide a complete enumeration of all complex Golay pairs of length up to 25, verifying that complex Golay pairs do not exist in lengths 23 and 25 but do exist in length 24. This independently verifies work done by F. Fiedler in 2013 that confirms the 2002 conjecture of Craigen, Holzmann, and Kharaghani that complex Golay pairs of length 23 don't exist. Our enumeration method relies on the rece…
▽ More
We provide a complete enumeration of all complex Golay pairs of length up to 25, verifying that complex Golay pairs do not exist in lengths 23 and 25 but do exist in length 24. This independently verifies work done by F. Fiedler in 2013 that confirms the 2002 conjecture of Craigen, Holzmann, and Kharaghani that complex Golay pairs of length 23 don't exist. Our enumeration method relies on the recently proposed SAT+CAS paradigm of combining computer algebra systems with SAT solvers to take advantage of the advances made in the fields of symbolic computation and satisfiability checking. The enumeration proceeds in two stages: First, we use a fine-tuned computer program and functionality from computer algebra systems to construct a list containing all sequences which could appear as the first sequence in a complex Golay pair (up to equivalence). Second, we use a programmatic SAT solver to construct all sequences (if any) that pair off with the sequences constructed in the first stage to form a complex Golay pair.
△ Less
Submitted 7 November, 2018; v1 submitted 14 May, 2018;
originally announced May 2018.
-
Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
Authors:
Curtis Bright,
Ilias Kotsireas,
Vijay Ganesh
Abstract:
We employ tools from the fields of symbolic computation and satisfiability checking---namely, computer algebra systems and SAT solvers---to study the Williamson conjecture from combinatorial design theory and increase the bounds to which Williamson matrices have been enumerated. In particular, we completely enumerate all Williamson matrices of even order up to and including 70 which gives us deepe…
▽ More
We employ tools from the fields of symbolic computation and satisfiability checking---namely, computer algebra systems and SAT solvers---to study the Williamson conjecture from combinatorial design theory and increase the bounds to which Williamson matrices have been enumerated. In particular, we completely enumerate all Williamson matrices of even order up to and including 70 which gives us deeper insight into the behaviour and distribution of Williamson matrices. We find that, in contrast to the case when the order is odd, Williamson matrices of even order are quite plentiful and exist in every even order up to and including 70. As a consequence of this and a new construction for 8-Williamson matrices we construct 8-Williamson matrices in all odd orders up to and including 35. We additionally enumerate all Williamson matrices whose orders are divisible by 3 and less than 70, finding one previously unknown set of Williamson matrices of order 63.
△ Less
Submitted 13 May, 2019; v1 submitted 3 April, 2018;
originally announced April 2018.