63 citations · 252 across the 39 of their papers we have counts for
10 papers · 1 filter
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…