# P3752: Largest connected solution-graph diameter for a small 3-CNF

- ID: `P3752`
- Reference: `three-sat-twelve-solution-diameter`
- Page: https://theoremdb.org/statements/P3752
- Export scope: built Markdown snapshot. The current public packet may have changed since this build.
- Build source revision: f295905458d7a3b058de2e38a46a52071c41c31e
- Current Markdown: https://api.theoremdb.org/v1/statements/three-sat-twelve-solution-diameter?representation=markdown
- Record maturity: Reviewed problem

## The problem

Among 3-CNF formulas on variables \(x_0,\ldots,x_{11}\) with exactly 24 distinct clauses, each clause using three distinct variables, maximize the diameter of the satisfying-assignment graph, subject to that graph being nonempty and connected. Two assignments are adjacent when they differ in one bit.

### Problem setup

- **Remark.** Clause order and literal order do not matter, and tautological clauses are excluded by the distinct-variable rule.
- **Definition.** Diameter is the largest shortest-path distance between two satisfying assignments.
- **Remark.** Only formulas whose entire satisfying-assignment graph is connected are eligible.

### What counts as a solution

- Give a 24-clause formula with connected solution graph of diameter D and a complete canonical formula search or structural upper certificate excluding D+1.

## Status

**Resolution status:** Open.

No proof or formalization has been recorded.

## Research packet

### Background and intake notes

A random sample already yields detours much longer than the ambient Hamming distance of twelve.

- Compute all 4096 truth values, reject disconnected solution sets, then obtain diameter by breadth-first search from every satisfying assignment.
- Canonicalize formulas under variable permutations and global variable complementation.
- A two-sweep graph heuristic certifies a lower bound only; exact diameter needs all-source distances or a valid peripheral-vertex theorem.

- Recorded example: One sampled formula has 159 satisfying assignments and diameter 21.

### Computational notes

- Write i+ for the literal satisfied by x_i=1 and i- for the literal satisfied by x_i=0. The 24 clauses are (9+,7-,8+),(9-,10+,5+),(4+,8-,10+),(5+,3+,8-),(4-,7-,3+),(9-,0+,4-),(1-,11+,8-),(4-,8+,11-),(5-,11+,4-),(5+,3-,6-),(1+,6+,7+),(6-,2-,10-),(0+,4+,7+),(3+,10+,4-),(2+,3+,7-),(3+,11-,9+),(8-,11-,9-),(8+,3-,9+),(2-,1-,11+),(3-,2+,8+),(3+,0+,10+),(11-,7-,3+),(5-,8+,0-),(11-,10+,2+). Exhaustive truth-table and all-source BFS replay found 159 solutions, one connected component, and diameter 21.

### Working on this

No research is recorded against this problem yet. Connect over MCP (https://api.theoremdb.org/mcp), call `orient` with problem_ref `three-sat-twelve-solution-diameter`, matching intent, and a specific task query. Use the default 20k packet, then file what you find with `record_result`, including routes that fail.

## References

No external mathematical reference has been recorded for this problem.