Vijay Ganesh

AAAI Conference 2025 Short Paper

Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)

• Zhengyang Lu
• Po-Chun Chien
• Nian-Ze Lee
• Vijay Ganesh

We build the first machine-learning-based algorithm selection tool for hardware verification described in the Btor2 format. In addition to hardware verifiers, our tool also selects from a set of software verifiers to solve a given Btor2 instance, enabled by a Btor2-to-C translator. We propose two embeddings for a Btor2 instance, Bag of Keywords and Bit-Width Aggregation. Pairwise classifiers are applied for algorithm selection. Upon evaluation, our tool Btor2-Select solves 30.0% more instances and reduces PAR-2 by 50.2%, compared to the PDR implementation in the HWMCC'20 winner model checker AVR. Measured by the Shapley values, the software verifiers collectively contributed 27.2% to Btor2-Select's performance.

JAIR Journal 2025 Journal Article

Improving and Understanding the Power of Satisfaction-Driven Clause Learning

• Albert Oliveras
• Chunxiao Li
• Darryl Wu
• Jonathan Chung
• Vijay Ganesh

In this paper, we explain how to improve Satisfaction-Driven Clause Learning (SDCL) SAT solvers by using a MaxSAT-based technique that enables them to learn shorter, and hence better, redundant clauses. A thorough empirical evaluation of an implementation on the MapleSAT solver shows that the resulting system solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver. Additionally we improve the understanding of the power of these solvers by proving that, given a refutation of a formula that consists of resolution and redundant-clause addition steps, an SDCL solver is able to produce a proof whose size is polynomial with respect to the size of the original refutation.

AAAI Conference 2025 Short Paper

LLM Stinger: Jailbreaking LLMs Using RL Fine-Tuned LLMs (Student Abstract)

• Piyush Jha
• Arnav Arora
• Vijay Ganesh

We introduce LLM Stinger, a novel approach that leverages Large Language Models (LLMs) to automatically generate adversarial suffixes for jailbreak attacks. Unlike traditional methods, which require complex prompt engineering or white-box access, LLM Stinger uses a reinforcement learning (RL) loop to fine-tune an attacker LLM, generating new suffixes based on existing attacks for harmful questions from the HarmBench benchmark. Our method significantly outperforms existing red-teaming approaches (we compared against 15 of the latest methods), achieving a +57.2% improvement in Attack Success Rate (ASR) on LLaMA2-7B-chat and a +50.3% ASR increase on Claude 2, both models known for their extensive safety measures. Additionally, we achieved a 94.97% ASR on GPT-3.5 and 99.4% on Gemma-2B-it, demonstrating the robustness and adaptability of LLM Stinger across open and closed-source models.

IJCAI Conference 2025 Conference Paper

Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3, 8) and R(3, 9) Problems

• Zhengyu Li
• Conor Duggan
• Curtis Bright
• Vijay Ganesh

The Ramsey problem R(3, k) seeks to determine the smallest value of n such that any red/blue edge coloring of the complete graph on n vertices must either contain a blue triangle (3-clique) or a red clique of size k. Despite its significance, many previous computational results for the Ramsey R(3, k) problem such as R(3, 8) and R(3, 9) lack formal verification. To address this issue, we use the software MathCheck to generate certificates for Ramsey problems R(3, 8) and R(3, 9) (and symmetrically R(8, 3) and R(9, 3)) by integrating a Boolean satisfiability (SAT) solver with a computer algebra system (CAS). Our SAT+CAS approach significantly outperforms traditional SAT-only methods, demonstrating an improvement of several orders of magnitude in runtime. For instance, our SAT+CAS approach solves R(3, 8) (resp. , R(8, 3)) sequentially in 59 hours (resp. , in 11 hours), while a SAT-only approach using state-of-the-art CaDiCaL solver times out after 7 days. Additionally, in order to be able to scale to harder Ramsey problems R(3, 9) and R(9, 3) we further optimized our SAT+CAS tool using a parallelized cube-and-conquer approach. Our results provide the first independently verifiable certificates for these Ramsey numbers, ensuring both correctness and completeness of the exhaustive search process of our SAT+CAS tool.

AAAI Conference 2024 Short Paper

A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)

• Conor Duggan
• Zhengyu Li
• Curtis Bright
• Vijay Ganesh

The Ramsey problem R(3,8) asks for the smallest n such that every red/blue coloring of the complete graph on n vertices must contain either a blue triangle or a red 8-clique. We provide the first certifiable proof that R(3,8) = 28, automatically generated by a combination of Boolean satisfiability (SAT) solver and a computer algebra system (CAS). This SAT+CAS combination is significantly faster than a SAT-only approach. While the R(3,8) problem was first computationally solved by McKay and Min in 1992, it was not a verifiable proof. The SAT+CAS method that we use for our proof is very general and can be applied to a wide variety of combinatorial problems.

IJCAI Conference 2024 Conference Paper

A SAT Solver + Computer Algebra Attack on the Minimum Kochen–Specker Problem

• Zhengyu Li
• Curtis Bright
• Vijay Ganesh

One of the fundamental results in quantum foundations is the Kochen–Specker (KS) theorem, which states that any theory whose predictions agree with quantum mechanics must be contextual, i. e. , a quantum observation cannot be understood as revealing a pre-existing value. The theorem hinges on the existence of a mathematical object called a KS vector system. While many KS vector systems are known, the problem of finding the minimum KS vector system in three dimensions (3D) has remained stubbornly open for over 55 years. To address the minimum KS problem, we present a new verifiable proof-producing method based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS) that uses an isomorph-free orderly generation technique that is very effective in pruning away large parts of the search space. Our method shows that a KS system in 3D must contain at least 24 vectors. We show that our sequential and parallel Cube-and-Conquer (CnC) SAT+CAS methods are significantly faster than SAT-only, CAS-only, and a prior CAS-based method of Uijlen and Westerbaan. Further, while our parallel pipeline is somewhat slower than the parallel CnC version of the recently introduced Satisfiability Modulo Theories (SMS) method, this is in part due to the overhead of proof generation. Finally, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a size of 40. 3 TiB in order 23.

AAAI Conference 2024 Short Paper

A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)

• Zhengyu Li
• Curtis Bright
• Vijay Ganesh

The problem of finding the minimum three-dimensional Kochen–Specker (KS) vector system, an important problem in quantum foundations, has remained open for over 55 years. We present a new method to address this problem based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS). Our approach improved the lower bound on the size of a KS system from 22 to 24. More importantly, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a proof size of 41.6 TiB for order 23. The efficiency is due to the powerful combination of SAT solvers and CAS-based orderly generation.

AAAI Conference 2024 Short Paper

BertRLFuzzer: A BERT and Reinforcement Learning Based Fuzzer (Student Abstract)

• Piyush Jha
• Joseph Scott
• Jaya Sriram Ganeshna
• Mudit Singh
• Vijay Ganesh

We present a novel tool BertRLFuzzer, a BERT and Reinforcement Learning (RL) based fuzzer aimed at finding security vulnerabilities for Web applications. BertRLFuzzer works as follows: given a set of seed inputs, the fuzzer performs grammar-adhering and attack-provoking mutation operations on them to generate candidate attack vectors. The key insight of BertRLFuzzer is the use of RL with a BERT model as an agent to guide the fuzzer to efficiently learn grammar-adhering and attack-provoking mutation operators. In order to establish the efficacy of BertRLFuzzer we compare it against a total of 13 black box and white box fuzzers over a benchmark of 9 victim websites with over 16K LOC. We observed a significant improvement, relative to the nearest competing tool in terms of time to first attack (54% less), new vulnerabilities found (17 new vulnerabilities), and attack rate (4.4% more attack vectors generated).

IJCAI Conference 2024 Conference Paper

Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

• Zhengyang Lu
• Stefan Siemer
• Piyush Jha
• Joel Day
• Florin Manea
• Vijay Ganesh

Modern SMT solvers, such as Z3, offer user-controllable strategies that allow solver users the ability to tailor solving strategies for their unique set of instances, thus dramatically enhancing the solver performance for their specific use cases. However, this approach of strategy customization presents a significant challenge: handcrafting an optimized strategy for a class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address this problem of automated SMT strategy synthesis via a novel Monte Carlo Tree Search (MCTS) based method. Our method treats strategy synthesis as a sequential decision-making process, whose search tree corresponds to the strategy space, and employs MCTS to navigate this vast search space. The key innovations that enable our method to identify effective strategies, while keeping costs low, are the ideas of layered and staged MCTS search. These novel heuristics allow for a deeper and more efficient exploration of the strategy space, enabling us to synthesize more effective strategies than the default ones in state-of-the-art (SOTA) SMT solvers. We implement our method, dubbed Z3alpha, as part of the Z3 SMT solver. Through extensive evaluations across six important SMT logics, Z3alpha demonstrates superior performance compared to the SOTA synthesis tool FastSMT, the default Z3 solver, and the CVC5 solver on most benchmarks. Remarkably, on a challenging QF_BV benchmark set, Z3alpha solves 42. 7% more instances than the default strategy in Z3.

NeurIPS Conference 2023 Conference Paper

Grounding Neural Inference with Satisfiability Modulo Theories

• Zifan Wang
• Saranya Vijayakumar
• Kaiji Lu
• Vijay Ganesh
• Somesh Jha
• Matt Fredrikson

Recent techniques that integrate solver layers into Deep Neural Networks (DNNs) have shown promise in bridging a long-standing gap between inductive learning and symbolic reasoning techniques. In this paper we present a set of techniques for integrating Satisfiability Modulo Theories (SMT) solvers into the forward and backward passes of a deep network layer, called SMTLayer. Using this approach, one can encode rich domain knowledge into the network in the form of mathematical formulas. In the forward pass, the solver uses symbols produced by prior layers, along with these formulas, to construct inferences; in the backward pass, the solver informs updates to the network, driving it towards representations that are compatible with the solver's theory. Notably, the solver need not be differentiable. We implement SMTLayer as a Pytorch module, and our empirical results show that it leads to models that 1) require fewer training samples than conventional models, 2) that are robust to certain types of covariate shift, and 3) that ultimately learn representations that are consistent with symbolic knowledge, and thus naturally interpretable.

AAAI Conference 2023 Short Paper

Robust Training for AC-OPF (Student Abstract)

• Fuat Can Beylunioglu
• Mehrdad Pirnia
• P. Robert Duimering
• Vijay Ganesh

Electricity network operators use computationally demanding mathematical models to optimize AC power flow (AC-OPF). Recent work applies neural networks (NN) rather than optimization methods to estimate locally optimal solutions. However, NN training data is costly and current models cannot guarantee optimal or feasible solutions. This study proposes a robust NN training approach, which starts with a small amount of seed training data and uses iterative feedback to generate additional data in regions where the model makes poor predictions. The method is applied to non-linear univariate and multivariate test functions, and an IEEE 6-bus AC-OPF system. Results suggest robust training can achieve NN prediction performance similar to, or better than, regular NN training, while using significantly less data.

TCS Journal 2023 Journal Article

Towards more efficient methods for solving regular-expression heavy string constraints

• Murphy Berzish
• Joel D. Day
• Vijay Ganesh
• Mitja Kulczynski
• Florin Manea
• Federico Mora
• Dirk Nowotka

IJCAI Conference 2022 Conference Paper

A Solver + Gradient Descent Training Algorithm for Deep Neural Networks

• Dhananjay Ashok
• Vineel Nagisetty
• Christopher Srinivasa
• Vijay Ganesh

We present a novel hybrid algorithm for training Deep Neural Networks that combines the state-of-the-art Gradient Descent (GD) method with a Mixed Integer Linear Programming (MILP) solver, outperforming GD and variants in terms of accuracy, as well as resource and data efficiency for both regression and classification tasks. Our GD+Solver hybrid algorithm, called GDSolver, works as follows: given a DNN D as input, GDSolver invokes GD to partially train D until it gets stuck in a local minima, at which point GDSolver invokes an MILP solver to exhaustively search a region of the loss landscape around the weight assignments of D’s final layer parameters with the goal of tunnelling through and escaping the local minima. The process is repeated until desired accuracy is achieved. In our experiments, we find that GDSolver not only scales well to additional data and very large model sizes, but also outperforms all other competing methods in terms of rates of convergence and data efficiency. For regression tasks, GDSolver produced models that, on average, had 31. 5% lower MSE in 48% less time, and for classification tasks on MNIST and CIFAR10, GDSolver was able to achieve the highest accuracy over all competing methods, using only 50% of the training data that GD baselines required.

AAAI Conference 2021 Conference Paper

A SAT-based Resolution of Lam’s Problem

• Curtis Bright
• Kevin K. H. Cheung
• Brett Stevens
• Ilias Kotsireas
• Vijay Ganesh

In 1989, computer searches by Lam, Thiel, and Swiercz experimentally resolved Lam’s problem from projective geometry—the long-standing problem of determining if a projective plane of order ten exists. Both the original search and an independent verification in 2011 discovered no such projective plane. However, these searches were each performed using highly specialized custom-written code and did not produce nonexistence certificates. In this paper, we resolve Lam’s problem by translating the problem into Boolean logic and use satisfiability (SAT) solvers to produce nonexistence certificates that can be verified by a third party. Our work uncovered consistency issues in both previous searches—highlighting the difficulty of relying on specialpurpose search code for nonexistence results.

AAAI Conference 2021 Conference Paper

Amnesiac Machine Learning

• Laura Graves
• Vineel Nagisetty
• Vijay Ganesh

The Right to be Forgotten is part of the recently enacted General Data Protection Regulation (GDPR) law that affects any data holder that has data on European Union residents. It gives EU residents the ability to request deletion of their personal data, including training records used to train machine learning models. Unfortunately, Deep Neural Network models are vulnerable to information leaking attacks such as model inversion attacks which extract class information from a trained model and membership inference attacks which determine the presence of an example in a model’s training data. If a malicious party can mount an attack and learn private information that was meant to be removed, then it implies that the model owner has not properly protected their user’s rights and their models may not be compliant with the GDPR law. In this paper, we present two efficient methods that address this question of how a model owner or data holder may delete personal data from models in such a way that they may not be vulnerable to model inversion and membership inference attacks while maintaining model efficacy. We start by presenting a real-world threat model that shows that simply removing training data is insufficient to protect users. We follow that up with two data removal methods, namely Unlearning and Amnesiac Unlearning, that enable model owners to protect themselves against such attacks while being compliant with regulations. We provide extensive empirical analysis that show that these methods are indeed efficient, safe to apply, effectively remove learned information about sensitive data from trained models while maintaining model efficacy.

AAAI Conference 2021 Short Paper

Logic Guided Genetic Algorithms (Student Abstract)

• Dhananjay Ashok
• Joseph Scott
• Sebastian J. Wetzel
• Maysum Panju
• Vijay Ganesh

We present a novel Auxiliary Truth enhanced Genetic Algorithm (GA) that uses logical or mathematical constraints as a means of data augmentation as well as to compute loss with the aim of increasing both data efficiency and accuracy of symbolic regression (SR) algorithms. Our method, logicguided genetic algorithm (LGGA), takes as input a set of labelled datapoints and auxiliary truths (AT) (mathematical facts known a priori about the unknown function the regressor aims to learn) and outputs a specially generated and curated dataset that can be used with any SR method. We evaluate LGGA against state-of-the-art SR tools, namely, Eureqa and TuringBot, and find that using these SR tools in conjunction with LGGA results in them solving up to 30. 0% more equations, needing only a fraction of the amount of data compared to the same tool without LGGA, i. e. , resulting in up to a 61. 9% improvement in data efficiency.

AAAI Conference 2020 Short Paper

LGML: Logic Guided Machine Learning (Student Abstract)

• Joseph Scott
• Maysum Panju
• Vijay Ganesh

We introduce Logic Guided Machine Learning (LGML), a novel approach that symbiotically combines machine learning (ML) and logic solvers to learn mathematical functions from data. LGML consists of two phases, namely a learning-phase and a logic-phase with a corrective feedback loop, such that, the learning-phase learns symbolic expressions from input data, and the logic-phase cross verifies the consistency of the learned expression with known auxiliary truths. If inconsistent, the logic-phase feeds back "counterexamples" to the learning-phase. This process is repeated until the learned expression is consistent with auxiliary truth. Using LGML, we were able to learn expressions that correspond to the Pythagorean theorem and the sine function, with several orders of magnitude improvements in data efficiency compared to an approach based on an out-of-the-box multi-layered perceptron (MLP).

IJCAI Conference 2020 Conference Paper

Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem

• Curtis Bright
• Kevin K. H. Cheung
• Brett Stevens
• Ilias Kotsireas
• Vijay Ganesh

In the 1970s and 1980s, searches performed by L. Carter, C. Lam, L. Thiel, and S. Swiercz showed that projective planes of order ten with weight 16 codewords do not exist. These searches required highly specialized and optimized computer programs and required about 2, 000 hours of computing time on mainframe and supermini computers. In 2010, these searches were verified by D. Roy using an optimized C program and 16, 000 hours on a cluster of desktop machines. We performed a verification of these searches by reducing the problem to the Boolean satisfiability problem (SAT). Our verification uses the cube-and-conquer SAT solving paradigm, symmetry breaking techniques using the computer algebra system Maple, and a result of Carter that there are ten nonisomorphic cases to check. Our searches completed in about 30 hours on a desktop machine and produced nonexistence proofs of about 1 terabyte in the DRAT (deletion resolution asymmetric tautology) format.

AAAI Conference 2019 Conference Paper

A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples

• Curtis Bright
• Dragomir Ž. Ðoković
• Ilias Kotsireas
• Vijay Ganesh

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 and a new set of good matrices of order 57. We also find that circulant good matrices do not exist in the orders 51, 63, and 69, thereby finding three new counterexamples to the conjecture that such matrices exist in all odd orders. Additionally, we prove a new relationship between the entries of good matrices and exploit this relationship in our enumeration algorithm. Our method applies the SAT+CAS paradigm of combining computer algebra functionality with modern SAT solvers to efficiently search large spaces which are specified by both algebraic and logical constraints.

AAAI Conference 2018 Conference Paper

A SAT+CAS Method for Enumerating Williamson Matrices of Even Order

• Curtis Bright
• Ilias Kotsireas
• Vijay Ganesh

We present for the first time an exhaustive enumeration of Williamson matrices of even order n < 65. The search method relies on the novel SAT+CAS paradigm of coupling SAT solvers with computer algebra systems so as to take advantage of the advances made in both the field of satisfiability checking and the field of symbolic computation. Additionally, we use a programmatic SAT solver which allows conflict clauses to be learned programmatically, through a piece of code specifically tailored to the domain area. Prior to our work, Williamson matrices had only been enumerated for odd orders n < 60, so our work increases the bounds that Williamson matrices have been enumerated up to and provides the first enumeration of Williamson matrices of even order. Our results show that Williamson matrices of even order tend to be much more abundant than those of odd orders. In particular, Williamson matrices exist for every even order n < 65 but do not exist in orders 35, 47, 53, and 59.

IJCAI Conference 2018 Conference Paper

An Empirical Study of Branching Heuristics through the Lens of Global Learning Rate

• Jia Liang
• Hari Govind
• Pascal Poupart
• Krzysztof Czarnecki
• Vijay Ganesh

In this paper, we analyze a suite of 7 well-known branching heuristics proposed by the SAT community and show that the better heuristics tend to generate more learnt clauses per decision, a metric we define as the global learning rate (GLR). We propose GLR as a metric for the branching heuristic to optimize. We test our hypothesis by developing a new branching heuristic that maximizes GLR greedily. We show empirically that this heuristic achieves very high GLR and interestingly very low literal block distance (LBD) over the learnt clauses. In our experiments this greedy branching heuristic enables the solver to solve instances faster than VSIDS, when the branching time is taken out of the equation. This experiment is a good proof of concept that a branching heuristic maximizing GLR will lead to good solver performance modulo the computational overhead. Finally, we propose a new branching heuristic, called SGDB, that uses machine learning to cheapily approximate greedy maximization of GLR. We show experimentally that SGDB performs on par with the VSIDS branching heuristic.

AAAI Conference 2016 Conference Paper

Exponential Recency Weighted Average Branching Heuristic for SAT Solvers

• Jia Liang
• Vijay Ganesh
• Pascal Poupart
• Krzysztof Czarnecki

Modern conflict-driven clause-learning SAT solvers routinely solve large real-world instances with millions of clauses and variables in them. Their success crucially depends on effective branching heuristics. In this paper, we propose a new branching heuristic inspired by the exponential recency weighted average algorithm used to solve the bandit problem. The branching heuristic, we call CHB, learns online which variables to branch on by leveraging the feedback received from conflict analysis. We evaluated CHB on 1200 instances from the SAT Competition 2013 and 2014 instances, and showed that CHB solves significantly more instances than VSIDS, currently the most effective branching heuristic in widespread use. More precisely, we implemented CHB as part of the MiniSat and Glucose solvers, and performed an apple-to-apple comparison with their VSIDS-based variants. CHB-based MiniSat (resp. CHB-based Glucose) solved approximately 16. 1% (resp. 5. 6%) more instances than their VSIDS-based variants. Additionally, CHB-based solvers are much more efficient at constructing first preimage attacks on step-reduced SHA-1 and MD5 cryptographic hash functions, than their VSIDS-based counterparts. To the best of our knowledge, CHB is the first branching heuristic to solve significantly more instances than VSIDS on a large, diverse benchmark of real-world instances.

IJCAI Conference 2016 Conference Paper

MATHCHECK: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers

• Edward Zulkoski
• Vijay Ganesh
• Krzysztof Czarnecki

We present a method and an associated system, called MathCheck, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driven clause-learning SAT solver. SAT+CAS systems, a la MathCheck, can be used as an assistant by mathematicians to either counterexample or finitely verify open universal conjectures on any mathematical topic (e. g. , graph and number theory, algebra, geometry, etc. ) supported by the underlying CAS system. Such a SAT+CAS system combines the efficient search routines of modern SAT solvers, with the expressive power of CAS, thus complementing both. The key insight behind the power of the SAT+CAS combination is that the CAS system can help cut down the search-space of the SAT solver, by providing learned clauses that encode theory-specific lemmas, as it searches for a counterexample to the input conjecture. We demonstrate the efficacy of our approach on a long-standing open conjecture regarding matchings of hypercubes.