BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Vijay Ganesh

Vijay Ganesh contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer ScienceSymbolic ComputationDiscrete MathematicsMachine Learningmath.COArtificial IntelligenceComputational ComplexityCryptography and Security

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
9works
0followers
8topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2026arXiv

MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs

We introduce MathConstraint, a hard, adaptive benchmark for evaluating the combinatorial reasoning capabilities of LLMs. We combine constraint satisfaction problems with rigorous solver-based verification and design an adaptive generator to create instances that remain challenging as the LLMs improve in their reasoning capabilities. Unlike existing benchmarks that quickly saturate on fixed datasets or use LLM-as-a-judge for checking solutions,MathConstraint uses parameterized problem types that enable scalable generation of arbitrarily difficult and automatically verifiable instances. We release MathConstraint-Easy ($266$ instances), on which frontier models achieve between $72.6\%$ (gemini-3.1-flash-lite) and $87.6\%$ (gpt-5.5) accuracy, and MathConstraint ($329$ instances) on which the same models drop to between $18.5\%$ (claude-4.6-sonnet) and $66.9\%$ (gpt-5.5) accuracy, demonstrating the resilience of our benchmark generator against rapid progress in LLM reasoning capabilities. We evaluate 12 frontier and open-weight models with and without access to a sandboxed Python environment that includes generic SAT/SMT solvers. Tool access roughly doubles frontier accuracy on MathConstraint (mean $+28$pp; up to $+52$pp for claude-4.6-sonnet). Further, halving the tool-call budget from $8$ to $4$ rounds erases up to $37$ points -- a sensitivity that most single-budget benchmarks miss. We release the generator, dataset, and evaluation harness as a robust environment for studying combinatorial reasoning and tool-use behavior under adversarially-tunable difficulty.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

A Solver + Gradient Descent Training Algorithm for Deep Neural Networks

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

xAI-GAN: Enhancing Generative Adversarial Networks via Explainable AI Systems

Generative Adversarial Networks (GANs) are a revolutionary class of Deep Neural Networks (DNNs) that have been successfully used to generate realistic images, music, text, and other data. However, GAN training presents many challenges, notably it can be very resource-intensive. A potential weakness in GANs is that it requires a lot of data for successful training and data collection can be an expensive process. Typically, the corrective feedback from discriminator DNNs to generator DNNs (namely, the discriminator's assessment of the generated example) is calculated using only one real-numbered value (loss). By contrast, we propose a new class of GAN we refer to as xAI-GAN that leverages recent advances in explainable AI (xAI) systems to provide a "richer" form of corrective feedback from discriminators to generators. Specifically, we modify the gradient descent process using xAI systems that specify the reason as to why the discriminator made the classification it did, thus providing the "richer" corrective feedback that helps the generator to better fool the discriminator. Using our approach, we observe xAI-GANs provide an improvement of up to 23.18% in the quality of generated images on both MNIST and FMNIST datasets over standard GANs as measured by Frechet Inception Distance (FID). We further compare xAI-GAN trained on 20% of the data with standard GAN trained on 100% of data on the CIFAR10 dataset and find that xAI-GAN still shows an improvement in FID score. Further, we compare our work with Differentiable Augmentation - which has been shown to make GANs data-efficient - and show that xAI-GANs outperform GANs trained on Differentiable Augmentation. Moreover, both techniques can be combined to produce even better results. Finally, we argue that xAI-GAN enables users greater control over how models learn than standard GANs.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords

Using techniques from the fields of symbolic computation and satisfiability checking we verify one of the cases used in the landmark result that projective planes of order ten do not exist. In particular, we show that there exist no projective planes of order ten that generate codewords of weight fifteen, a result first shown in 1973 via an exhaustive computer search. We provide a simple satisfiability (SAT) instance and a certificate of unsatisfiability that can be used to automatically verify this result for the first time. All previous demonstrations of this result have relied on search programs that are difficult or impossible to verify---in fact, our search found partial projective planes that were missed by previous searches due to previously undiscovered bugs. Furthermore, we show how the performance of the SAT solver can be dramatically increased by employing functionality from a computer algebra system (CAS). Our SAT+CAS search runs significantly faster than all other published searches verifying this result.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

CDCL(Crypto) SAT Solvers for Cryptanalysis

Over the last two decades, we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers on industrial problems from a variety of domains. The availability of such powerful general-purpose search tools as SAT solvers has led many researchers to propose SAT-based methods for cryptanalysis, including techniques for finding collisions in hash functions and breaking symmetric encryption schemes. Most of the previously proposed SAT-based cryptanalysis approaches are blackbox techniques, in the sense that the cryptanalysis problem is encoded as a SAT instance and then a CDCL SAT solver is invoked to solve the said instance. A weakness of this approach is that the encoding thus generated may be too large for any modern solver to solve efficiently. Perhaps a more important weakness of this approach is that the solver is in no way specialized or tuned to solve the given instance. To address these issues, we propose an approach called CDCL(Crypto) (inspired by the CDCL(T) paradigm in Satisfiability Modulo Theory solvers) to tailor the internal subroutines of the CDCL SAT solver with domain-specific knowledge about cryptographic primitives. Specifically, we extend the propagation and conflict analysis subroutines of CDCL solvers with specialized codes that have knowledge about the cryptographic primitive being analyzed by the solver. We demonstrate the power of this approach in the differential path and algebraic fault analysis of hash functions. Our initial results are very encouraging and reinforce the notion that this approach is a significant improvement over blackbox SAT-based cryptanalysis.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Nonexistence Certificates for Ovals in a Projective Plane of Order Ten

In 1983, a computer search was performed for ovals in a projective plane of order ten. The search was exhaustive and negative, implying that such ovals do not exist. However, no nonexistence certificates were produced by this search, and to the best of our knowledge the search has never been independently verified. In this paper, we rerun the search for ovals in a projective plane of order ten and produce a collection of nonexistence certificates that, when taken together, imply that such ovals do not exist. Our search program uses the cube-and-conquer paradigm from the field of satisfiability (SAT) checking, coupled with a programmatic SAT solver and the nauty symbolic computation library for removing symmetries from the search.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Towards a Complexity-theoretic Understanding of Restarts in SAT solvers

Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been well-established empirically, a theoretical explanation of whether restarts are indeed crucial to the power of CDCL solvers is lacking. In this paper, we prove a series of theoretical results that characterize the power of restarts for various models of SAT solvers. More precisely, we make the following contributions. First, we prove an exponential separation between a {\it drunk} randomized CDCL solver model with restarts and the same model without restarts using a family of satisfiable instances. Second, we show that the configuration of CDCL solver with VSIDS branching and restarts (with activities erased after restarts) is exponentially more powerful than the same configuration without restarts for a family of unsatisfiable instances. To the best of our knowledge, these are the first separation results involving restarts in the context of SAT solvers. Third, we show that restarts do not add any proof complexity-theoretic power vis-a-vis a number of models of CDCL and DPLL solvers with non-deterministic static variable and value selection.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem

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 2011, 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.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

Effective problem solving using SAT solvers

In this article we demonstrate how to solve a variety of problems and puzzles using the built-in SAT solver of the computer algebra system Maple. Once the problems have been encoded into Boolean logic, solutions can be found (or shown to not exist) automatically, without the need to implement any search algorithm. In particular, we describe how to solve the $n$-queens problem, how to generate and solve Sudoku puzzles, how to solve logic puzzles like the Einstein riddle, how to solve the 15-puzzle, how to solve the maximum clique problem, and finding Graeco-Latin squares.

0 citations0 reviewsNo code linkedOpen access