English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Tseitin-formulas are systems of parity constraints whose structure isdescribed by a graph. These formulas have been studied extensively in proofcomplexity as hard instances in many proof systems. In this paper, we provethat a class of unsatisfiable Tseitin-formulas of bounded degree has regularresolution refutations of polynomial length if and only if the treewidth of allunderlying graphs $G$ for that class is in $O(\log|V(G)|)$. To do so, we showthat any regular resolution refutation of an unsatisfiable Tseitin-formula withgraph $G$ of bounded degree has length $2^{\Omega(tw(G))}/|V(G)|$, thusessentially matching the known $2^{O(tw(G))}poly(|V(G)|)$ upper bound up. Ourproof first connects the length of regular resolution refutations ofunsatisfiable Tseitin-formulas to the size of representations of\textit{satisfiable} Tseitin-formulas in decomposable negation normal form(DNNF). Then we prove that for every graph $G$ of bounded degree, everyDNNF-representation of every satisfiable Tseitin-formula with graph $G$ musthave size $2^{\Omega(tw(G))}$ which yields our lower bound for regularresolution.

Characterizing Tseitin-formulas with short regular resolution refutations