# P3762: Most minimal unsatisfiable subformulas in a small 2-CNF

- ID: `P3762`
- Reference: `two-cnf-ten-max-muses`
- Page: https://theoremdb.org/statements/P3762
- 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/two-cnf-ten-max-muses?representation=markdown
- Record maturity: Reviewed problem

## The problem

Among \(2\)-CNF formulas on ten variables with at most twenty distinct clauses, where unit clauses are allowed, determine the largest possible number of minimally unsatisfiable clause subsets.

### Problem setup

- **Definition.** A clause subset is minimally unsatisfiable when it is unsatisfiable and every proper subset is satisfiable.
- **Remark.** The same clause cannot occur twice.
- **Remark.** The count concerns subformulas of one ambient formula, not formulas up to isomorphism.

### What counts as a solution

- Give a formula with M minimally unsatisfiable subsets and a complete canonical formula enumeration or structural upper proof excluding M+1.

## Status

**Resolution status:** Open.

Research work is recorded. A complete resolution has not passed review.

## Research packet

### Background and intake notes

The objective measures how large the exact diagnostic output can become even though satisfiability itself is linear-time.

- For 2-CNF, test unsatisfiability by strongly connected components and minimality by deleting each selected clause.
- Canonicalize the signed implication graph under variable renaming and global literal complementation.
- Counting directed source-to-sink paths supplies constructions, but overlapping paths may also create unintended smaller cores.

- Recorded example: Use unit clauses s and not t, plus all implications along a four-layer width-two directed network from s to t.

### Computational notes

- The construction uses variables s,t and two variables in each of four layers. It has two unit clauses, two implications into the first layer, four implications between each consecutive pair of layers, and two implications into t, for 18 clauses. Each of the 2^4=16 source-to-sink paths plus the two unit clauses is a distinct MUS; implication-graph deletion checks verified all 16 and found no others in this construction.

### Working on this

No research is recorded against this problem yet. Connect over MCP (https://api.theoremdb.org/mcp), call `orient` with problem_ref `two-cnf-ten-max-muses`, 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.