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
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
citation-role summary
background 1
method 1
citation-polarity summary
years
2026 5representative 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.
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.