63 citations · 252 across the 39 of their papers we have counts for
43 papers
A SAT Solver and 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 contex…
CoTran: An LLM-based Code Translator using Reinforcement Learning with Feedback from Compiler and Symbolic Execution
Prithwish Jana, Piyush Jha, Haoyang Ju +3
In this paper, we present an LLM-based code translation method and an associated tool called CoTran, that translates whole-programs from one high-level programming language to anot…
Limits of CDCL Learning via Merge Resolution
Marc Vinyals, Chunxiao Li, Noah Fleming +2
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. Howeve…
Formal Languages via Theories over Strings
Joel D. Day, Vijay Ganesh, Nathan Grewal +1
We investigate the properties of formal languages expressible in terms of formulas over quantifier-free theories of word equations, arithmetic over length constraints, and language…
On the proof complexity of MCSAT
Gereon Kremer, Erika Abraham, Vijay Ganesh
Satisfiability Modulo Theories (SMT) and SAT solvers are critical components in many formal software tools, primarily due to the fact that they are able to easily solve logical pro…
String Theories involving Regular Membership Predicates: From Practice to Theory and Back
Murphy Berzish, Joel D. Day, Vijay Ganesh +4
Widespread use of string solvers in formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this con…
On the Hierarchical Community Structure of Practical Boolean Formulas
Chunxiao Li, Jonathan Chung, Soham Mukherjee +5
Modern CDCL SAT solvers easily solve industrial instances containing tens of millions of variables and clauses, despite the theoretical intractability of the SAT problem. This gap…
A SAT-based Resolution of Lam's Problem
Curtis Bright, Kevin K. H. Cheung, Brett Stevens +2
In 1989, computer searches by Lam, Thiel, and Swiercz experimentally resolved Lam's problem from projective geometry$\unicode{x2014}$the long-standing problem of determining if a p…
Logic Guided Genetic Algorithms
Dhananjay Ashok, Joseph Scott, Sebastian Wetzel +2
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 (in conj…
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 g…
An SMT Solver for Regular Expressions and Linear Arithmetic over String Length
Murphy Berzish, Mitja Kulczynski, Federico Mora +4
We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement…
LGML: Logic Guided Machine Learning
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 with the goal of learning mathematical funct…
CDCL(Crypto) SAT Solvers for Cryptanalysis
Saeed Nejati, Vijay Ganesh
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…
Discovering Symmetry Invariants and Conserved Quantities by Interpreting Siamese Neural Networks
Sebastian J. Wetzel, Roger G. Melko, Joseph Scott +2
In this paper, we introduce interpretable Siamese Neural Networks (SNN) for similarity detection to the field of theoretical physics. More precisely, we apply SNNs to events in spe…
Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
Chunxiao Li, Noah Fleming, Marc Vinyals +2
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…
Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
Curtis Bright, Kevin K. H. Cheung, Brett Stevens +2
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 no…
Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem
Curtis Bright, Kevin K. H. Cheung, Brett Stevens +2
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 se…
A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords
Curtis Bright, Kevin Cheung, Brett Stevens +3
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 n…
MPro: Combining Static and Symbolic Analysis for Scalable Testing of Smart Contract
William Zhang, Sebastian Banescu, Leonardo Passos +2
Smart contracts are executable programs that enable the building of a programmable trust mechanism between multiple entities without the need of a trusted third-party. Researchers…
An Empirical Investigation of Randomized Defenses against Adversarial Attacks
Yannik Potdevin, Dirk Nowotka, Vijay Ganesh
In recent years, Deep Neural Networks (DNNs) have had a dramatic impact on a variety of problems that were long considered very difficult, e. g., image classification and automatic…
Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
Curtis Bright, Ilias Kotsireas, Albert Heinle +1
We use techniques from the fields of computer algebra and satisfiability checking to develop a new algorithm to search for complex Golay pairs. We implement this algorithm and use…
The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
Curtis Bright, Dragomir Ž. Đoković, Ilias Kotsireas +1
In this paper, we provide an overview of the SAT+CAS method that combines satisfiability checkers (SAT solvers) and computer algebra systems (CAS) to resolve combinatorial conjectu…
SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
Curtis Bright, Ilias Kotsireas, Vijay Ganesh
Over the last few decades, many distinct lines of research aimed at automating mathematics have been developed, including computer algebra systems (CASs) for mathematical modelling…
Interpolating Strong Induction
Hari Govind V K, Yakir Vizel, Vijay Ganesh +1
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, propert…