2 citations · 3 across the 2 of their papers we have counts for
5 papers · 1 filter
The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
Curtis Bright, Dragomir Ž. Đoković, Ilias Kotsireas +1
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 conjectu…
SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
Curtis Bright, Ilias Kotsireas, Vijay Ganesh
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…
A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples
Curtis Bright, Dragomir Z. Djokovic, Ilias Kotsireas +1
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 an…
Enumeration of Complex Golay Pairs via Programmatic SAT
Curtis Bright, Ilias Kotsireas, Albert Heinle +1
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. Thi…
Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
Curtis Bright, Ilias Kotsireas, Vijay Ganesh
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 com…