Publications

20. A SAT Solver + Computer Algebra Attack on the Minimum Kochen–Specker Problem
Zhengyu LiCurtis BrightVijay Ganesh
In submission
[pdf] [bib]

19. A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)
Conor DugganZhengyu LiCurtis BrightVijay Ganesh
The 38th AAAI Conference on Artificial Intelligence (AAAI 2024)
[pdf] [bib] [poster]

18. A SAT Solver and Computer Algebra Attack on the Minimum Kochen–Specker Problem (Student Abstract)
Zhengyu LiCurtis BrightVijay Ganesh
The 38th AAAI Conference on Artificial Intelligence (AAAI 2024)
[pdf] [bib] [poster]

17. An SC-Square Approach to the Minimum Kochen–Specker Problem
Zhengyu LiCurtis BrightVijay Ganesh
The 7th Workshop on Satisfiability Checking and Symbolic Computation (SC² 2022)
[pdf] [bib]

16. When Satisfiability Solving Meets Symbolic Computation
Curtis Bright, Ilias Kotsireas, Vijay Ganesh
Communications of the ACM (CACM 2022)
[pdf] [bib]

15. A SAT-based Resolution of Lam's Problem
Curtis Bright, Kevin Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh
The 35th AAAI Conference on Artificial Intelligence (AAAI 2021)
[pdf] [bib] [poster]

14. Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem
Curtis Bright, Kevin Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh
The 29th International Joint Conference on Artificial Intelligence (IJCAI 2020)
[pdf] [bib] [poster]

13. Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
Curtis Bright, Kevin Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh
The 31st International Workshop on Combinatorial Algorithms (IWOCA 2020)
[pdf] [bib]

12. A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords
Curtis Bright, Kevin Cheung, Brett Stevens, Dominique Roy, Ilias Kotsireas, Vijay Ganesh
Applicable Algebra in Engineering, Communication and Computing (AAECC 2020)
2020 AAECC Best Paper Award
[pdf] [bib]

11. The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
Curtis Bright, Dragomir Ž. Ðoković, Ilias Kotsireas, Vijay Ganesh
Annals of Mathematics and Artificial Intelligence (AMAI 2019)
[pdf] [bib]

10. SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
Curtis BrightIlias Kotsireas, Vijay Ganesh
The 29th International Conference on Computer Science and Software Engineering (CASCON 2019)
[pdf] [bib]

9. ​Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
Curtis Bright, Ilias Kotsireas, Albert HeinleVijay Ganesh
Journal of Symbolic Computation (JSC 2021)
[pdf] [bib]

8. ​Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
Curtis Bright, Ilias Kotsireas, Vijay Ganesh
Journal of Symbolic Computation (JSC 2020)
[pdf] [bib]

7. A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples
Curtis Bright, Dragomir Ž. Ðoković, Ilias Kotsireas, Vijay Ganesh
The Thirty-Third AAAI Conference on Artificial Intelligence (AAAI 2019)
[pdf] [bib] [poster]

6. Enumeration of Complex Golay Pairs via Programmatic SAT
Curtis Bright, Ilias Kotsireas, Albert Heinle, Vijay Ganesh
The 43rd International Symposium on Symbolic and Algebraic Computation (ISSAC 2018)
[pdf] [bib]

5. A SAT+CAS Method for Enumerating Williamson Matrices of Even Order
Curtis Bright, Ilias Kotsireas, Vijay Ganesh
The Thirty-Second AAAI Conference on Artificial Intelligence (AAAI 2018)
[pdf] [bib] [poster]

4. The SAT+CAS Paradigm and the Williamson Conjecture (Extended Abstract)
Curtis Bright, Ilias Kotsireas, Vijay Ganesh
ACM Communications in Computer Algebra (CCA 2018)
[pdf] [bib] [poster]

3. Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures
Ed Zulkoski, Curtis Bright, Albert Heinle, Ilias Kotsireas, Krzysztof Czarnecki, Vijay Ganesh
Journal of Automated Reasoning (JAR 2017)
In Special Issue for Best Papers at CADE 2015
[pdf] [bib]

2. MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias Kotsireas, Saeed Nejati, Krzysztof Czarnecki
The 18th International Workshop on Computer Algebra in Scientific Computing (CASC 2016)
Symbolic Computation + Satisfiability Checking (SC²) Track Invited Paper
[pdf] [bib]
The 1st Workshop on Satisfiability Checking and Symbolic Computation (SC² 2016)
[pdf] [bib]

1. MathCheck: A Math Assistant based on a Combination of Computer Algebra Systems and SAT Solvers
Ed Zulkoski, Vijay Ganesh, Krzysztof Czarnecki
The 25th International Conference on Automated Deduction (CADE 2015)​
MathCheck selected for JAR Special Issue on Best Papers at CADE 2015
[pdf] [bib]
The 25th International Joint Conference on Artificial Intelligence (IJCAI 2016)​
IJCAI 'Sister Conference Best Paper Track' Invited Paper
[pdf] [bib]