New encodings achieve 2n + 2√(2n) + O(n^{1/3}) clauses for AtMostOne, refuting prior optimality conjectures, with a matching lower bound and grid compression yielding 2n + o(n) clauses for AtMost_k when k = o(n^{1/3}).
PySAT: A Python toolkit for prototyping with SAT oracles
7 Pith papers cite this work, alongside 246 external citations. Polarity classification is still indexing.
7
Pith papers citing it
246
external citations · OpenAlex
citation-role summary
background 1
method 1
citation-polarity summary
years
2026 7representative citing papers
Graph theory characterizes BVA reencodings, proving any 2-CNF on n variables can be reduced to roughly 0.396 n²/lg n clauses with minor extra steps and that at-most-one needs at least 3n-6 clauses.
A SAT-plus-LLM method discovers infinite families of doubly saturated Ramsey-good graphs, answering Grinstead and Roberts' 1982 question.
IdMAT and LIndA enable learning any regular language consistent with an incomplete inductive teacher by reducing uncertainties to incremental SAT solving for tasks like language separation and invariant synthesis.
The work provides an efficient algorithm for computing minimal input character explanations for finite automata decisions.
Bunny codes are qLDPC codes found via exhaustive search that achieve ~3x higher code rate than toric codes (periodic) and ~2x over rotated surface codes (open) when using CNOT+CXSWAP on nearest-neighbor connectivity, with some showing 10x lower logical error rates in simulation.
LLMs generate verifiable MaxSAT encodings from natural language, achieving over 80% acceptance rates on preference tasks where direct LLM reasoning fails.
citing papers explorer
-
Near-Optimal Encodings of Cardinality Constraints
New encodings achieve 2n + 2√(2n) + O(n^{1/3}) clauses for AtMostOne, refuting prior optimality conjectures, with a matching lower bound and grid compression yielding 2n + o(n) clauses for AtMost_k when k = o(n^{1/3}).
-
Automated Reencoding Meets Graph Theory
Graph theory characterizes BVA reencodings, proving any 2-CNF on n variables can be reduced to roughly 0.396 n²/lg n clauses with minor extra steps and that at-most-one needs at least 3n-6 clauses.
-
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
A SAT-plus-LLM method discovers infinite families of doubly saturated Ramsey-good graphs, answering Grinstead and Roberts' 1982 question.
-
Automata Learning with an Incomplete but Inductive Teacher (Technical Report)
IdMAT and LIndA enable learning any regular language consistent with an incomplete inductive teacher by reducing uncertainties to incremental SAT solving for tasks like language separation and invariant synthesis.
-
A Formal Framework for the Explanation of Finite Automata Decisions
The work provides an efficient algorithm for computing minimal input character explanations for finite automata decisions.
-
Bunny Codes: Broadening Superconducting Quantum Error Correction Capability through Advanced Control Engineering
Bunny codes are qLDPC codes found via exhaustive search that achieve ~3x higher code rate than toric codes (periodic) and ~2x over rotated surface codes (open) when using CNOT+CXSWAP on nearest-neighbor connectivity, with some showing 10x lower logical error rates in simulation.
-
Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability
LLMs generate verifiable MaxSAT encodings from natural language, achieving over 80% acceptance rates on preference tasks where direct LLM reasoning fails.