Headshot of Curtis
Curtis Bright
cbright

I solve math­e­mat­i­cal prob­lems through sat­is­fi­a­bil­ity solv­ing and com­puter al­ge­bra. Cur­rently, I am an as­sis­tant pro­fes­sor in the School of Com­puter Sci­ence at the Uni­ver­sity of Wind­sor and an ad­junct re­search pro­fes­sor in the School of Math­e­mat­ics and Sta­tis­tics at Car­leton Uni­ver­sity. I com­pleted my PhD in the Cheri­ton School of Com­puter Sci­ence at the Uni­ver­sity of Wa­ter­loo and I re­main the lead de­vel­oper of the Math­Check pro­ject. See my cur­ricu­lum vitae or bio for a sum­mary of my aca­d­e­mic ca­reer and my re­search state­ment, pub­li­ca­tion list, or show­case for an overview of my re­search.

News: The Al­go­rithms & Math­e­mat­ics group at Wind­sor is ac­cept­ing ap­pli­ca­tions for open re­search po­si­tions.

I co-chaired (with James Dav­en­port) the 2021 SC-square work­shop held on Au­gust 19–20, 2021.

Published Works

My work has been pub­lished in a num­ber of no­table venues in­clud­ing in the Jour­nal of Au­to­mated Rea­son­ing, at the AAAI Con­fer­ence on Ar­ti­fi­cial In­tel­li­gence 2018 (and 2019, 2021), at ISSAC 2018 (and 2011), at CASC 2016, at CAS­CON 2019, in the Jour­nal of Ex­per­i­men­tal Math­e­mat­ics, in the Jour­nal of Sym­bolic Com­pu­ta­tion (twice), in the An­nals of Math­e­mat­ics and Ar­ti­fi­cial In­tel­li­gence, in IEEE Trans­ac­tions of In­for­ma­tion The­ory, in Ap­plic­a­ble Al­ge­bra in En­gi­neer­ing, Com­mu­ni­ca­tion and Com­put­ing (re­ceiv­ing the 2020 best paper award), at ICTAI 2021, at IWOCA 2020, at IJCAI 2020, and ap­pears in Maple in Math­e­mat­ics Ed­u­ca­tion and Re­search. Most of the ar­ti­cles are be­hind pay­walls but preprints for each of my pa­pers are avail­able below if you do not have ac­cess through the pub­lisher's site.

Brag­ging rights: My Erdős num­ber is 2, through the pa­pers Min­i­mal el­e­ments for the prime num­bers (Bright, Dev­illers, Shal­lit) and New bounds on the length of fi­nite Pierce and Engel se­ries (Erdős, Shal­lit). I have been awarded 0x$1.20 at Knuth's Bank of San Ser­riffe for find­ing a typo in The Art of Com­puter Pro­gram­ming pre­sent since the first edi­tion (!) of vol­ume 2 in 1969. In the 2015 ver­sion of his clas­sic text Ga­lois The­ory, Ian Stew­art cited a re­port of mine. Ad­di­tion­ally, Noam Elkies once gave a talk ref­er­enc­ing a re­sult that I showed as an un­der­grad­u­ate stu­dent—the tech­ni­cal re­port is dear to my heart as one of the first pa­pers I ever wrote.

Writings

Copies of my aca­d­e­mic writ­ings in re­verse chrono­log­i­cal order. The most re­cent are typ­i­cally co-writ­ten with stu­dents that I am su­per­vis­ing and may be preprints in the process of being fi­nal­ized. The old­est are re­ports writ­ten dur­ing my un­der­grad­u­ate stud­ies that I have archived as a part of my life­long com­mit­ment to im­prove my writ­ing.

Showcase

Apps and posters that I've writ­ten to show­case my re­search and some of its ap­pli­ca­tions. I enjoy bring­ing life to my re­search by using ac­ces­si­ble vi­su­al­iza­tions and in­ter­ac­tiv­ity.

KR 2022 talk preview Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation August 3, 2022
Tutte colloquium preview SAT Solving with Computer Algebra for Combinatorics April 1, 2022
AAAI22 poster preview IP and CP Revisited for Mutually Orthogonal Latin Squares (Student Abstract) with N. Rubin, B. Stevens, K. Cheung. February 27, 2022
Dagstuhl tutorial preview Isomorph-Free Exhaustive Generation in SAT Solving (Invited Tutorial) February 17, 2022
Harvard presentation preview When Computer Algebra Meets Satisfiability: A New Approach to Combinatorial Mathematics with V. Ganesh. November 3, 2021
CanaDAM 2021 preview SAT Solvers and Combinatorics Problems May 25, 2021
Simons TV Logo Computer Algebra and SAT for Mathematical Search April 21, 2021
AAAI2021 poster preview A SAT-Based Resolution of Lam's Problem February 4, 2021
AAAI2021 opening slide A SAT-Based Resolution of Lam's Problem [full video] February 3, 2021
IJCAI2020 poster preview Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem January 14, 2021
IJCAI2020 presentation preview Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem [5 min highlights] January 6, 2021
CMS2020 presentation preview A Resolution of Lam's Problem via Satisfiability Solvers December 4, 2020
Hadamard 160 preview Hadamard 160 in Cool Tones with B. Lee. November 15, 2020
IWOCA2020 presentation preview Nonexistence Certificates for Ovals in a Projective Plane of Order Ten June 8, 2020
MC2019 presentation preview Effective Problem Solving Using SAT Solvers October 17, 2019
Colouring of the 8x8 queens graph Graph Colouring with SAT September 9, 2019
A SAT+CAS approach to finding good matrices poster A SAT+CAS Approach to Finding Good Matrices January 28, 2019
15-puzzle instance Solving the 15-puzzle December 19, 2018
Completed Sudoku puzzle Interactive Sudoku December 3, 2018
Highlighted clique of size 4 in a graph with 20 vertices Clique Finding with SAT November 15, 2018
Graeco-Latin square of order 10 Finding Graeco-Latin Squares November 7, 2018
Solution of the 8-Queens problem The n-Queens Problem October 4, 2018
Sudoku puzzle Solving the World's Hardest Sudoku October 4, 2018
Einstein with the text 'Who owns the fish?' Solving the Einstein Riddle October 4, 2018
The SAT+CAS paradigm and the Williamson conjecture poster The SAT+CAS Paradigm and the Williamson Conjecture July 17, 2018
A SAT+CAS method for enumerating Williamson matrices of even order poster A SAT+CAS Method for Enumerating Williamson Matrices of Even Order February 4, 2018
Example truth table Online Truth Table Generator May 8, 2013
Ataxx gameplay example Ataxx AI November 15, 2012
The quartic formula (cropped) The Quartic Formula [webpage] April 21, 2012
Vector rational number reconstruction poster Vector Rational Number Reconstruction April 9, 2011

Talks

An archive of my aca­d­e­mic talks that have used slides.

Group

The fol­low­ing stu­dents are work­ing or have worked in my group:

Bio

I joined the fac­ulty of the School of Com­puter Sci­ence at the Uni­ver­sity of Wind­sor in 2020 and taught In­tro­duc­tion to Al­go­rithms and Pro­gram­ming II in the win­ter of 2021. In Au­gust 2021, I co-chaired (with James Dav­en­port) the 2021 SC-square work­shop. In the fall of 2021, I taught a grad­u­ate course on com­pu­ta­tional dis­crete math­e­mat­ics. In the win­ter of 2022, I will teach Key Con­cepts in Com­puter Sci­ence and In­tro­duc­tion to Al­go­rithms and Pro­gram­ming II.

I am cur­rently the lead de­vel­oper of the Math­Check pro­ject run by pro­fes­sor Vijay Ganesh at the Uni­ver­sity of Wa­ter­loo. In 2020, I held an NSERC post­doc­toral fel­low­ship at Car­leton Uni­ver­sity work­ing with pro­fes­sors Kevin Che­ung and Brett Stevens. Our major re­sult was gen­er­at­ing and ver­i­fy­ing the first set of nonex­is­tence cer­tifi­cates for solv­ing Lam's prob­lem.

Be­tween 2017 and 2019, I was a post­doc­toral fel­low of the Com­puter Aided Re­search Group at the Uni­ver­sity of Wa­ter­loo. I was also af­fil­i­ated with the CARGO Lab at Wil­frid Lau­rier Uni­ver­sity and worked with pro­fes­sor Ilias Kot­sireas on com­bi­na­to­r­ial ma­trix the­ory. Dur­ing this time, I de­vised the first proof that Williamson ma­tri­ces exist in all or­ders that are pow­ers of two.

I in­terned at Maple­soft in 2017 and again in 2018. While at Maple­soft I ap­plied my re­search to dra­mat­i­cally im­prove some dis­crete op­ti­miza­tion rou­tines of Maple—for ex­am­ple, in the lat­est ver­sion of Maple the chro­matic num­ber of the Queen Graph of the chess­board can be com­puted in a few sec­onds in­stead of a few hours. I have writ­ten a num­ber of Maple ap­pli­ca­tions demon­strat­ing how to ef­fec­tively use Maple's SAT solver in a va­ri­ety of prob­lems and pre­sented many of these ap­pli­ca­tions at the 2019 Maple con­fer­ence.

In March 2017, I de­fended my PhD the­sis, su­per­vised by Vijay Ganesh and Krzysztof Czar­necki. My the­sis demon­strated the ef­fec­tive­ness of com­bin­ing sat­is­fi­a­bil­ity check­ing and sym­bolic com­pu­ta­tion for solv­ing math­e­mat­i­cal prob­lems.

In Fall 2015, I taught El­e­men­tary Al­go­rithm De­sign and Data Ab­strac­tion along­side Gor­don Cor­mack to 258 stu­dents. This course is the fol­low-up to De­sign­ing Func­tional Pro­grams in­tended for CS and math ma­jors and uses the pro­gram­ming lan­guage C.

In Sum­mer 2015, I was the sole in­struc­tor of 145 stu­dents in In­tro­duc­tion to Com­puter Sci­ence 1, an in­tro­duc­tion to com­puter sci­ence in­tended for non-CS ma­jors. As the in­struc­tor I was re­spon­si­ble for com­pil­ing 9 as­sign­ments through­out the term and each one con­sisted of ques­tions newly de­vel­oped by my­self.

In Fall 2014, I taught De­sign­ing Func­tional Pro­grams, an in­tro­duc­tion to com­puter sci­ence for CS and math ma­jors based around the pro­gram­ming lan­guage Racket. I co­or­di­nated with 5 other in­struc­tors to teach 876 stu­dents.

In Sum­mer 2014, as a part of Google's sum­mer of code I su­per­vised (along with William Hart) the un­der­grad­u­ate stu­dent Ab­hi­nav Baid and over­saw the im­ple­men­ta­tion of a fast vari­ant of the LLL al­go­rithm for lat­tice basis re­duc­tion in the open source num­ber the­ory li­brary FLINT. This code is avail­able in the lat­est ver­sion of FLINT in the fm­pz_lll mod­ule.

In Spring 2013, I re­ceived an award for ex­cep­tional per­for­mance as an in­struc­tional as­sis­tant in the course Logic and Com­pu­ta­tion. Dur­ing this term I wrote an on­line truth table gen­er­a­tor for eas­ily gen­er­at­ing truth ta­bles to in­clude in as­sign­ment so­lu­tions and course notes.

In Win­ter 2013, I de­signed the SCG logo (a spoof on a pro­posed UW logo). At the time I was a grad­u­ate stu­dent and I've made pub­licly avail­able a col­lec­tion of the lec­ture notes that I took as a stu­dent.

In 2007, I started a per­sonal web­site for nonaca­d­e­mic pro­jects, though most of my ef­fort these days goes into ad­vanc­ing my re­search pro­gram.