Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Preprint
Data sources: ZENODO
addClaim

Canonical Quotient-State Realization of Bounded-Width Dynamic Programming in Layered Tseytin 3-CNF

Authors: Daghbouche, Karim; Duman, Deniz;

Canonical Quotient-State Realization of Bounded-Width Dynamic Programming in Layered Tseytin 3-CNF

Abstract

This paper studies canonical quotient-state compression in a deterministic residual decision model for a bounded-width layered 3-CNF family arising from standard Tseytin encodings of bounded-fanin layered Boolean circuits. We define an admitted target family F of bounded-width layered Tseytin 3-CNF instances and prove that the fixed gate-by-gate translation from the source family lands inside this family. On this family we study a canonical residual model M whose state identity is given by canonical active-core type, cut index, and a canonically represented suffix summary associated with that cut. For F, we prove: every reachable residual admits an active/future cut with bounded boundary; the unresolved suffix affects continuation only through a Boolean suffix summary on that bounded boundary; the suffix summary at a fixed cut index is determined by the fixed input and the cut position in the admitted layered regime; the suffix-summary sequence is computable in deterministic polynomial time by backward dynamic programming on the layered suffix; the branch-labelled successor on canonical residual states is well defined; and, for fixed W and Δ, the full reachable canonical quotient-state space is linearly bounded in the clause count and therefore polynomially bounded. The result is a structural realization for the admitted bounded-width family. It expresses the standard bounded-interface dynamic-programming semantics as a rigorous quotient-state construction inside a forward residual model, with all state-counting and running-time bounds parameterized by the fixed constants W and Δ. As a corollary, the same conclusion applies to formulas obtained from the fixed gate-by-gate Tseytin translation of bounded-fanin layered Boolean circuits.

Powered by OpenAIRE graph
Found an issue? Give us feedback