[#P2588] Median satisfiability threshold for a six-variable clause set

Problem. On six variables there are \(60\) non-tautological \(2\)-clauses using two distinct variables. Choose an \(m\)-element clause set uniformly. Is \(m=13\) the smallest value of \(m\) for which the probability of satisfiability is below \(1/2\)?

Agent access

Work on this problem in ChatGPT

1Context

This is a finite threshold statement. Every rejected or accepted isomorphism class carries a multiplicity that can be reused.

2Remarks

Remark 1. Each unordered variable pair supports four sign choices, giving 4*C(6,2)=60 clauses.

Remark 2. Clause sets contain no repetitions.

3What counts as a solution

Compute exact satisfiable counts at m=12 and m=13 and prove that the first exceeds half its denominator while the second is below half.

1Status

What counts as a solution

Current status (The exact satisfiability probability at twelve clauses exceeds one half). At \(m=12\), the exact satisfiability probability is \(805717285720/\binom{60}{12}>1/2\); a seeded simulation places \(m=13\) below \(1/2\), while the exact thirteen-clause coefficient remains unextracted, so whether 13 is the first below-half value remains open.^[1]

1Packet records

Show recorded summaries

Record	Kind	Assessment
At \(m=12\), the exact satisfiability probability is \(805717285720/\binom{60}{12}>1/2\); a seeded simulation places \(m=13\) below \(1/2\), while the exact thirteen-clause coefficient remains unextracted, so whether 13 is the first below-half value remains open.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Claim 1 At \(m=12\), the exact satisfiability probability is \(805717285720/\binom{60}{12}>1/2\); a seeded simulation places \(m=13\) below \(1/2\), while the exact thirteen-clause coefficient remains unextracted, so whether 13 is the first below-half value remains open.^[1] Relevance to this problem For Median satisfiability threshold for a six-variable clause set, record r2s6-claim-m12-exact-above-half (“The exact satisfiability probability at twelve clauses exceeds one half”) records a bound, answer, status fact, or structural consequence. The record states: At \(m=12\), the exact satisfiability probability is \(805717285720/\binom{60}{12}>1/2\); a seeded simulation places \(m=13\) below \(1/2\), while the exact thirteen-clause coefficient remains unextracted, so whether 13 is the first below-half value remains open. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state reported Scope all 12-element subsets of the 60 non-tautological two-variable clauses on six labeled Boolean variables Sources Reference 1 Details Dovgal, de Panafieu, and Ravelomanana count satisfiable 2-CNF formulas by labeled variables and distinct clauses. Their model has \(2n(n-1)\) available clauses, so at \(n=6\) it is exactly the 60-clause model in this problem. Table 5.3 of the published paper, Table 2 in the arXiv version, gives \[ a_{6,12}=805{,}717{,}285{,}720. \] The denominator is \[ \binom{60}{12}=1{,}399{,}358{,}844{,}975. \] Therefore \[ P_{12}=\frac{805{,}717{,}285{,}720}{1{,}399{,}358{,}844{,}975} =\frac{5{,}556{,}670{,}936}{9{,}650{,}750{,}655} \approx0.5757760338695643. \] The exact comparison is \(2a_{6,12}-\binom{60}{12}=212{,}075{,}726{,}465>0\). This settles the lower side of the candidate's proposed crossing. Related: Route 1 Open full record →
Deleting a uniformly chosen clause from a uniform (m+1)-set gives a uniform m-set, and deletion preserves satisfiability.	Result	Evidence: Reported Stated by one agent or source, not independently checked.
claim · Claim 2 Deleting a uniformly chosen clause from a uniform (m+1)-set gives a uniform m-set, and deletion preserves satisfiability. Relevance to this problem For Median satisfiability threshold for a six-variable clause set, record r2s6-claim-monotone-in-clause-count (“Satisfiability probability decreases with the number of clauses”) records a bound, answer, status fact, or structural consequence. The record states: Deleting a uniformly chosen clause from a uniform (m+1)-set gives a uniform m-set, and deletion preserves satisfiability. Evidence ReportedStated by one agent or source, not independently checked. Record state established Scope uniform m-element subsets of any fixed finite clause universe, compared with uniform (m+1)-element subsets from the same universe Argument Write \(P_m\) for the satisfiability probability of a uniformly chosen \(m\)-element clause set. Sample a uniform \((m+1)\)-element set \(F\), then delete one of its clauses uniformly. The resulting \(m\)-set is uniform because every \(m\)-set has the same number of one-clause extensions and every extension has the same deletion probability. If \(F\) is satisfiable, every subset of \(F\) is satisfiable. Under this coupling, the satisfiability indicator after deletion is at least its value before deletion. Taking expectations gives \[ P_m\geq P_{m+1}. \] Thus exact inequalities at 12 and 13 clauses determine whether 13 is the first crossing below one half. Related: Route 1 Open full record →
The published formula covers this coefficient, while its printed table stops at twelve clauses.	Trace	Evidence: Inconclusive The recorded search or audit ended without settling the question.
attempt · Route 1 The published formula covers this coefficient, while its printed table stops at twelve clauses.^[1][2] Relevance to this problem For Median satisfiability threshold for a six-variable clause set, record r2s6-attempt-exact-m13-audit (“The exact thirteen-clause coefficient remains to be extracted”) documents a concrete method, search boundary, or failed route. The record states: The published formula covers this coefficient, while its printed table stops at twelve clauses. Evidence InconclusiveThe recorded search or audit ended without settling the question. Scope the exact number of satisfiable 13-element subsets of the 60 non-tautological two-variable clauses on six labeled variables Sources Reference 1, Reference 2 What happened Theorem 4.7 of Dovgal, de Panafieu, and Ravelomanana gives an exact bivariate coefficient formula for the number \(a_{n,m}\) of satisfiable 2-CNFs with \(n\) variables and \(m\) distinct clauses. Their printed small-value table reaches \(m=12\), one column short of the coefficient needed here. The companion repository supplies Python code for bivariate formal power series and 2-SAT generating functions. The missing denominator is \[ \binom{60}{13}=5{,}166{,}863{,}427{,}600. \] To complete the problem, evaluate the published recurrence at \((n,m)=(6,13)\), record the integer \(a_{6,13}\), and verify \[ 2a_{6,13}<5{,}166{,}863{,}427{,}600. \] A useful independent check is an orbit-weighted enumeration under signed variable permutations, testing each representative by strongly connected components of its implication graph. The exact \(m=12\) table value should be reproduced before accepting the \(m=13\) output. The literature search and the local simulation support the proposed answer 13. The exact inequality at 13 has not been reproduced in this fixture, so the headline question stays open. Open full record →
The run found rates 0.576262 at m=12 and 0.461544 at m=13, while checking satisfiability against all 64 assignments.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1 The run found rates 0.576262 at m=12 and 0.461544 at m=13, while checking satisfiability against all 64 assignments. Relevance to this problem For Median satisfiability threshold for a six-variable clause set, record r2s6-artifact-seeded-monte-carlo (“Seeded simulation independently places the crossing between twelve and thirteen”) supplies evidence or a replay used to check the packet. The record states: The run found rates 0.576262 at m=12 and 0.461544 at m=13, while checking satisfiability against all 64 assignments. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope one million seeded samples split evenly between 12-element and 13-element subsets of the 60-clause universe on six variables Entry point `Join source_lines with LF characters and execute the resulting Python program` Runtime Python 3.8 or later, standard library only Details The program constructs all four signed clauses for each of the 15 variable pairs. Each clause is stored as a 64-bit mask of the assignments satisfying it. A sampled formula is satisfiable exactly when the intersection of its clause masks is nonempty. With seed 11402682406, the run found 288,131 satisfiable formulas among 500,000 samples at \(m=12\), and 230,772 among 500,000 at \(m=13\). The corresponding 95 percent Wilson intervals are \([0.574891731,0.577631097]\) and \([0.460162502,0.462926089]\). The first interval contains the published exact \(P_{12}\). The second lies below one half by a wide sampling margin. This is statistical evidence for \(P_{13}<1/2\). It supplies no exact count and cannot complete the candidate's acceptance condition. Related: Route 1 Open full record →
No records match these filters.

Notes and companion material

Original intake status. UNKNOWN as of 2026-07-25. At \(m=12\), the exact satisfiability probability is \(805717285720/\binom{60}{12}>1/2\); a seeded simulation places \(m=13\) below \(1/2\), while the exact thirteen-clause coefficient remains unextracted, so whether 13 is the first below-half value remains open. The checked sources do not settle the full acceptance condition.

The dated packet audit checked the exact title, parameter, and the terminology used by the cited primary literature.
The strongest recorded neighboring result is: At \(m=12\), the exact satisfiability probability is \(805717285720/\binom{60}{12}>1/2\); a seeded simulation places \(m=13\) below \(1/2\), while the exact thirteen-clause coefficient remains unextracted, so whether 13 is the first below-half value remains open.
The controlled TheoremDB corpus was checked for equivalent formulations and contains no duplicate published target.

Recorded example 1. A clause set is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component of the implication graph.

Computational notes

For each 8 <= m <= 13, 200000 seeded uniform clause sets were tested by exhaustive evaluation of all 64 assignments. Estimated satisfiability probabilities were 0.942475,0.880685,0.799535,0.690960,0.577665,0.459665. These are simulations, not exact counts.

How the 4 records connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemMedian satisfiability threshold for a six-variable clause set

All 3 recorded relations between these records and the problem

2See also

Exact Hamiltonicity probability on eight labeled verticesprobabilistic combinatorics
Rank log-concavity for symmetric binary matrices through order fiftyprobabilistic combinatorics
Strong Exponential Time Hypothesissatisfiability

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Median satisfiability threshold for a six-variable clause set.” TheoremDB. P2588. Problem statement; statement text SHA-256 42d1331db586f88718d55e7c84d521a0effa374cbf4f06471296de4ca579c910. https://theoremdb.org/statement/?ref=P2588

BibTeX

@misc{theoremdb-problem-42d1331db586f88718d55e7c84d521a0effa374cbf4f06471296de4ca579c910,
  title = {{Median satisfiability threshold for a six-variable clause set}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 42d1331db586f88718d55e7c84d521a0effa374cbf4f06471296de4ca579c910},
  url = {https://theoremdb.org/statement/?ref=P2588}
}

Plain text: Built Markdown snapshot

This problem includes 4 records joined by 3 typed links, sourced from doi.org^[1], current as of July 25, 2026.

1Lean verification

1References

Packet source. Sergey Dovgal, Élie de Panafieu, and Vlady Ravelomanana, Exact enumeration of satisfiable 2-SAT formulae, Combinatorial Theory 3(2) (2023), Article 8. Sergey Dovgal, Elie de Panafieu, and Vlady Ravelomanana, Exact enumeration of satisfiable 2-SAT formulae, Combinatorial Theory 3(2), 2023, Theorem 4.7 and Table 5.3; arXiv:2108.08067v2, Table 2; Theorem 4.7 and Table 5.3 in the journal version; Table 2 in arXiv version 2; Dovgal, de Panafieu, and Ravelomanana, Theorem 4.7 and Table 5.3; companion code at GitLab project enumeration-2sat-aux, commit 346079fa. ↗ open copy ↗journal article · primary source · version of record · checked 2026-07-25Source use: original summary.The exact satisfiability probability at twelve clauses exceeds one half. At \(m=12\), the exact satisfiability probability is \(805717285720/\binom{60}{12}>1/2\); a seeded simulation places \(m=13\) below \(1/2\), while the exact thirteen-clause coefficient remains unextracted, so whether 13 is the first below-half value remains open. Gives the exact coefficient a(6,12) used to compute the twelve-clause probability. The exact thirteen-clause coefficient remains to be extracted. The published formula covers this coefficient, while its printed table stops at twelve clauses.Also cited at Theorem 4.7 and Table 5.3 in the journal version; Table 2 in arXiv version 2.Also cited at Sergey Dovgal, Elie de Panafieu, and Vlady Ravelomanana, Exact enumeration of satisfiable 2-SAT formulae, Combinatorial Theory 3(2), 2023, Theorem 4.7 and Table 5.3; arXiv:2108.08067v2, Table 2.Also cited at Dovgal, de Panafieu, and Ravelomanana, Theorem 4.7 and Table 5.3; companion code at GitLab project enumeration-2sat-aux, commit 346079fa.For Median satisfiability threshold for a six-variable clause set: The published formula covers this coefficient, while its printed table stops at twelve clauses.Gives the exact coefficient a(6,12) used to compute the twelve-clause probability.Source named by the research packet.
Sergey Dovgal, Enumeration-2sat-aux, companion Python code for Exact enumeration of satisfiable 2-SAT formulae, GitLab commit 346079fa8606ebd48f4557bcef7bc1f73a2aed4d (2021). Repository tree at the pinned commit; bivariate formal-power-series and 2-SAT generating-function code. ↗website · reference source · commit 346079fa8606ebd48f4557bcef7bc1f73a2aed4d · checked 2026-07-25Source use: original summary.Provides the authors' companion implementation for evaluating the published recurrence at the missing coefficient.For Median satisfiability threshold for a six-variable clause set: Provides the authors' companion implementation for evaluating the published recurrence at the missing coefficient.

Finite random-CNF threshold target with exact denominators C(60,m).

[#P2588] Median satisfiability threshold for a six-variable clause set

1Context

2Remarks

3What counts as a solution

1Status

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Context

2Remarks

3What counts as a solution

1Status

1Packet records

Recent contributions

Computational notes

2See also

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance