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

- ID: `P2588`
- Reference: `random-two-sat-six-median`
- Page: https://theoremdb.org/statements/P2588
- Record maturity: Reviewed problem with recorded work

## 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\)?

### Remarks

- **Remark.** Each unordered variable pair supports four sign choices, giving 4*C(6,2)=60 clauses.
- **Remark.** Clause sets contain no repetitions.

### What 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.

## Status

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](#reference-1)

## Work

### Evidence for the current status

**Claim 1 (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.

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.

### Background and intake notes

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

- Original intake status: Status unknown. Exact finite-n random 2-SAT counts may be available in the literature.
- Satisfiability depends only on the implication digraph. Count clause sets by canonical signed-graph type rather than testing all C(60,m) sets individually.
- It suffices to prove the two exact inequalities at m=12 and m=13 once monotonicity under adding clauses is stated.

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

### Other known results

- **Theorem 1** (established): Deleting a uniformly chosen clause from a uniform (m+1)-set gives a uniform m-set, and deletion preserves satisfiability.

### Prior approaches

- **Route 1** (inconclusive): The published formula covers this coefficient, while its printed table stops at twelve clauses. [1](#reference-1) [2](#reference-2)

### Runnable artifacts

- **Artifact 1** (reproduced): The run found rates 0.576262 at m=12 and 0.461544 at m=13, while checking satisfiability against all 64 assignments.

### 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.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `random-two-sat-six-median`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## References

1. <a id="reference-1"></a>Sergey Dovgal, Élie De Panafieu, and Vlady Ravelomanana, “Exact enumeration of satisfiable 2-SAT formulae”. Combinatorial Theory 3(2) (2023). DOI 10.5070/C63261985. 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 https://doi.org/10.5070/C63261985
   - 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
   - journal_article; primary source; version of record; open preprint arXiv:2108.08067v2; checked 2026-07-28
   - Open copy: https://arxiv.org/abs/2108.08067v2
   - Source use: original_summary
   - 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.
2. <a id="reference-2"></a>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 https://gitlab.com/sergey-dovgal/enumeration-2sat-aux/-/tree/346079fa8606ebd48f4557bcef7bc1f73a2aed4d
   - software; software source; commit 346079fa8606ebd48f4557bcef7bc1f73a2aed4d; checked 2026-07-28
   - Source use: citation_only
   - For Median satisfiability threshold for a six-variable clause set: Provides the authors' companion implementation for evaluating the published recurrence at the missing coefficient.
   - Provides the authors' companion implementation for evaluating the published recurrence at the missing coefficient.