
On the proof complexity of MCSAT
Satisfiability Modulo Theories (SMT) and SAT solvers are critical compon...
read it

On the Hierarchical Community Structure of Practical Boolean Formulas
Modern CDCL SAT solvers easily solve industrial instances containing ten...
read it

A SATbased Resolution of Lam's Problem
In 1989, computer searches by Lam, Thiel, and Swiercz experimentally res...
read it

Logic Guided Genetic Algorithms
We present a novel Auxiliary Truth enhanced Genetic Algorithm (GA) that ...
read it

Amnesiac Machine Learning
The Right to be Forgotten is part of the recently enacted General Data P...
read it

LGML: Logic Guided Machine Learning
We introduce Logic Guided Machine Learning (LGML), a novel approach that...
read it

CDCL(Crypto) SAT Solvers for Cryptanalysis
Over the last two decades, we have seen a dramatic improvement in the ef...
read it

Discovering Symmetry Invariants and Conserved Quantities by Interpreting Siamese Neural Networks
In this paper, we introduce interpretable Siamese Neural Networks (SNN) ...
read it

Towards a Complexitytheoretic Understanding of Restarts in SAT solvers
Restarts are a widelyused class of techniques integral to the efficienc...
read it

LogicGAN: Logicguided Generative Adversarial Networks
Generative Adversarial Networks (GANs) are a revolutionary class of Deep...
read it

Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
In 1983, a computer search was performed for ovals in a projective plane...
read it

Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem
In the 1970s and 1980s, searches performed by L. Carter, C. Lam, L. Thie...
read it

A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords
Using techniques from the fields of symbolic computation and satisfiabil...
read it

MPro: Combining Static and Symbolic Analysis for Scalable Testing of Smart Contract
Smart contracts are executable programs that enable the building of a pr...
read it

An Empirical Investigation of Randomized Defenses against Adversarial Attacks
In recent years, Deep Neural Networks (DNNs) have had a dramatic impact ...
read it

Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
We use techniques from the fields of computer algebra and satisfiability...
read it

The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
In this paper, we provide an overview of the SAT+CAS method that combine...
read it

SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
Over the last few decades, many distinct lines of research aimed at auto...
read it

Effective problem solving using SAT solvers
In this article we demonstrate how to solve a variety of problems and pu...
read it

Interpolating Strong Induction
The principle of strong induction, also known as kinduction is one of t...
read it

New Infinite Families of Perfect Quaternion Sequences and Williamson Sequences
We present new constructions for perfect and odd perfect sequences over ...
read it

A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples
We enumerate all circulant good matrices with odd orders divisible by 3 ...
read it

Enumeration of Complex Golay Pairs via Programmatic SAT
We provide a complete enumeration of all complex Golay pairs of length u...
read it

Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
We employ tools from the fields of symbolic computation and satisfiabili...
read it

Applying Computer Algebra Systems and SAT Solvers to the Williamson Conjecture
We employ tools from the fields of symbolic computation and satisfiabili...
read it

The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability
The study of word equations (or the existential theory of equations over...
read it

Relating Complexitytheoretic Parameters with SAT Solver Performance
Over the years complexity theorists have proposed many structural parame...
read it

SATbased Analysis of Large Realworld Feature Models is Easy
Modern conflictdriven clauselearning (CDCL) Boolean SAT solvers provid...
read it
Vijay Ganesh
verfied profile
I am a computer scientist and applied logician, broadly interested in software engineering, security, AI and mathematics. Prior to joining Waterloo as a professor, I was a scientist at MIT (20072012) and completed my PhD from Stanford University (2007).
Research interests:
* ML for Logic, i.e., machine learning for logical reasoning (SAT/SMT solvers and theorem provers)
* Logic for ML, i.e., logical reasoning aimed at testing, analysis, verification, and security of ML
* Mathematical logic and complexity theory