Paid Dense Clause Word Conversion

Abstract

A fixed finite word machine densely names every appearing variable and preserves the ordinary clause count.

Theorem 1.1 (Total raw words, clean finite execution and assignment transport).

$$\forall w\in \mathrm{List}\left(Bool\right),\mathrm{Nonempty}\left(\mathrm{EvalsToInTime}\left(\mathrm{step}\left(denseMachine\right),\mathrm{initList}\left(denseMachine,w\right),\mathrm{some}\left(\mathrm{haltList}\left(denseMachine,\mathrm{denseOutput}\left(w\right)\right)\right),80\cdot {\left(\mathrm{length}\left(w\right)+1\right)}^2\right)\right)\wedge \left(\mathrm{length}\left(\mathrm{denseOutput}\left(w\right)\right)\le \mathrm{length}{\left(w\right)}^2+8\cdot \mathrm{length}\left(w\right)+7\wedge \left(\mathrm{readWord}\left(false,\mathrm{denseOutput}\left(w\right)\right)=\mathrm{some}\left(\mathrm{densePrepared}\left(w\right)\right)\wedge \left(\left(\forall c\in Clause,c\in \mathrm{snd}\left(\mathrm{densePrepared}\left(w\right)\right)\Rightarrow \mathrm{length}\left(c\right)\le 3\right)\wedge \mathrm{unaryCount}\left(\mathrm{snd}\left(\mathrm{densePrepared}\left(w\right)\right)\right)=\mathrm{rawCount}\left(w\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Computability/DenseClauseConversion.dense_word_run (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source problem counts assignments to exactly the distinct canonical binary names appearing in the decoded ordinary clauses. A malformed word has count zero. The dictionary retains the rightmost occurrence of each name, and its first-index lookup determines the dense unary variable.

One fixed eighteen-stack Boolean machine runs the whole-word parser, constructs the dictionary with paid comparisons and restoration, writes the explicit dimension and every dense literal index, clears the dictionary and reverses the output. All scratch stacks and finite control reset in the exact haltList configuration. Its direct bound is eighty times (input length plus one) squared. The returned word has length at most the square of input length plus eight times input length plus seven.

The returned source decodes to the total prepared explicit-universe formula and every clause has at most three literals. An assignment equivalence through the actual deduplicated dictionary preserves ordinary CNF evaluation and the number of satisfying assignments. Rejection returns the valid zero-variable one-empty-clause source 0011000. That same word can also arise from a valid empty-clause source; output equality does not characterize rejection. Empty formulas, repeated literals and tautologies are included. No Hamiltonian or oracle occurs in this counting definition.

References

• Truth anchor: D5/S0/Computability/DenseClauseConversion.dense_word_run
• Dependency: D5/S0/Computability/ClauseWordCodec
• Dependency: D5/S0/Computability/DenseClauseExecution