Abstract
In this paper we present MathCheck2, a tool which combines sophisticated search procedures of current SAT solvers with domain specific knowledge provided by algorithms implemented in computer algebra systems (CAS). MathCheck2 is aimed to finitely verify or to find counterexamples to mathematical conjectures, building on our previous work on the MathCheck system. Using MathCheck2 we validated the Hadamard conjecture from design theory for matrices up to rank 136 and a few additional ranks up to 156. Also, we provide an independent verification of the claim that Williamson matrices of order 35 do not exist, and demonstrate for the first time that 35 is the smallest number with this property. Finally, we provided more than 160 matrices to the Magma Hadamard database that are not equivalent to any matrices previously included in that database.
Cite
CITATION STYLE
Bright, C., Ganesh, V., Heinle, A., Kotsireas, I., Nejati, S., & Czarnecki, K. (2016). Mathcheck2: A SAT+CAS verifier for combinatorial conjectures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9890 LNCS, pp. 117–133). Springer Verlag. https://doi.org/10.1007/978-3-319-45641-6_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
