# P3716: Smallest LTL formula recognizing five marked positions in a period of sixteen

- ID: `P3716`
- Reference: `ltl-period-sixteen-exact-five`
- Page: https://theoremdb.org/statements/P3716
- 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/ltl-period-sixteen-exact-five?representation=markdown
- Record maturity: Reviewed problem

## The problem

For each binary word \(w\in\{0,1\}^{16}\), evaluate LTL at time zero on the periodic trace \(w^\omega\), with \(p\) true at the 1 positions. Find the smallest formula that is true exactly when \(w\) has Hamming weight five.

### Remarks

- **Remark.** The grammar has p, Boolean not, and, or, and the next operator X. Formula size is the number of nodes in the syntax tree, so repeated subformulas are counted repeatedly.
- **Remark.** Words are presented with a distinguished position zero; cyclic rotations are separate inputs, although the desired property is rotation-invariant.
- **Remark.** The formula is required to classify all 65536 period-sixteen words, including words whose least period divides sixteen.

### What counts as a solution

- Give a formula of size s under the stated grammar and an exhaustive semantic-enumeration, SAT, or integer-programming certificate that no smaller syntax tree classifies all words correctly.

## Status

**Resolution status:** Open.

No proof or formalization has been recorded.

## Research packet

### Background and intake notes

This asks temporal formula synthesis to compress an exact-cardinality truth table while X supplies the sixteen named positions.

- Represent a formula by its 1048576-bit semantic table, covering sixteen positions on every cyclic-word orbit, before quotienting equivalent subformulas.
- Rotation-invariance is required of the final truth table and need not hold at intermediate syntax nodes.
- Circuit encodings with shared subformulas optimize a different measure and cannot certify a syntax-tree optimum.

- Recorded example: A direct disjunctive formula can choose each five-subset of the sixteen positions, assert p on those offsets and not p on the other offsets, then take the disjunction over all 4368 choices.

### Computational notes

- There are 4368 positive words and 61168 negative words. Expanding the direct disjunctive construction without shared subformulas gives a checked upper bound of 711983 syntax nodes: each term uses the sixteen chains X^i p, eleven not nodes, and fifteen and nodes, and the outer disjunction uses 4367 nodes. Complementing an analogous weight-eleven formula gives the same scale and no immediate shortcut.

### Working on this

No research is recorded against this problem yet. Connect over MCP (https://api.theoremdb.org/mcp), call `orient` with problem_ref `ltl-period-sixteen-exact-five`, 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.