5 papers
MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs
Viresh Pati, Zhengyu Li, Piyush Jha +3
We introduce MathConstraint, a hard, adaptive benchmark for evaluating the combinatorial reasoning capabilities of LLMs. We combine constraint satisfaction problems with rigorous s…
SAT + NAUTY: Orderly Generation of Small Kochen-Specker Sets Containing the Smallest State-independent Contextuality Set
Zhengyu Li, Curtis Bright, Stefan Trandafir +2
We present a search for small Kochen-Specker (KS) sets in dimension 3, specifically targeting extensions of the 13-ray Yu-Oh set, which has been proven to be the minimal witness to…
AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems
Piyush Jha, Zhengyu Li, Zhengyang Lu +3
This paper introduces AlphaMapleSAT, a Cube-and-Conquer (CnC) parallel SAT solver that integrates Monte Carlo Tree Search (MCTS) with deductive feedback to efficiently solve challe…
Verified Certificates via SAT and Computer Algebra Systems for the Ramsey and Problems
Zhengyu Li, Conor Duggan, Curtis Bright +1
The Ramsey problem seeks to determine the smallest value of such that any red/blue edge coloring of the complete graph on vertices must either contain a blue tria…
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…