Satisfiability Problem (SAT) Professors and Supervisors in Canada

Xujie Siمشاهده پروفایل

استادیار

University of TorontoCanada

Xujie Si is an Assistant Professor in the Department of Computer Science at the University of Toronto. He is also a faculty affiliate at the Vector Institute and an affiliate member at Mila - Quebec AI Institute, holding a Canada CIFAR AI Chair. Previously, he served as an Assistant Professor at McGill University's School of Computer Science. Education: Ph.D., Computer and Information Science, University of Pennsylvania (advised by Mayur Naik) M.S., Computer Science, Vanderbilt University B.E. (with Honors), Nankai University Research Focus: His work bridges AI and program reasoning, emphasizing the integration of statistical and logical methods. Key areas include: Static analysis and verification using deep learning/reinforcement learning Neuro-symbolic systems for urban simulation (e.g., LogiCity) Automated theorem proving via LLMs and symbolic reasoning Program repair and compiler fuzzing Recent Article Trends: Recent work focuses on synergizing LLMs with symbolic reasoning (e.g., Olympiad inequality proving), advancing SAT solving with graph neural networks, and applying neuro-symbolic methods to Euclidean geometry formalization. Awards: Canada CIFAR AI Chair (2023) Lab/Teams: Leads research teams exploring program analysis, neuro-symbolic AI, and formal verification at the University of Toronto and Vector Institute.

پروفایل رسمی دانشگاه

Valentine Kabanetsمشاهده پروفایل

استاد

Simon Fraser UniversityCanada

Valentine Kabanets is a Professor in the School of Computing Science at Simon Fraser University. He holds a Ph.D. in Computer Science from the University of Toronto (2000), M.Sc. from Simon Fraser University (1996), and B.Sc. from the National University of Kiev (1993). His research focuses on computational complexity theory, pseudorandomness, circuit lower bounds, and cryptography. He has received prestigious awards including the Nerode Prize (2013) and multiple best-paper awards at conferences like STOC and CCC. Teaching includes courses on computability and complexity (CMPT 308), data structures and algorithms (CMPT 307), and advanced complexity theory. His research explores foundational questions such as derandomization of algorithms, connections between upper/lower bounds in complexity, and cryptographic hardness assumptions. He leads the Algorithms and Complexity Theory Lab and has supervised numerous graduate students and postdocs. Kabanets' work bridges theoretical insights with practical algorithmic advancements, contributing to both foundational computer science and applied cryptography.

پروفایل رسمی دانشگاه

David A. D. Tompkinsمشاهده پروفایل

دانشیار

University of WaterlooCanada

Dave Tompkins is an Associate Professor in the David R. Cheriton School of Computer Science at the University of Waterloo. He holds a PhD in Computer Science and a MASc in Electrical Engineering from the University of British Columbia, along with a BESc and BSc from Western University. His primary research focuses on Stochastic Local Search (SLS) algorithms for the Satisfiability Problem (SAT) and MAX-SAT. Research Interests: His work spans Stochastic Local Search Algorithms SAT and MAX-SAT problem solving Dynamic Local Search techniques Heuristic algorithm design and optimization Data compression and image coding Genetic algorithms and game theory Scientific Awards: He has received Best Paper Award (2006, CCAI) Best Poster Awards (2003, ASI; 1999, ASI) Gold and Silver Medals in SAT Competitions (2004) Incomplete Solver Track Awards (2012, MAX-SAT) Projects: He is known for developing the UBCSAT framework and the Captain Jack SAT solver. He has also contributed to standards like JBIG2 and JPEG-2000.

پروفایل رسمی دانشگاه

Vijay Ganeshمشاهده پروفایل

استاد

University of WaterlooCanada

Dr. Vijay Ganesh is a Professor of Computer Science at Georgia Institute of Technology, where he also serves as Associate Director of the IDEaS Institute and is affiliated with Tech AI. Previously, he held roles as Associate Professor (2018–2023) and Assistant Professor (2012–2018) at the University of Waterloo, and Research Scientist at MIT (2007–2012). He earned his PhD from Stanford University in 2007. His research focuses on SAT/SMT solvers and their applications in AI, software engineering, security, mathematics, and physics. Notable contributions include developing solvers like MapleSAT, Z3str4, and AlphaZ3, and exploring machine learning-augmented reasoning. He has led projects in logic for AI, proof complexity, and security of blockchain technologies. His awards include ACM Impact Paper (2019), ACM Test of Time (2016), and DATE’s Ten-Year Most Influential Paper (2008). He has advised startups like Quantstamp, a blockchain security firm, and co-directed the Waterloo AI Institute (2021–2023). His teaching includes courses on discrete mathematics, software engineering, and AI. Education: PhD in Computer Science, Stanford University (2007); Master’s in Electrical Engineering, Stanford (2000) Research Interests: SAT/SMT solvers, formal methods, automated testing, AI security, combinatorial mathematics Affiliations: Georgia Tech’s School of Computer Science, IDEaS Institute

پروفایل رسمی دانشگاه

David G. Mitchellمشاهده پروفایل

دانشیار

Simon Fraser UniversityCanada

David G. Mitchell is an Associate Professor in the Department of Computing Science at Simon Fraser University (SFU). He is part of the School of Computing Science and affiliated with the Computational Logic Laboratory. His research focuses on propositional satisfiability (SAT) and finite domain constraint satisfaction (CSP), exploring their complexity and practical algorithm design for applications in formal verification and related tasks. Education : Ph.D., Computer Science, University of Toronto, 2002 M.Sc., Computing Science, Simon Fraser University, 1993 B.Sc., Cognitive Science and Artificial Intelligence, University of Toronto, 1989 Research Interests : Mitchell's work bridges mathematical logic and computer science, emphasizing SAT-based problem solving, constraint modeling languages, and automated reasoning. His contributions include advancements in clause learning, resolution complexity, and declarative programming frameworks for solving NP problems. He has developed tools like MXC and Enfragmo, which apply SAT techniques to real-world applications. Students : Mitchell has advised numerous graduate students, including current PhD candidates Mona Mehdizadeh and Sima Jamali, and past advisees such as Sahba Etezad, Heng Liu, and Faraz Hach. His students' work spans algorithm optimization, constraint satisfaction, and formal verification. Labs/Teams : He is a member of the Computational Logic Laboratory at SFU, contributing to research in logic-based problem-solving and algorithm development.

پروفایل رسمی دانشگاه

Holger H. Hoosمشاهده پروفایل

استاد

University of British ColumbiaCanada

Holger H. Hoos is a Professor at the University of British Columbia's Computer Science Department, affiliated with the Institute for Computational Intelligence and Cognitive Systems (ICICS) and the Peter-Wall Institute for Advanced Studies. As of 2017, his primary affiliation shifted to Leiden University (Netherlands), though he remains connected to UBC. His research focuses on algorithmics, bioinformatics, computational intelligence, and computer music, with significant contributions to stochastic local search, empirical algorithmics, and SAT solving. Education: Ph.D. (Dr.rer.nat) in Computer Science from TU Darmstadt (1998), postdoctoral fellow at UBC. He has led the BETA Lab and SALIERI Project, exploring biomolecular structure prediction and music algorithms. Research interests span stochastic algorithms, RNA structure prediction, automated algorithm configuration, and interdisciplinary applications like flow cytometry analysis. His work bridges theoretical foundations with empirical methods, emphasizing practical problem-solving. Awards include the AAAI Fellowship, multiple best paper awards (GECCO 2020, IJCAI-JAIR 2010), and leadership roles in conferences like AAAI and LION. He has advised over 30 students, contributing to impactful projects in bioinformatics and AI. Labs/Teams: Founder of the BETA Lab (Bioinformatics, Theoretical and Empirical Algorithms), member of the Laboratory for Computational Intelligence (LCI), and collaborator on SALIERI (Computer Music).

پروفایل رسمی دانشگاه

Curtis Brightمشاهده پروفایل

استادیار

University of WindsorCanada

Dr. Curtis Bright is an Assistant Professor in the School of Computer Science at the University of Windsor. He holds a PhD in Computer Science from the University of Waterloo (2017) and an MMath in Computational Mathematics from the same institution (2004). His research focuses on computer-assisted proofs, automated reasoning, symbolic computation, and discrete mathematics. He leads the MathCheck project, which combines satisfiability checking (SAT) and computer algebra systems (CAS) for mathematical conjectures verification. **Education:** PhD, Computer Science, University of Waterloo (2017) MMath, Computational Mathematics, University of Waterloo (2004) **Research Interests:** Dr. Bright specializes in automating mathematics, particularly verification and counterexample generation of conjectures, computer-assisted proofs, automated reasoning algorithms, satisfiability checking, and symbolic computation. His work bridges combinatorics, experimental mathematics, and computational algebra. Recent projects include solving Lam’s problem via SAT and exhaustive generation, resolving the abc conjecture’s lower bound, and producing certificates for Ramsey numbers R(3,8) and R(3,9). **Awards:** Jacques Calmet Best Paper Award (2021) ACA Early Researcher Award (2022) Judges’ Choice Award at Maple Conference (2021) **Advising & Grants:** He supervises multiple PhD, MSc, and undergraduate students, including recent graduates Sadman Sakib (MSc), Nahiyan Alamgir (MSc), and Yameen Ajani (MSc). His research has been supported by grants such as 170 CPU years and 20TB storage from DRAC for Kochen-Specker system studies. He co-leads the MathCheck group at Waterloo and the Algorithms & Mathematics group at Windsor. **Labs/Teams:** His work is anchored in the MathCheck project and collaborations with institutions like Carleton University and the University of Waterloo. His team develops innovative SAT+CAS methodologies for combinatorial and mathematical challenges.

پروفایل رسمی دانشگاه

Dave Tompkinsمشاهده پروفایل

دانشیار

University of WaterlooCanada

Dave Tompkins is an Associate Professor in the Department of Computer Science at the University of Waterloo and serves as Associate Director of Undergraduate Studies. He holds a Ph.D. from the University of British Columbia (2010), an M.A.Sc. (2000), and dual B.Sc./B.E.Sc. degrees from the University of Western Ontario (1994/1996). His teaching focus is on the core computer science curriculum, emphasizing foundational courses. His research interests span SAT solving, stochastic local search (SLS) algorithms, algorithm configuration, and image compression techniques. Dr. Tompkins has contributed extensively to the field of SAT solving through publications on methods like Adaptive Novelty+, Dynamic Scoring Functions, and UBCSAT tool development. His work also includes studies on variable selection heuristics and algorithm adaptation strategies. Notably, he has explored warped landscapes in SAT solving and reactive scaling techniques. Earlier research involved bi-level image compression using JBIG2 standards, addressing challenges in lossy and lossless coding. His publication trends reflect a strong emphasis on algorithm design and analysis, particularly in combinatorial optimization and constraint satisfaction problems. While no scientific awards are explicitly listed, his contributions to SLS methodologies and SAT solving have likely impacted the field significantly. No grants or advising records are documented in the provided materials.

پروفایل رسمی دانشگاه

Calin Antonمشاهده پروفایل

دانشیار

MacEwan UniversityCanada

Dr. Calin Anton is an Associate Professor in the Department of Computer Science at MacEwan University, where he has taught since 2008. He holds a PhD from the University of Alberta, specializing in computing science, and previously served as an Assistant Professor at Augustana Faculty (University of Alberta) from 2005 to 2007. His research focuses on generating hard satisfiable instances of the satisfiability problem using random subgraph isomorphism and exploring empirical algorithms and artificial intelligence. Education: B.Sc. in Computing Science (1996), University of Bucharest M.Sc. in Computing Science (1997), University of Bucharest PhD in Computing Science (2005), University of Alberta His research interests include satisfiability problem analysis, heuristic search, and computational complexity. Recent work involves transitioning towards computer security. He has collaborated with undergraduate students on instance generators used in SAT solver competitions. Awards & Funding: NSERC Discovery Grant (2006–2010) MacEwan University Research Funds (2010–2012) Conference Travel Support (2010–2011) Teaching & Advising: Teaches courses in algorithmics, artificial intelligence, and foundational computer science. Available to supervise senior independent study projects.

پروفایل رسمی دانشگاه

Yong Gaoمشاهده پروفایل

استاد

University of British ColumbiaCanada

Yong Gao is a Professor of Computer Science, Data Science, and Mathematics at the University of British Columbia (UBC) Okanagan, affiliated with the Irving K. Barber Faculty of Science. He holds a PhD from the University of Alberta and leads research in algorithmic and computational problems in artificial intelligence, network science, and computational biology. His work emphasizes graph theory, probabilistic methods, and applications in social media and biological systems. Educational Background : PhD in Computer Science, University of Alberta Research Interests : Algorithmic foundations of AI and network science Graph-based methods for computational biology and social media analysis Probabilistic modeling of complex systems Awards & Grants : Recipient of multiple NSERC Discovery Grants (2006–2019) UBC Okanagan Startup Grant (2005–2008) Senior Member, Association for the Advancement of AI (AAAI) Professional Roles : Member, Centre for Optimization, Convex Analysis and Nonsmooth Analysis Graduate student supervisor Teaching : Courses in algorithm design, artificial intelligence, discrete mathematics, and network science.

پروفایل رسمی دانشگاه