GPT-6 Astra finds a 3SAT reduction showing monotone Dualization (minimal hypergraph transversals) has no polynomial algorithm under ETH
Awaiting review
Importance: major (4 of 5)The takeaway
Whether monotone Boolean dualization, equivalently enumerating all minimal transversals of a hypergraph, can be done in output-polynomial time has been open since the 1990s. A short preprint says no, assuming the Exponential Time Hypothesis, and its authors say the proof ‘was originally discovered by GPT-6 Astra’.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Preprint only
- Importance
- Major (4 of 5)
- Last verified
- 9 October 2026
Your AI and this story
- GPT-6 Astra161 days after its cutoff
- Claude Opus 5.5100 days after its cutoff
- Gemini 3.8 Flash191 days after its cutoff
- Grok 4.7130 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 100 days before it.
Key facts
- Problem: Dual asks whether two monotone CNFs are mutually dual (equivalently whether L = Tr(H) for hypergraphs H, L); Dualization asks to enumerate all minimal transversals of H. Their output-polynomial solvability is a long-standing open problem; Fredman–Khachiyan’s 1996 algorithm runs in N^O(log N / log log N)
- Theorem 1: a deterministic algorithm maps a 3CNF with n variables to hypergraphs H, L with L ⊆ Tr(H), of size 2^O(n^(2/3)(log n)^(1/3)), such that the formula is satisfiable iff L ≠ Tr(H)
- Consequence under ETH: no N^o(√(log N / log log N)) algorithm for Dual or Dualization, hence no polynomial-time algorithm for Dual and no output-polynomial enumeration for Dualization. It also rules out output-polynomial algorithms for the many problems known to be Dualization-hard (minimal dominating sets, which are ‘polynomially equivalent’, and others)
- AI disclosure (verbatim): ‘The proof of Theorem 1 was originally discovered by GPT-6 Astra (OpenAI). The authors subsequently reconstructed and revised the argument and rewrote its exposition. The same AI model was also used to prepare drafts of several parts of the manuscript. The authors have verified the correctness of the results and take full responsibility’
- The paper is short (main text ends on page 9); unrefereed; no Lean formalization; no expert reactions found on X, HN or blogs as of 9 Oct
- Not in OpenAI’s 6 Oct catalogue (no Dualization or transversal family in CONTENTS.md)
What happened
Dualization of monotone Boolean functions appears in databases, data mining, AI and convex geometry, and many enumeration problems are known to be exactly as hard. Fredman and Khachiyan showed in 1996 that it can be done in quasipolynomial time, and since then the question has been whether it can be done in output-polynomial time. Most work has found tractable special cases.
Kobayashi, Kurita and Wasa give a subexponential reduction from 3SAT: partial assignments to blocks of variables become vertices, and the formula is satisfiable exactly when a candidate list of minimal transversals is incomplete. With the Exponential Time Hypothesis this rules out polynomial-time duality testing. The authors say GPT-6 Astra discovered the proof of the main theorem.
Why it matters
If it holds, it closes the main question about Dualization conditionally. The quasipolynomial algorithm is close to optimal and a whole family of enumeration problems inherits the lower bound. Because the argument is short and the claim is strong, expert checking matters. Status: unrefereed.
What is disputed or not yet verified
| Verification | Unrefereed preprint; checked by the authors |
|---|
Sources
1 source from 1 site. Numbers match the chips in the text.
1 source: 1 primary
Primary
Changes
- Filed from the arXiv PDF