| dc.description.abstract | Computational methods have become a valuable tool for studying mathematical problems and for constructing large combinatorial objects. In fact, it is often not possible to find large combinatorial objects using human reasoning alone and the only known way of accessing such objects is to use computational methods. These methods require deriving mathematical properties which the object in question must necessarily satisfy, translating those properties into a format that a computer can process, and then running a search through a space which contains the objects which satisfy those properties.
In this thesis, we solve some combinatorial and number theoretic problems which fit into the above framework and present computational strategies which can be used to perform the search and preprocessing. In particular, one strategy we examine uses state-of-the-art tools from the symbolic computation and SAT/SMT solving communities to execute a search more efficiently than would be the case using the techniques from either community in isolation. To this end, we developed the tool MathCheck2, which combines the sophisticated domain-specific knowledge of a computer algebra system (CAS) with the powerful general-purpose search routines of a SAT solver. This fits into the recently proposed SAT+CAS paradigm which is based on the insight that modern SAT solvers (some of the best general-purpose search tools ever developed) do not perform well in all applications but can be made more efficient if supplied with appropriate domain-specific knowledge. To our knowledge, this is the first PhD thesis which studies the SAT+CAS paradigm which we believe has potential to be used in many problems for a long time to come.
As case studies for the methods we examine, we study the problem of computing Williamson matrices, the problem of computing complex Golay sequences, and the problem of computing minimal primes. In each case, we provide results which are competitive with or improve on the best known results prior to our work. In the first case study, we provide for the first time an enumeration of all Williamson matrices up to order 45 and show that 35 is the smallest order for which Williamson matrices do not exist. These results were previously known under the restriction that the order was odd but our work also considers even orders, as Williamson did when he defined such matrices in 1944. In the second case study, we provide an independent verification of the 2002 conjecture that complex Golay sequences do not exist in order 23 and enumerate all complex Golay sequences up to order 25. In the third case study, we compute the set of minimal primes for all bases up to 16 as well for all bases up to 30 with possibly a small number of missing elements. | en |
