Paper deep dive

Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas

Dmitry V. Alexandrov

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 98

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%

Last extracted: 8/25/2026, 6:22:38 AM

Summary

This paper presents the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a combinatorial framework for Boolean satisfiability (SAT) that translates 3-CNF formulas into Compact Triplets Structures (CTS) and applies a Simple Vertex Intersection (SVI) filter. The authors prove that for the 'sliding-window' fragment of 3-CNF, SVI non-emptiness is a necessary and sufficient condition for satisfiability, providing polynomial-time bounds. For general 3-CNF, SVI is only a sound filter (non-emptiness is necessary but not sufficient). The paper introduces VFR, an OCaml prototype extracted from the Rocq formalisation, and benchmarks it against standard SAT instances.

Entities (10)

Dmitry V. Alexandrov · person · 99%Rocq · softwaretool · 99%3-CNF · problem-class · 98%Romanov's Triplet Logic · logicframework · 98%OCaml · programming-language · 97%Simple Vertex Intersection · algorithm · 97%Compact Triplets Structure · data-structure · 96%VFR · softwaretool · 95%Sliding-window CNF · problem-class · 94%Z3 · softwaretool · 90%

Relation Signals (7)

Romanov's Triplet Logic → formalisedin → Rocq

confidence 98% · We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant.

VFR → extractedfrom → Rocq

confidence 95% · an extracted OCaml prototype... The Rocq development comprises over 23,000 lines of code

VFR → implements → Romanov's Triplet Logic

confidence 95% · We introduce VFR (Verified Filter for Romanov's triplet logic), an extracted OCaml prototype that implements a verified decision procedure

Romanov's Triplet Logic → uses → Simple Vertex Intersection

confidence 95% · TLS is a combinatorial framework... based on triplet structures and a filter that we call Simple Vertex Intersection (SVI).

Simple Vertex Intersection → appliesto → Compact Triplets Structure

confidence 94% · SVI, which constructs hyperstructures via tier-wise intersection... For two CTS S1 and S2, the Simple Vertex Intersection constructs a hyperstructure

Sliding-window CNF → hasproperty → polynomial_time_decidable

confidence 92% · For the well-formed sliding-window fragment, we prove explicit polynomial-time bounds for the filter stages... SVI non-emptiness is necessary but not sufficient... for aligned structures, we prove a full bi-implication

Dmitry V. Alexandrov → authored → Romanov's Triplet Logic

confidence 90% · One such approach is Romanov’s Triplet Logic (TLS), introduced in “Non-Orthodox Combinatorial Models Based on Discordant Structures” [3]... Dmitry V. Alexandrov

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a combinatorial framework originally motivated by Boolean satisfiability, based on triplet structures and a filter that we call Simple Vertex Intersection (SVI). We formalise the core of TLS, including its translation from 3-CNF, the clearing procedure, and the SVI algorithm. For the well-formed sliding-window fragment, we prove explicit polynomial-time bounds for the filter stages and verify the translation and intersection operations. Our main contribution is a precise correctness boundary: for general formulas, SVI non-emptiness is necessary but not sufficient for satisfiability; for aligned structures, we prove a full bi-implication, extended to systems of structures. We also formalise the grouped-window translation and provide a formal counterexample to its completeness. We introduce VFR (Verified Filter for Romanov's triplet logic), an extracted OCaml prototype that implements a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF, with a Python runtime and Docker packaging. Benchmarks corroborate the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises over 23,000 lines of code, with 424 proved lemmas and no unproved assumptions.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

94,878 characters extracted from source content.

Expand or collapse full text

Formal verification of Romanov’s triplet logic: A verified filter for sliding-window 3-CNF with application to structured formulasORCID: 0000-0002-9759-8787 Dmitry V. Alexandrov1 Address: HSE University Moscow, Russia Email: dvalexandrov@hse.ru Abstract. We present the first mechanised formalisation of Romanov’s Triplet Logic (TLS) in the Rocq proof assistant. TLS is a combinatorial framework originally motivated by Boolean satisfiability, based on triplet structures and a filter that we call Simple Vertex Intersection (SVI). We formalise the core of TLS, including its translation from 3-CNF, the clearing procedure, and the SVI algorithm. For the well-formed sliding-window fragment, we prove explicit polynomial-time bounds for the filter stages and verify the translation and intersection operations. Our main contribution is a precise correctness boundary: for general formulas, SVI non-emptiness is necessary but not sufficient for satisfiability; for aligned structures, we prove a full bi-implication, extended to systems of structures. We also formalise the grouped-window translation and provide a formal counterexample to its completeness. We introduce VFR (Verified Filter for Romanov’s triplet logic), an extracted OCaml prototype that implements a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF, with a Python runtime and Docker packaging. Benchmarks corroborate the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises over 23,000 lines of code, with 424 proved lemmas and no unproved assumptions. keywordsFormal verification, interactive theorem proving, SAT solving, proof assistants, mechanised mathematics, Rocq, triplet logic, polynomial-time bounds, one-sided filter 2000 Mathematics Subject Classification03B70, 68Q60, 03B35 1. Introduction The Boolean satisfiability problem (SAT) is a cornerstone of computational complexity theory, with applications ranging from hardware verification to automated planning [8]. Despite decades of research, no polynomial-time algorithm is known for 3-SAT, and the prevailing conjecture is that ≠ P≠ NP [1, 2]. Nevertheless, numerous alternative approaches have been proposed, each offering new structural insights into the problem. One such approach is Romanov’s Triplet Logic (TLS), introduced in “Non-Orthodox Combinatorial Models Based on Discordant Structures” [3]. TLS encodes a 3-CNF (Conjunctive Normal Form) formula as a Compact Triplets Formula (CTF), transforms it into a Compact Triplets Structure (CTS) containing all triplets not forbidden by the corresponding clause group, and applies Simple Vertex Intersection (SVI), which constructs hyperstructures via tier-wise intersection. Romanov developed this approach with the goal of efficient SAT solving via tier-wise triplet analysis and hyperstructure intersection. Following Romanov’s original terminology, we refer to these tiered combinatorial objects as Compact Triplets Structures. Throughout the paper, the abbreviation CTS always denotes Romanov’s construction, formalised and extended here in the Rocq proof assistant. Romanov’s key insight is a novel geometric decomposition: instead of searching over variable assignments directly, TLS searches over paths through a layered graph of triplet tiers. This perspective is structurally distinct from classical DPLL (Davis–Putnam–Logemann–Loveland) / CDCL (Conflict-Driven Clause Learning) approaches and offers a new combinatorial perspective on constraint satisfaction problems. In this paper we treat TLS as a self-contained mathematical framework and subject it to rigorous formal analysis, using 3-CNF formulas as a motivating source of benchmark instances rather than as the primary object of study. Our contributions. We formalise the core of TLS in the Rocq proof assistant [4] (version 9.1.1), complemented by exhaustive model checking. Our findings are: (1) We formalise CTF, CTS, hyperstructures, and SVI in Rocq, proving basic correctness lemmas about path construction and compatibility (Section 4). (2) We clarify the correctness boundary of TLS: the existence of a joint satisfying set (JSS) implies SVI’s non-emptiness for non-empty structures (JSS ⇒ SVI non-emptiness, proved in Rocq), but the converse does not hold in general (Section 6). We validate the failure of the reverse direction with both Rocq counterexamples and exhaustive Python-based model checking (Section 5). (3) We introduce VFR (Verified Filter for Romanov’s triplet logic), a prototype implementation (Section 7). It uses the verified clause-by-clause pipeline for well-formed sliding-window CNF and falls back to an unverified grouped-window heuristic for general 3-CNF (Section 1.1). (4) We benchmark VFR on random and structured 3-CNF instances (Section 8). On the verified fragment agreement is 100%; on general random instances the filter is ineffective. (5) We prove a new theorem in Rocq establishing that the aligned intersection of two CTS has a non-empty set of full-length paths if and only if a compatible joint satisfying set exists (Theorem 4.3). This provides the formal foundation for the post-check. The equivalence is conceptually straightforward—it is essentially a restatement of the definition of a compatible path in the intersection—but its verified mechanisation yields an extracted, correct-by-construction decision procedure for aligned structures. (6) We extend this bi-implication to systems of k aligned structures (Theorem 4.4), proving that the systemic tier-wise intersection contains a full-length path iff a compatible joint satisfying set exists for the entire system. (7) We formalise the clearing procedure’s termination using a tight measure (cts_sizects\_size) and prove a semantic fixed-point characterisation: every surviving triplet has compatible neighbours in adjacent tiers (Section 4). (8) We identify a semantic gap between the weak formula-level predicate satisfies_ctfsatisfies\_ctf (which checks each 3-bit window independently) and structure-level path existence (build_paths_all requires globally compatible consecutive triplets). We formalise this in Theorem 4.7: there exist CTFs that admit locally consistent assignments under satisfies_ctfsatisfies\_ctf yet yield no compatible path after clearing (Section 6). This motivates the aligned-intersection approach, for which we recover completeness. Implications. Our work sharpens the understanding of TLS. SVI is not a complete decision procedure. However, when SVI reports emptiness, the formula is guaranteed unsatisfiable—a property we prove formally. Furthermore, TLS offers a novel combinatorial visualisation of SAT instances through tiered triplet structures. This geometric perspective may aid in educational contexts and in analysing formula structure before invoking expensive CDCL solvers. Why this matters for automated reasoning. The paper’s primary audience is the formal-verification and automated-reasoning community rather than the SAT-competition community. Our goal is not to outperform CDCL on benchmark suites—a task for which decades of engineering have produced highly optimised, unverified solvers—but to demonstrate that a non-classical combinatorial framework can be fully mechanised, its correctness boundary exactly determined, and its polynomial fragments certified with concrete complexity bounds. Such mechanised reconstructions are valuable because they (i) expose hidden assumptions that informal descriptions miss, (i) produce certified building blocks that compose into larger verified systems, and (i) provide rigorous foundations for teaching and further research. More concretely, TLS offers three affordances that complement verified CDCL solvers. As an intermediate representation, triplet tiers make variable-interaction structure explicit: a formula analyst can inspect which triplets survive clearing and immediately see local inconsistencies that would be buried in a flat clause list. As a preprocessor, the verified SVI filter can be placed in front of any solver; when it reports UNSAT the answer is proof-carrying, and when it is inconclusive the solver falls back to standard search with no loss. As a certification target, the geometric path-building algorithm yields a concrete witness—a sequence of compatible triplets—that is easier to audit than a DRAT (Delete-Resolution-Asymmetric-Tautology) trace. These properties do not make TLS faster than CDCL, but they make it structurally transparent, and the polynomial bounds are machine-checked rather than merely claimed. Structure of the paper. Section 2 introduces CTF, CTS, and SVI. Section 4 describes our Rocq formalisation and proves the forward direction. Section 5 reports empirical validation results that show the reverse direction fails; the boundary is detailed in Section 6. Section 7 presents VFR, validated experimentally in Section 8. Section 9 discusses residual benefits, related work, limitations, and future directions. Section 10 concludes. 1.1. Scope and limitations To avoid misunderstanding, we state the scope of the formalisation explicitly. Table 1 summarises every component of the pipeline, marking each as formally verified, trusted, or heuristic. Verified in Rocq: CTF, CTS, clearing, aligned intersection, and the clause-by-clause CNF-to-CTF translation in which every clause becomes its own tier. For this fragment theorems about path existence, SVI soundness, and polynomial-time bounds are mechanically proved. Not verified: the grouped-window decomposition that merges multiple clauses sharing the same variable triple into a single tier; the dense sliding-window, overlapping-group, and mixed-overlap benchmarks; and the general 3-CNF heuristic pipeline. These are empirical illustrations of an unverified heuristic, not formal results. See Section 3 for the heuristic pipeline and Section 8 for the benchmarks. Table 1. Trust boundary: verified components, trusted base, and heuristics. “Extr.” indicates whether the component is extracted to executable OCaml code. Component Status Reference / Caveat Extr. CTF, CTS, clearing definitions Verified Rocq 9.1.1, no admitted proofs No SVI soundness (forward) Verified Theorem 4.1 No Aligned intersection (bi-impl.) Verified Theorem 4.3 No Systemic aligned (k structs) Verified Theorem 4.4 No Polynomial complexity Verified O⁡(n4)O(n^4) clearing (generic), O⁡(n2)O(n^2) clearing (single-forbidden) and SVI; n = CTS size (tiers+triplets). Full solver includes exponential post-check No CNF→ (clause-by-clause) Verified Sliding-window CNF only Yes Strong CTF predicate Verified GapClosure.v No Swansea RUP (Reverse Unit Propagation) checker Trusted base Rocq-extracted elsewhere Yes OCaml extraction Trusted base Rocq → OCaml compiler N/A Z3 SAT solver Trusted external UNSAT proofs checked by Swansea N/A Grouped-window decomposition Heuristic Forward soundness only; completeness open No Dense / overlap / mixed pipelines Heuristic Empirical evaluation only No General 3-CNF (Z3 fallback) Heuristic Unverified decomposition No 2. Background: Romanov’s triplet logic Verified core (mechanised in Rocq). For well-formed sliding-window CNF, the clause-by-clause translation, clearing, aligned intersection, and SVI filter are formally proved correct (Table 1). Heuristic shell (unverified). Grouped-window decomposition, greedy permutation search, overlapping-group handling, post-check backtracking, and the general 3-CNF pipeline are empirical heuristics with no formal guarantee. 2.1. Compact Triplets Formula (CTF) A 3-CNF formula over n Boolean variables x1,…,xnx_1,…,x_n is a conjunction of clauses, each a disjunction of exactly three literals. In TLS, a clause is represented as a triplet (v1,v2,v3)∈0,13(v_1,v_2,v_3)∈\0,1\^3 relative to an ordered triple of variable indices (i,j,k)(i,j,k). A Compact Triplets Formula (CTF) is a collection of such triplets grouped by their variable indices into tiers. Definition 2.1 (Tier). A tier over variable indices (i,j,k)(i,j,k) is a set of triplets t⊆0,13t \0,1\^3. A CTF is a list of tiers. The pipeline translates each 3-literal clause into a forbidden triplet (negation pattern), builds a CTF tier per clause, and then forms the raw CTS by tier-wise complementation. The clearing procedure (Listing 1) is applied last to remove incompatible triplets. 2.2. Compact Triplets Structure (CTS) Given a CTF F, the Compact Triplets Structure S=CTS⁡(F)S=CTS(F) is obtained by replacing each tier t of F with its complement: Si=0,13∖Fi.S_i=\0,1\^3 F_i. (1) Intuitively, S contains all triplets that are not forbidden by the corresponding clause group. Definition 2.2 (Compatibility). Two triplets a=(a1,a2,a3)a=(a_1,a_2,a_3) and b=(b1,b2,b3)b=(b_1,b_2,b_3) are compatible if their overlapping positions agree: a2=b1anda3=b2.a_2=b_1 a_3=b_2. (2) Lemma 2.1 (Compatibility Degree). For every triplet t∈0,13t∈\0,1\^3 there are exactly two triplets t′t with compatible⁡(t,t′)=compatible(t,t )= true (forward) and exactly two with compatible⁡(t′,t)=compatible(t ,t)= true (backward). Consequently, the clearing procedure cannot remove a triplet because it has “too many” neighbours; rather, it removes triplets whose two potential partners have already been eliminated. For a fixed triplet t=(0,1,1)t=(0,1,1), exactly two triplets are compatible in the forward direction and exactly two in the reverse direction (Figure 1). 011110111001101forward (2)reverse (2)Path:101010101x0=1x_0=1x1=0x_1=0x2=1x_2=1x3=0x_3=0x4=1x_4=1(x0,x1,x2)(x_0,x_1,x_2)(x1,x2,x3)(x_1,x_2,x_3)(x2,x3,x4)(x_2,x_3,x_4) Figure 1. Top: the compatible-degree property for triplet t=(0,1,1)t=(0,1,1). Exactly two triplets are compatible in each direction (2-regular relation). Bottom: a valid path 101→010→101101→ 010→ 101 through three tiers, inducing the assignment x0=1,x1=0,x2=1,x3=0,x4=1x_0=1,x_1=0,x_2=1,x_3=0,x_4=1. Overlapping positions enforce consistency across adjacent triplets. The path is drawn in assignment order (increasing tier indices); build_paths_all stores paths in reverse order, prepending each new triplet ahead of the current head (Listing 2). A path through a CTS S=[t1,…,tm]S=[t_1,…,t_m] is a sequence of triplets p=[c1,…,cm]p=[c_1,…,c_m] such that ci∈tic_i∈ t_i and adjacent triplets are compatible. Each full-length path induces a variable assignment by flattening the triplets: if p=[(a1,b1,c1),(a2,b2,c2),…]p=[(a_1,b_1,c_1),(a_2,b_2,c_2),…], the corresponding satisfying set is the list =[a1;b1;c1;a2;b2;c2;…]s=[a_1;b_1;c_1;a_2;b_2;c_2;…]. A list s satisfies a CTS S if every consecutive triple (⁡[3i],⁡[3i+1],⁡[3i+2])(s[3i],s[3i+1],s[3i+2]) belongs to tier i. A joint satisfying set (JSS) of two structures S1,S2S_1,S_2 is a single list s that satisfies both simultaneously. Figure 2 summarises the abstraction stack. The construction pipeline transforms a 3-CNF formula (bottom) into a concrete assignment (top) through a sequence of representation changes; the dashed arrow shows the verified feedback loop. Input: 3-CNF formula (clauses over x0…xn−1x_0… x_n-1) Level 0: CTF — forbidden triplets (clause ↦ negation) Level 1: Raw CTS — allowed triplets (complement of CTF) Level 2: Cleared CTS — two-way adjoinable (SVI / EP filter) Level 3: Path — compatible sequence (a2=b1,a3=b2a_2=b_1,\;a_3=b_2) Output: Assignment — variable values (flattened path) cnf_to_ctfcomplementclear_structurebuild_paths_allss_to_assignmenteval_cnf Figure 2. Levels of abstraction in VFR. Each layer transforms the representation toward a concrete variable assignment; the dashed arrow shows the verified feedback loop (OCaml-extracted eval_cnf). Each tier contains triplets over a sliding window of three variables; adjacent tiers overlap by two variables, ensuring that compatibility propagates constraints forward. 2.3. Simple Vertex Intersection (SVI) For two CTS S1S_1 and S2S_2, the Simple Vertex Intersection constructs a hyperstructure H=SVI⁡(S1,S2)H=SVI(S_1,S_2) as follows: (1) Build basic graphs G1G_1 and G2G_2 where vertices are triplets annotated with their tier index. (2) Compute the set of common vertices: triplets that appear in G1G_1 and whose triplet value appears somewhere in G2G_2 (not necessarily at the same tier index). (3) Return the hyperstructure containing these common vertices. In Romanov’s framework, H is non-empty if and only if S1S_1 and S2S_2 share a joint satisfying set—an assignment that satisfies both structures tier-by-tier (a claim we refute in Section 6). The definition extends naturally to k≥2k≥ 2 structures. The Systemic Simple Vertex Intersection (SSVISSVI) computes common vertices across all pairs of structures in a family =S1,…,SkS=\S_1,…,S_k\, producing a hyperstructure system HSS. Non-emptiness of HSS implies that every pair of structures in S shares a common triplet, which is the analogue of Theorem 4.1 for multiple structures (Theorem 4.2 below). From CNF to CTS. The concrete construction algorithms—grouping clauses by variable sets, building complement tiers, and clearing—are described in Section 3. Only the clause-by-clause pipeline is formally verified (Table 1). 3. Heuristic Pipeline Caveat. The pipeline described below—grouping clauses by variable sets and constructing CTS tiers via complementation—is the one used in the VFR prototype. It is not formally verified in Rocq; only the simplified clause-by-clause pipeline of Section 3.1 (for well-formed sliding-window CNF) is mechanised. The following description serves as operational documentation and motivation for the verified fragment. We now describe the concrete algorithms for constructing CTS from a 3-CNF formula. The pipeline consists of three phases: decomposition, tier construction, and clearing. Step 1: Decomposition. Given a 3-CNF formula ϕφ with n variables and m clauses, group the clauses by their sets of variable indices. For each group g with variables i,j,k\i,j,k\ and |g||g| clauses: (1) Create a permutation π=[i,j,k,…]π=[i,j,k,…] where the first three positions are the group’s variables and the remaining n−3n-3 positions are the other variables in some fixed order. (2) For each clause C=(ℓi∨ℓj∨ℓk)C=( _i _j _k) in the group, encode it as a triplet (v1,v2,v3)(v_1,v_2,v_3) where vp=1v_p=1 if the p-th literal is negated and vp=0v_p=0 otherwise. (3) Collect all triplets into a CTF FgF_g annotated with variable indices (i,j,k)(i,j,k). The result is a list of CTFs [F1,…,Fk][F_1,…,F_k] where k≤mk≤ m. 11 1 The formalisation in FormulaTranslation.v translates each clause to a distinct tier for well-formed sliding-window CNF. The grouped-window pipeline is an unverified heuristic for general 3-CNF (Table 1). Step 2: Tier Construction. For each CTF F with tiers grouped by variable indices (i,j,k)(i,j,k): (1) For each tier t containing forbidden triplets T⊆0,13T \0,1\^3, construct the complement tier t′=0,13∖Tt =\0,1\^3 T. (2) Assemble the tiers into a raw CTS SrawS_raw. Step 3: Clearing Procedure. The raw CTS may contain incompatible triplets that cannot participate in any full-length path. The clearing procedure removes them iteratively (Listing 1): Listing 1: Clearing Procedure (pseudocode) ⬇ 1 function ClearSingleTier(tier_idx, all_tiers): 2 current := all_tiers[tier_idx] 3 prev := all_tiers[tier_idx-1] if tier_idx > 0 else AllTriplets 4 next := all_tiers[tier_idx+1] if tier_idx+1 < |all_tiers| else AllTriplets 5 return t in current | exists p in prev : Compatible(t,p) 6 and exists n in next : Compatible(t,n) 7 8 function ClearStructurePass(S): 9 return [ ClearSingleTier(i, S) for i = 0 .. |S|-1 ] 10 11 function ClearStructure(S): 12 repeat cts_size(S) times: 13 S := ClearStructurePass(S) 14 return S Here AllTriplets denotes the set of all 23=82^3=8 possible triplet values; it is used as a boundary condition so that end tiers do not need special-casing. The iteration bound cts_size(S)=∑i|Ti|cts\_size(S)= _i|T_i| is the total number of triplets; it suffices because each pass either removes at least one triplet or leaves the structure unchanged (Theorem 4.9). This is a fixed-point computation: in each pass, a new tier is built containing only triplets that have at least one compatible neighbour in each adjacent tier (or lie at a boundary). The process repeats until no more triplets are eliminated. The resulting structure is the cleared CTS. Note that the implementation builds a fresh list ([t for t in current if ...]) using a functional list comprehension rather than in-place mutation. Example. Consider the formula over 3 variables: ϕ=(x1∨x2∨x3)∧(¬x1∨x2∨¬x3)∧(x1∨¬x2∨x3).φ=(x_1 x_2 x_3) ( x_1 x_2 x_3) (x_1 x_2 x_3). All clauses share variables 1,2,3\1,2,3\, so decomposition yields a single CTF with one tier and forbidden triplets: T=(0,0,0),(1,0,1),(0,1,0).T=\(0,0,0),\;(1,0,1),\;(0,1,0)\. The complement tier contains the remaining 5 triplets: t′=(0,0,1),(0,1,1),(1,0,0),(1,1,0),(1,1,1).t =\(0,0,1),\;(0,1,1),\;(1,0,0),\;(1,1,0),\;(1,1,1)\. Since there is only one tier, the clearing procedure does nothing. The final CTS consists of this single tier. Listing 2: Path-Building Algorithm (pseudocode) ⬇ 1 function ExtendPaths(partial_paths, tier): 2 if partial_paths is empty: 3 return [ [t] for t in tier ] 4 result := [] 5 for path in partial_paths: 6 for t in tier: 7 if Compatible(t, head(path)): 8 result.append( [t] + path ) 9 return result 10 11 function BuildPathsAll(cts): 12 paths := [] 13 for tier in cts: 14 paths := ExtendPaths(paths, tier) 15 return [ p for p in paths if len(p) == len(cts) ] Definition 3.1 (Sliding-Window CNF). A 3-CNF formula ϕφ with n variables is a well-formed sliding-window CNF if its clauses can be ordered so that the i-th clause contains exactly the variables (xi,xi+1,xi+2)(x_i,x_i+1,x_i+2) for i=0,…,n−3i=0,…,n-3. Multiple clauses may share the same window. Remark 3.1 (Tractability of the verified fragment). Well-formed sliding-window CNF has primal graph pathwidth ≤2≤ 2: each clause covers three consecutive vertices of a path, so the primal graph is a subgraph of the square of a path. SAT for graphs of bounded pathwidth is a classic tractable case: dynamic programming on a path decomposition solves it in linear time. Consequently, the verified polynomial bounds for clearing and SVI do not expand the class of polynomially solvable 3-SAT instances; they merely reconstruct the same pathwidth-≤2≤ 2 fragment within Romanov’s framework, but with a formally certified algorithm. The value lies in the mechanisation—certifying that Romanov’s triplet constructions yield a correct decision procedure for this fragment—not in a new complexity improvement. 3.1. Why General 3-CNF Falls Outside the Verified Fragment The decomposition described above preserves satisfiability only when the input formula is already a well-formed sliding-window CNF (Definition 3.1), i.e., every clause uses three consecutive variables. For an arbitrary 3-CNF formula containing clauses such as (x1∨x5∨x9)(x_1 x_5 x_9), typically no variable ordering can place those three variables in consecutive positions while simultaneously satisfying the same requirement for all other clauses. Formally, the question “does there exist a permutation of variables that makes this 3-CNF sliding-window?” is the consecutive-ones property of the clause–variable incidence matrix: columns correspond to variables, and each clause-row must have its three ones in consecutive positions. This property is decidable in polynomial time by the classical PQ-tree algorithm of Booth and Lueker [16]. The primal graph of a sliding-window formula is an interval graph of clique number at most three (and hence of pathwidth at most two), and bounded pathwidth is decidable in linear time for every fixed width. The limitation is therefore structural rather than algorithmic: the sliding-window class is narrow, and a generic 3-CNF formula admits no valid ordering. Moreover, a polynomial-time transformation of an arbitrary 3-CNF into an equisatisfiable sliding-window CNF would imply P==NP, since the fragment itself is solvable in polynomial time by dynamic programming on its bounded-pathwidth primal graph. This justifies our restriction: our Rocq theorems apply to sliding-window CNF formulas; general decomposition falls outside the verified fragment (Table 1). Permutation search. Although the existence of a valid ordering is decidable in polynomial time (see above), our verified implementation is an exhaustive permutation search (file Permutation.v) that guarantees to find a variable ordering making the formula sliding-window whenever one exists. The Rocq formalisation defines permute_cnf (apply a variable permutation) and a sliding-window predicate (checked via is_sliding_cnf_bool), together with a length-preservation lemma. The verified algorithm exhaustive_sliding_window_permutation enumerates all n!n! permutations and returns the first valid one; we prove both soundness (any returned permutation is correct) and completeness (if a sliding-window ordering exists, it is found). Because of factorial complexity the search is practical only for n≤8n≤ 8 (8!=40 3208!=40\,320). For larger instances the Python solver falls back to an unverified heuristic backtracking search (module permutation_heuristic.py) or delegates directly to the external CDCL pipeline. Permutations are proved to preserve satisfiability (permute_cnf_preserves_sat); a verified polynomial-time recognition algorithm (replacing the exhaustive search) is left to future work. When a permutation is found, the solver follows the verified clause-by-clause pipeline on the permuted formula; when it fails, the fallback path verified by external proof checking (Z3 + Swansea RUP checker) takes over. This yields a “heuristic fallback” path: for small structured instances the entire pipeline is formally guaranteed, while for large random instances the trust boundary reduces to the external proof checker. 4. Formalisation in Rocq We formalised the core data structures and algorithms of TLS in Rocq 9.1.1. The development spans seventeen Rocq files covering triplets, tiers, compatibility, CTF-to-CTS construction, clearing, path building, SVI and systemic alignment, formula translation and equivalence, formal counterexamples, grouped sliding-window CNF, variable relabelling, overlapping groups, gap closure, heuristic decomposition, exhaustive permutation search, and OCaml extraction. 4.1. Key Definitions A triplet is a triple of Booleans. A tier is a list of triplets. A CTS is a list of tiers. A satisfying set s is a flattened path: if the underlying path of triplets is [(a1,b1,c1),(a2,b2,c2),…][(a_1,b_1,c_1),(a_2,b_2,c_2),…], then s == [a1;b1;c1;a2;b2;c2;…][a_1;b_1;c_1;a_2;b_2;c_2;…]. The function extract_triplet_local(,i)extract\_triplet\_local(s,i) retrieves the i-th triplet as (⁡[3i],⁡[3i+1],⁡[3i+2])(s[3i],s[3i+1],s[3i+2]) (or None if the list is too short). Consequently, for a satisfying set produced by s_from_path_flats\_from\_path\_flat, extract_triplet_local(,i)extract\_triplet\_local(s,i) yields the sliding-window triplet over variables (xi,xi+1,xi+2)(x_i,x_i+1,x_i+2) (the flattening enforces bi=ai+1b_i=a_i+1 and ci=bi+1c_i=b_i+1, so the logical window slides by one variable even though the list indices advance by three). The constructor s_from_path_flats\_from\_path\_flat flattens a path of triplets [(a1,b1,c1),(a2,b2,c2),…][(a_1,b_1,c_1),(a_2,b_2,c_2),…] into [a1;b1;c1;a2;b2;c2;…][a_1;b_1;c_1;a_2;b_2;c_2;…], so consecutive triplets share the overlapping variables b1=a2b_1=a_2 and c1=b2c_1=b_2 required by compatiblecompatible. Definition 4.1 (Satisfying Set). Let S=[T0,T1,…,Tm−1]S=[T_0,T_1,…,T_m-1] be a CTS and let =[v0,v1,…]s=[v_0,v_1,…] be a list of Boolean values. For each tier index i, let tripi()=(⁡[3i],⁡[3i+1],⁡[3i+2])trip_i(s)=(s[3i],s[3i+1],s[3i+2]) (or undefined if the list is too short). Then s satisfies S, written is_satisfying_set(S,)is\_satisfying\_set(S,s), iff for every i<mi<m the triplet tripi()trip_i(s) is defined and belongs to TiT_i. Definition 4.2 (Joint Satisfying Set). A list s is a joint satisfying set of S1S_1 and S2S_2, written JSS⁡(S1,S2,)JSS(S_1,S_2,s), iff it satisfies both structures simultaneously: is_satisfying_set(S1,)∧is_satisfying_set(S2,)is\_satisfying\_set(S_1,s) \_satisfying\_set(S_2,s). An empty structure is vacuously satisfiable; non-emptiness of both structures is enforced as an explicit premise in Theorem 4.1 (S1≠[],S2≠[]S_1≠[],S_2≠[]). 4.2. Design Choices We represent triplets as native triples (bool * bool * bool) and structures as lists rather than vectors or finite types. This choice reflects a trade-off between expressiveness and proof automation: lists provide structural induction principles that Rocq’s auto and lia tactics handle well, while avoiding the proof-engineering overhead of dependent types for fixed-length sequences. A subtle issue arose with the definition of path. Our initial attempt used Definition path := list triplet, which created a type synonym that is convertible but not unifiable with list triplet. This blocked rewrite and subst tactics across the development. Removing the type synonym and using list triplet directly resolved the issue and is a lesson for other mechanisation efforts. 4.3. Proved Lemmas We proved 424 lemmas and theorems across the seventeen files. The development required nested inductions and careful handling of arithmetic side conditions involving nth_error and tier lengths. The most technically demanding was build_paths_aux_contains_expected_path, which required nested induction on the accumulator of build_paths_aux together with delicate arithmetic reasoning about nth_error and tier lengths. Key lemmas include: • Path existence (Lemma 4.3): if a satisfying set exists, build_paths_aux contains a path extending any suffix with triplets drawn from the set. • Forward direction (Theorem 4.1): existence of a joint satisfying set implies non-emptiness of SVI. • Aligned intersection equivalence (Theorem 4.3): for structures of equal length, the aligned intersection has a full-length path iff a compatible joint satisfying set exists. • Systemic aligned completeness (Theorem 4.4): for a system of k aligned structures, the systemic tier-wise intersection has a full-length path iff a compatible joint satisfying set exists for the entire system. • CTF-to-CTS soundness (Lemma 4.5): every path produced by build_paths_all on ctf_to_cts yields a satisfying assignment for both the original formula and the cleared structure. • Clearing fixed-point characterisation (Theorem 4.10): after clearing, every remaining triplet has compatible neighbours in both adjacent tiers (or lies at a boundary). • Raw construction completeness (Lemma 4.7): if a satisfying set is compatible with the raw (non-cleared) CTS, then build_paths_all on that raw CTS is non-empty. • Cleared CTF strong completeness (Lemma 4.8): for a non-empty cleared CTF, compatibility-aware satisfiability implies non-emptiness of build_paths_all. This closes the loop between the strong predicate and path existence for the cleared structure. • Semantic gap between weak satisfiability and path existence (Theorem 4.7): there exist CTFs that admit locally consistent assignments under satisfies_ctfsatisfies\_ctf yet yield no compatible path after clearing. This shows that the weak predicate does not guarantee global path existence; completeness is recovered only at the level of aligned intersection (Theorem 4.3). • CNF-to-CTF satisfiability equivalence (Theorem 4.5): for well-formed sliding-window CNF formulas, satisfiability in standard CNF semantics is equivalent to satisfiability of the translated CTF. The formalisation uses a simplified clause-by-clause pipeline: each clause becomes a separate CTF tier containing exactly one forbidden triplet (its negation pattern). The proof constructs a greedy assignment sat_assignment_aux that satisfies each clause independently. Because the translation is one-to-one, consecutive tiers necessarily share overlapping variables, and the satisfying set s_from_path_flats\_from\_path\_flat enforces global consistency. This is not the grouped-window pipeline of Section 3; it is an equivalent simplified view used for formal verification. • Path existence equivalence (Lemma 4.4): a compatible satisfying set exists for a non-empty structure iff build_paths_all contains at least one path. • Raw construction emptiness (Lemma 4.6): a tier of build_cts_from_ctf is empty iff the corresponding formula tier contains all 8 triplets(per-tier complementation). • Compatible degree (Lemma 2.1): for any triplet, exactly 2 triplets are compatible in the forward direction and exactly 2 in the reverse direction. Theorem 4.1 (Forward Direction of SVI). Let S1,S2S_1,S_2 be non-empty CTS. If there exists a joint satisfying set s for S1S_1 and S2S_2 (in the weak, index-flexible sense), then the Simple Vertex Intersection is non-empty: ∃.JSS⁡(S1,S2,)⟹SVI⁡(S1,S2)≠∅. \;.\;JSS(S_1,S_2,s)\; \;SVI(S_1,S_2)≠ . Proof sketch. Every triplet tit_i of s appears in some tier of both S1S_1 and S2S_2. SVI computes common vertices by value, so at least t0t_0 is a common vertex. Hence the hyperstructure contains t0t_0 and is non-empty. ∎ Theorem 4.2 (Systemic Forward Direction). Let =[S1,…,Sk]S=[S_1,…,S_k] be a system of non-empty CTS. If there exists a joint satisfying set for all structures in S, then the systemic SVI produces a non-empty hyperstructure system: ∃.∀i≤k.is_satisfying_set(Si,)⟹SSVI⁡()≠∅. \;.\;∀ i≤ k\;.\;is\_satisfying\_set(S_i,s)\; \;SSVI(S)≠ . Proof sketch. SSVI applies the pairwise SVI to every pair (S1,Si)(S_1,S_i) with i>1i>1. By Theorem 4.1 each pairwise SVI is non-empty because s satisfies both structures. Therefore every hyperstructure in the system is non-empty. ∎ Theorem 4.3 (Aligned Intersection Equivalence). For all S1,S2S_1,S_2 with |S1|=|S2||S_1|=|S_2|, if both are non-empty, then ∃ JSScompat(S1,S2)⟺build_paths_all(cts_intersection_raw(S1,S2))≠[].∃ JSS_compat(S_1,S_2)\; \;build\_paths\_all(cts\_intersection\_raw(S_1,S_2))≠[]. Although the statement is intuitively clear—a compatible path through the tier-wise intersection exists precisely when a sequence of triplets is compatible across both structures—it is exactly the kind of “obvious” fact that often breaks during mechanisation. The value of the formal proof is that it certifies consistency among three independently defined concepts (the compatibility-aware satisfying set, the aligned intersection operation, and the inductive path-building algorithm) and establishes that the right-hand side is computable and has been extracted to OCaml (Section 7). Reconciling the recursive definitions of is_satisfying_set_compatis\_satisfying\_set\_compat and build_paths_all is a non-trivial engineering task: subtle mismatches in base cases or accumulator shapes that a human reader overlooks become hard proof obligations in Rocq. Lemma 4.1 (Path Extension). Let R be a suffix of a CTS, s a compatible satisfying set, and acc a set of partial paths. If every path in acc can be extended by triplets drawn from s, then build_paths_aux(R,)build\_paths\_aux(R,acc) contains at least one full-length extension whose prefix consists exactly of the triplets prescribed by s. Corollary 4.1 (Aligned Intersection Equivalence). For all S1,S2S_1,S_2 with |S1|=|S2||S_1|=|S_2|, let I=cts_intersection_raw(S1,S2)I=cts\_intersection\_raw(S_1,S_2). Then ∃.JSScompat(S1,S2,)⟺build_paths_all(I)≠[]. \;.\;JSS_compat(S_1,S_2,s)\; \;build\_paths\_all(I)≠[]. Theorem 4.4 (Systemic Aligned Completeness). Let =[S1,S2,…,Sk]S=[S_1,S_2,…,S_k] be a system of aligned CTS ((all of equal length)). Define the systemic raw intersection Ik=cts_intersection_raw_k()I_k=cts\_intersection\_raw\_k(S). Then ∃.∀i≤k.is_satisfying_set_compat(Si,)⟺build_paths_all(Ik)≠[]. \;.\;∀ i≤ k\;.\;is\_satisfying\_set\_compat(S_i,s)\; \;build\_paths\_all(I_k)≠[]. Proof sketch. The proof proceeds by induction on the system size, using the pairwise aligned-intersection lemmas as the base case. For the forward direction, if a common satisfying set s exists, it satisfies every pairwise intersection, hence the systemic intersection, and therefore build_paths_all(Ik)≠[]build\_paths\_all(I_k)≠[]. For the reverse direction, any path through IkI_k yields a sequence =s_from_path(π)s=s\_from\_path(π) that belongs to every tier of every structure; by the splitting lemma this s satisfies each SiS_i compatibly. ∎ Lemma 4.2 (Raw Intersection Non-Empty). For non-empty aligned structures of equal length, cts_intersection_rawcts\_intersection\_raw is never empty. Proof sketch (Aligned Intersection). The non-emptiness premise is redundant: for non-empty aligned structures, cts_intersection_rawcts\_intersection\_raw is never empty (Lemma 4.2). (⇒ ) Given a compatible satisfying set s, we construct a path through the intersection by induction on the tier index. At each step, the compatibility of adjacent triplets in s guarantees that the corresponding triplet exists in the intersection tier and is compatible with the previous one. By Lemma 4.3 (proved by nested induction on the recursive structure), this path is present in build_paths_allbuild\_paths\_all. (⇐ ) Given a full-length path p in the intersection, every triplet ci∈pc_i∈ p belongs to tier i of both S1S_1 and S2S_2. The compatibility of adjacent triplets in p ensures that s_from_paths\_from\_path produces a satisfying set compatible with both structures. Lemma 4.3 (Path Existence from Satisfying Set). Let S be a non-empty CTS and s a satisfying set for S. Then build_paths_auxbuild\_paths\_aux contains a path extending any suffix with triplets drawn from s. Lemma 4.4 (Structural Characterisation). For any non-empty CTS S: build_paths_all(S)=[]⟺¬∃.is_satisfying_set_compat(S,).build\_paths\_all(S)=[]\; \; \, \;.\;is\_satisfying\_set\_compat(S,s). Equivalently, build_paths_all(S)≠[]build\_paths\_all(S)≠[] iff there exists at least one compatible satisfying set (hence at least one full-length path). This equivalence closes the loop between the semantic notion of satisfying set and the algorithmic notion of path existence for a single structure. Theorem 4.3 lifts the same equivalence to aligned intersections of pairs. 4.4. Translation Correctness The verified pipeline relies on two correctness bridges between the classical CNF world and the triplet world. Lemma 4.5 (Soundness of CTF-to-CTS Translation). For every formula ϕφ and every path p∈build_paths_all(ctf_to_cts(ϕ))p \_paths\_all(ctf\_to\_cts(φ)), the flattened assignment s_from_path(rev⁡(p))s\_from\_path(rev(p)) both satisfies ϕφ (in the formula-level sense) and is a compatible satisfying set for the cleared structure. Theorem 4.5 (CNF-to-CTF Equivalence). For well-formed sliding-window CNF formulas, satisfiability in standard CNF semantics is equivalent to satisfiability of the translated CTF. Lemma 4.5 bridges formula-level satisfiability and structure-level compatibility: any path produced by build_paths_allbuild\_paths\_all on the translated CTS yields a satisfying assignment for the original formula. Theorem 4.5 certifies that the entire translation pipeline (CNF→ → → ) is semantically faithful for the verified fragment. Lemma 4.6 (Per-Tier Complementation). A tier of the raw CTS is empty iff the corresponding formula tier contains all 8 triplets (i.e., the forbidden set covers the entire space). This per-tier complementation is the mechanism behind the counterexample of Section 6 (combined with arc-consistency filtering in clearing). Lemma 4.7 (Raw Construction Completeness). For any non-empty formula ϕφ, if s is a compatible satisfying set of the raw CTS build_cts_from_ctf(ϕ)build\_cts\_from\_ctf(φ), then build_paths_allbuild\_paths\_all on that raw CTS is non-empty. Thus completeness holds for the raw (non-cleared) construction: any compatible satisfying set guarantees a non-empty path set. The non-emptiness precondition excludes the degenerate case of an empty formula. Lemma 4.8 (Cleared CTF Strong Completeness). For a non-empty cleared CTF, compatibility-aware satisfiabilityimplies non-emptinessofbuild_paths_allbuild\_paths\_all. Theorem 4.6 (Relabelling preserves satisfiability). Let f be a formula in which every clause uses only variables v1,v2,v3\v_1,v_2,v_3\. Then (∃a,eval_cnf(a,f)=)⟺(∃a′,eval_cnf(a′,relabel_cnf(v1,v2,v3,f))=). array[]@l(∃ a,\;eval\_cnf(a,f)= true)\\ (∃ a ,\;eval\_cnf(a ,relabel\_cnf(v_1,v_2,v_3,f))= true). array The forward direction builds a from a′a by placing the three bits a0′,a1′,a2′a _0,a _1,a _2 at positions v1,v2,v3v_1,v_2,v_3. The backward direction projects to the first three positions. Lemma 4.9 (Dense Groups Soundness). For dense sliding-window groups, the forward CTF-level link soundness holds: every assignment that satisfies the grouped CNF yields a satisfying set for the corresponding CTF. 4.5. Counterexamples and Formal Limits The positive results above are complemented by two formal counterexamples that mark the exact boundaries of what the framework can guarantee. Semantic gap. The weak predicate satisfies_ctfsatisfies\_ctf checks each 3-bit window independently and does not enforce agreement on overlapping bits between consecutive windows. Consequently it admits locally consistent assignments that are not globally realisable as compatible paths. Theorem 4.7 (Semantic Gap). There exists a CTF ϕφ and an assignment s such that s satisfies ϕφ in the weak formula-level sense, yet build_paths_all(ctf_to_cts(ϕ))=[]build\_paths\_all(ctf\_to\_cts(φ))=[]. Counterexample. Take a 2-tier CTF where tier 0 forbids all triplets except (0,1,1)(0,1,1) and tier 1 forbids all except (1,0,1)(1,0,1). These two survivors are incompatible (the overlap bits 1≠01≠ 0 do not match), so clearing removes both and yields empty tiers. Yet the assignment =[0,1,1,1,0,1]s=[0,1,1,1,0,1] avoids each tier’s local forbidden set, giving satisfies_ctf(,ϕ)=truesatisfies\_ctf(s,φ)=true. This formally separates weak formula-level satisfiability from structure-level path existence. ∎ Clearing is not conservative. Clearing uses the directed predicate can_adjoincan\_adjoin, which requires a forward-compatible successor, whereas build_paths_allbuild\_paths\_all checks only backward compatibility. Hence a triplet may belong to a valid path yet still be removed. Theorem 4.8 (Clearing removes valid paths). There exists a CTS S and a sequence s such that (1) is_satisfying_set_compat(S,)=is\_satisfying\_set\_compat(S,s)= true, (2) build_paths_all(S)≠∅build\_paths\_all(S)≠ , (3) build_paths_all(clear_structure(S))=∅build\_paths\_all(clear\_structure(S))= . Counterexample. Take a 3-tier CTS S=[(1,0,0),(0,1,0),(0,0,1)]S=[\(1,0,0)\,\;\(0,1,0)\,\;\(0,0,1)\] with the unique compatible path π=[(1,0,0),(0,1,0),(0,0,1)]π=[(1,0,0),(0,1,0),(0,0,1)]. The middle triplet (0,1,0)(0,1,0) has no forward-compatible successor in tier 2 (the only candidate (0,0,1)(0,0,1) is incompatible because the overlapping bit 1≠01≠ 0). Hence clearing removes (0,1,0)(0,1,0), which in turn destroys the only full-length path. Yet π satisfies every tier of S compatibly, so build_paths_all(S)≠∅build\_paths\_all(S)≠ while build_paths_all(clear_structure(S))=∅build\_paths\_all(clear\_structure(S))= . ∎ Remark 4.1 (Why these limits do not invalidate the main results). Clearing is nevertheless sound (it never creates new paths) and monotone in the reverse direction: any path that survives clearing was already present in the original structure (Lemma 4.10). Completeness is recovered by Theorem 4.3, which bypasses clearing entirely and works directly on the aligned intersection. The semantic gap is closed for the verified fragment by the strong predicate satisfies_ctf_strongsatisfies\_ctf\_strong (Section 6). Positive properties of clearing. Despite the negative results above, clearing satisfies two fundamental properties that justify its use as an optimisation. Theorem 4.9 (Clearing Termination). The clearing procedure terminates. The measure cts_size(S)=∑i|Ti|cts\_size(S)= _i|T_i| (the total number of triplets in all tiers) strictly decreases whenever triplets are eliminated and is bounded below by 00, so only finitely many eliminations are possible. Theorem 4.10 (Fixed-Point Characterisation). After clearing, every surviving triplet t in tier i has at least one compatible predecessor in tier i−1i-1 and at least one compatible successor in tier i+1i+1 (except at the boundaries i=0i=0 and i=m−1i=m-1, where only the existing neighbour is required). The termination bound uses cts_size(S)cts\_size(S) rather than the coarse 8⋅|S|8·|S|, yielding a tighter proof. The fixed-point theorem gives a semantic characterisation of the survivors: only triplets with two-way adjoinability remain. Lemma 4.10 (Clearing monotonicity for paths). For any non-empty CTS S and any path π, π∈build_paths_all(clear⁡(S))⟹π∈build_paths_all(S).π \_paths\_all(clear(S))\; \;π \_paths\_all(S). Proof sketch. Construct the satisfying set =s⁡(rev⁡(π))s=s(rev(π)) from the reversed path. Because π is valid in clear⁡(S)clear(S), s is a compatibility-aware satisfying set for clear⁡(S)clear(S). Since clearing only shrinks tiers, every triplet of s in a cleared tier also lies in the original tier. By induction on the tier list, compatibility-awareness transfers from the cleared structure to the original one, and the path-existence theorem yields a path π′π with exactly the same triplets as π. ∎ 4.6. Constructive Solver for Grouped Sliding-Window CNF For grouped sliding-window CNFs with disjoint variable ranges (multiple clauses per consecutive variable window) we formalise in Rocq a recursive, extractable solver solve_grouped_sliding. The solver processes each group independently: it translates the group to a CTF, finds satisfying sets via the verified path-building pipeline, and merges the resulting assignments into a global assignment. If the pipeline yields no valid set for a group, the solver falls back to a verified greedy assignment constructor sat_assignment_aux. Theorem 4.11 (Grouped solver soundness). For every well-formed grouped sliding-window CNF, if solve_grouped_sliding returns an assignment, that assignment satisfies the entire concatenated formula. Theorem 4.12 (Grouped solver completeness). For every well-formed grouped sliding-window CNF, if every group is individually satisfiable, then solve_grouped_sliding returns some assignment. The key ingredient is Lemma eval_cnf_merge_assignments_concat (Structured.v): merging a group assignment into the accumulated result preserves satisfiability of the concatenated formula, even when the current group appears again later in the list. This allows the recursive solver to handle duplicate groups without backtracking. Extraction metrics. The solver is not merely proved correct but extracted to executable OCaml code. Rocq’s Extraction command produces VFR.ml (786 lines, ≈ 21 KiB), which contains the verified implementations of build_paths_all, eval_cnf, ctf_to_cts, and solve_grouped_sliding. A thin JSON bridge (vfr_solver.ml, 261 lines, ≈ 9 KiB) reads CNF formulas from stdin and prints satisfying assignments or UNSAT verdicts. Together they form a standalone verified executable that requires no Rocq runtime. 5. Empirical Validation via Exhaustive Enumeration Before undertaking Rocq proofs of the reverse direction, we used a Python-based model checker to exhaustively enumerate all pairs of CTS structures up to small bounds (787,244 exhaustive cases plus 500 random instances). Four SVI variants were checked; in every case where a reverse implication was claimed, the model checker found a counterexample. All counterexamples share the same pattern: SVI finds a common triplet between tier i of S1S_1 and tier j≠ij≠ i of S2S_2, creating a non-empty hyperstructure despite the absence of a tier-aligned satisfying set. This empirical observation motivated the aligned-intersection construction of Theorem 4.3. 6. The Correctness Boundary: False Positives in SVI 6.1. The Correctness Boundary Romanov’s framework assumes that non-emptiness of SVI is equivalent to the existence of a joint satisfying set. Formally: ∃ JSS(S1,S2)⟺H=SVI⁡(S1,S2)≠∅.∃ JSS(S_1,S_2)\; \;H=SVI(S_1,S_2)≠ . (3) Only the forward direction (⇒ ), i.e. ∃JSS⟹H≠∅, \; \;H≠ , (4) is true and is proved in our Rocq development as Theorem 4.1. The converse (H≠∅⇒∃JSSH≠ ) does not hold in general. 22 2 The definition is_satisfying_setis\_satisfying\_set treats an empty structure as vacuously satisfiable ([]↦True[] ). Non-emptiness of both structures is therefore stated as an explicit premise in Theorem 4.1 (S1≠[],S2≠[]S_1≠[],S_2≠[]) and in Theorem 4.2 (∀S∈system,structure(S)≠[]∀ S ,structure(S)≠[]). The compat version is_satisfying_set_compatis\_satisfying\_set\_compat also uses []↦True[] . Its completeness theorem (Theorem 4.3) carries the premise cts_intersection_raw≠[]cts\_intersection\_raw≠[], but this premise is redundant for non-empty aligned structures: cts_intersection_rawcts\_intersection\_raw is never empty when both inputs are non-empty and aligned (Lemma 4.2). A separate observation concerns the semantic gap between the weak formula-level predicate satisfies_ctfsatisfies\_ctf and structure-level path existence. The predicate satisfies_ctfsatisfies\_ctf checks each 3-bit window independently: it merely verifies that extract_triplet_local(,i)extract\_triplet\_local(s,i) avoids the forbidden triplets of tier i. It does not enforce that consecutive windows agree on their overlapping 2 bits. Consequently, satisfies_ctfsatisfies\_ctf admits locally consistent assignments that are not globally realisable as compatible paths. We formalise this gap in Theorem 4.7: there exists a CTF ϕφ and an assignment s with satisfies_ctf(,ϕ)=truesatisfies\_ctf(s,φ)=true, yet build_paths_all(ctf_to_cts(ϕ))=[]build\_paths\_all(ctf\_to\_cts(φ))=[]. In this counterexample, tier 0 permits only (,,)(false,true,true) and tier 1 permits only (,,)(true,false,true). These two survivors are incompatible (their overlapping bits do not match), so clearing removes both. The CTF is therefore unsatisfiable as a sliding-window formula: the overlapping variable x2x_2 receives conflicting values (true from the first window, false from the second). Yet satisfies_ctfsatisfies\_ctf returns true because it inspects each tier through non-overlapping chunks ⁡[3i .. 3i+2]s[3i\,..\,3i+2]. This does not contradict Lemma 4.5: that lemma states only the soundness direction (every path produced by build_paths_all yields a formula-level satisfying set), which holds for arbitrary CTFs, whereas the counterexample concerns the converse. Moreover, for well-formed sliding-window CNF translated via the clause-by-clause pipeline of FormulaTranslation.v, each clause becomes a tier with exactly one forbidden triplet, and the constructed satisfying set s_from_path_flats\_from\_path\_flat is a flattened assignment where consecutive triplets necessarily agree on overlaps. Hence satisfies_ctfsatisfies\_ctf coincides with true satisfiability for such formulas. The counterexample operates outside this well-formed class (it is a generic CTF with 7 forbidden triplets per tier), exposing the weakness of the generic predicate. It is important to note that clearing is not a conservative transformation with respect to arbitrary paths or strong satisfying sets. The predicate can_adjoincan\_adjoin used during clearing requires two-way adjoinability (both a forward-compatible predecessor and a forward-compatible successor), whereas build_paths_all checks only backward compatibility (compatible next prev). Consequently, a triplet may belong to a valid path yet still be removed by clearing because it lacks a forward-compatible partner in the next tier (Theorem 4.8). The “emptiness” in the counterexample above is a genuine loss of paths, not merely a detection of inconsistency. This directional asymmetry is an intrinsic feature of the current formalisation. It is not a bug: clearing is used only as an optimisation (it is sound—it never creates new paths), while completeness is recovered by Theorem 4.3 via aligned intersection and build_paths_all, which do not rely on clearing preserving all paths. This counterexample rules out the naive hope that running clearing before SVI would yield a complete decision procedure; instead, completeness requires the aligned-intersection construction of Theorem 4.3. At the same time, clearing is monotone in the reverse direction: any full-length path that survives clearing was already present in the original structure (Lemma 4.10). Monotonicity does not contradict non-conservativity: it merely states that clearing never creates new full-length paths, only removes existing ones. The aligned-intersection approach (Theorem 4.3) recovers completeness by operating on the intersection directly, bypassing the need for clearing to preserve paths. 6.2. Why SVI Gives False Positives The Simple Vertex Intersection computes common vertices between G1G_1 and G2G_2 without requiring tier alignment. A triplet from tier i of S1S_1 is considered “common” if its value appears in any tier of S2S_2. False positives arise from two distinct phenomena: (1) Cross-tier matching. A triplet from tier i of S1S_1 matches a triplet from tier j≠ij≠ i of S2S_2. SVI reports them as “common” even though no aligned satisfying set can use them simultaneously. (2) Partial tier match. Some corresponding tiers share triplets, but at least one tier has no common triplet. SVI finds the existing matches and reports non-empty, yet no aligned satisfying set exists because the unmatched tier cannot be satisfied. For example, tier 0 of S1S_1 and tier 1 of S2S_2 share triplet (0,0,0)(0,0,0), so SVI reports non-empty. However, tier 1 of S1S_1 and tier 1 of S2S_2 have no common triplet, so no aligned satisfying set exists. Bidirectional compatibility. Attempts to define forward-compatible satisfying sets and prove that clearing preserves bidirectional compatibility were abandoned after we proved that compatiblecompatible is a directed relation and that path-derived satisfying sets cannot guarantee forward compatibility. This does not affect our main results: Theorem 4.3 establishes equivalence through build_paths_all, which checks only backward compatibility. 6.3. Concrete Counterexamples Cross-tier mismatch. Consider: S1=[(0,0,0),(1,1,1)],S2=[(1,1,1),(0,0,0)].S_1=[\(0,0,0)\,\(1,1,1)\], S_2=[\(1,1,1)\,\(0,0,0)\]. SVI finds two common triplets: (0,0,0)(0,0,0) appears in tier 0 of S1S_1 and tier 1 of S2S_2; (1,1,1)(1,1,1) appears in tier 1 of S1S_1 and tier 0 of S2S_2. Consequently SVI returns a non-empty hyperstructure. Yet no aligned joint satisfying set exists, because tier 0 of S1S_1 and tier 0 of S2S_2 share no triplet, and likewise for tier 1. The structures are mutually “shifted.” Partial tier match. Consider: S1=[(0,0,0),(1,1,1)],S2=[(0,0,0),(0,1,0)].S_1=[\(0,0,0)\,\(1,1,1)\], S_2=[\(0,0,0)\,\(0,1,0)\]. SVI finds the common triplet (0,0,0)(0,0,0) (present in tier 0 of both structures) and returns a non-empty hyperstructure. However, tier 1 of S1S_1 and tier 1 of S2S_2 have no common triplet, so no aligned joint satisfying set exists. The formula is unsatisfiable, but SVI reports non-empty. 7. VFR: A Prototype Solver with Post-Checking Since SVI is not a complete decision procedure, we propose VFR: a prototype solver that uses SVI as a fast, one-sided filter for structured formulas, followed by an exhaustive post-check. (All formal guarantees are summarised in Table 1.) 7.1. Architecture Figure 3 illustrates the VFR solving pipeline. The input 3-CNF formula is first decomposed into CTFs; each CTF is converted to a CTS via complementation and clearing. SVI then acts as a filter whose running time is polynomial in the structure size (see complexity analysis below): if it returns False, the formula is guaranteed unsatisfiable. If SVI returns True, the exponential post-check searches for a globally consistent assignment. Any candidate is finally verified against the original CNF. (Only the SVI filter is formally verified; see Table 1.) 3-CNFDecomposeBuild CTSClearSVI =∅= ?UNSATPost-checkFound?SATUNSATYesNoYesNo Figure 3. The VFR solving pipeline as a flowchart. Only the SVI filter is formally verified for the sliding-window fragment; decomposition and post-check are unverified heuristics for general 3-CNF. (1) Decomposition. The 3-CNF formula is split into CTFs grouped by variable sets. (2) CTS Construction. Each CTF is converted to a CTS via complement and clearing. (3) SVI Filter (polynomial). Run EffectiveProcedure. If it returns False, return UNSAT immediately. This step is guaranteed correct: no false negatives. (4) Post-Check (exponential). If SVI returns True, search for a globally consistent assignment by backtracking over partial assignments from each CTS. If none exists, SVI produced a false positive; return UNSAT. (5) Verification. Any candidate assignment is checked against the original CNF formula. Complexity analysis. Table 2 summarises the complexity of each pipeline stage. Table 2. Verified polynomial complexity bounds (mechanised in Complexity.v and GapClosure.v) Stage Time bound Provenance Decomposition (heuristic) O⁡(m⋅log⁡m)O(m· m) Grouping clauses by variable triples Tier construction O⁡(k)O(k) k tiers, at most 8 triplets each Clearing (generic) ≤100n4+100≤ 100n^4+100 Theorem 7.1 Clearing (single-forbidden) ≤2000n2+2000≤ 2000n^2+2000 Theorem 7.2 SVI filter ≤3n2+7≤ 3n^2+7 Theorem 7.3 Full pipeline ≤200n4+200≤ 200n^4+200 Theorem 7.4 The constants in Table 2 emerge from a formal cost model that counts every cons cell, compatibility check, and list traversal. For generic clearing, each pass costs O⁡(n3)O(n^3) (every triplet is checked against both neighbours, each of size O⁡(n)O(n)) and at most n passes are iterated, yielding 100n4+100100n^4+100 after routine arithmetic induction. The SVI bound 3n2+73n^2+7 comes from summing the quadratic costs of building two basic graphs and intersecting their vertices. For single-forbidden structures clearing is the identity (Corollary 7.1), so only one pass is needed and the bound collapses to 2000n2+20002000n^2+2000. Decomposition groups m clauses by variable sets; sorting yields O⁡(mlog⁡m)O(m m) time. Tier construction builds complement tiers of size at most 8 triplets each, taking O⁡(k)O(k) for k tiers. Clearing is a fixed-point computation: each pass checks every line against all lines of each neighbour, giving O⁡(tj2)O(t_j^2) per tier. The number of passes is bounded by the total number of lines (cts_sizects\_size), giving overall O⁡(cts_size⋅∑jmjtj2)O(cts\_size· _jm_jt_j^2). In the mechanisation we use the exact measure ∑i|tieri| _i|tier_i| instead of the coarse 8⋅|S|8·|S|, which yields a tighter termination proof (Theorem 4.9). SVI filter computes common vertices between all pairs of CTFs. For CTFs with |Vj||V_j| and |Vj′||V_j | vertices, the pairwise intersection is O⁡(|Vj|⋅|Vj′|)O(|V_j|·|V_j |). Summing over all pairs gives O⁡(∑j<j′|Vj|⋅|Vj′|)O( _j<j |V_j|·|V_j |), which is polynomial in the input size. For k CTFs each with O⁡(n)O(n) triplets, this simplifies to O⁡(n2k2)O(n^2k^2). Formal verification. The Rocq development includes a mechanised cost model (file Complexity.v, approximately 1,000 lines) that defines explicit cost functions mirroring the recursive structure of each algorithm. Every cons cell, compatibility check, and list traversal is assigned a unit cost. The bounds in Table 2 are explicit inequalities proved in Rocq by induction on the structure of the input, where n is the combined input size (tiers plus triplets). For the verified clause-by-clause translation each clause becomes one tier, so n=Θ⁡(m)n= (m) where m is the number of clauses; for well-formed sliding-window CNF, m=O⁡(v)m=O(v) with v the number of variables. These polynomial bounds apply only to the filter stages (clearing and SVI). The complete decision procedure includes the aligned-intersection post-check, which is exponential in the worst case (O⁡(8m)O(8^m) path enumeration). These are not merely asymptotic statements; they are explicit inequalities proved in Rocq by induction on the structure of the input, with arithmetic appeals to nia. Full definitions and intermediate lemmas (e.g., single-tier and single-pass bounds) are formalised in files Complexity.v and GapClosure.v. Aligned intersection (used in the post-check) builds cts_intersection_rawcts\_intersection\_raw tier-by-tier, then calls build_paths_all. The intersection construction is linear in tier size; path enumeration is the dominant cost: a CTS with m tiers and at most 8 triplets per tier has at most 8m8^m full-length paths in the worst case (all triplets mutually compatible). Hence build_paths_all is O⁡(8m)O(8^m) time and space. Post-check backtracks over k CTFs. If the j-th CTF has pjp_j paths, the search explores the product space in O⁡(∏j=1kpj)O( _j=1^kp_j) time. Since pj≤8mjp_j≤ 8^m_j, the worst-case matches aligned intersection. The recursion depth is k and each partial assignment stores n variables, giving O⁡(n⋅k)O(n· k) space. This exponential worst case is unavoidable unless = P= NP, but structured instances with tight constraints (small tijt_ij after clearing) can be solved efficiently in practice. 7.2. Derivation of Polynomial Bounds The concrete constants in Table 2 arise from a formal cost model that assigns unit cost to every cons cell, compatibility check, and list traversal. Generic clearing is quartic because each pass filters every triplet against two neighbouring tiers and the process iterates at most cts_size(S)cts\_size(S) times; for single-forbidden sliding-window structures clearing is the identity (Corollary 7.1), so only one pass is needed and the bound collapses to quadratic. The SVI bound comes from building two basic graphs and intersecting their vertices. Full cost-model definitions, intermediate lemmas, and the arithmetic inductions are given in files Complexity.v and GapClosure.v. Theorem 7.1 (Generic Clearing Bound). clear_structureclear\_structure is bounded by 100n4+100100n^4+100 in the generic case. Theorem 7.2 (Tight Clearing Bound). For single-forbidden sliding-window structures, clear_structureclear\_structure is bounded by 2000n2+20002000n^2+2000. Theorem 7.3 (SVI Filter Bound). effective_procedureeffective\_procedure is bounded by 3n2+73n^2+7. Theorem 7.4 (Full Pipeline Bound). The full SVI pipeline is bounded by 200n4+200200n^4+200. Corollary 7.1 (Full clearing is identity). Let S be a non-empty CTS whose every tier is single-forbidden. Then clear⁡(S)=Sclear(S)=S. 7.3. Python Implementation The Python runtime (approximately 2,500 lines across eight modules) mirrors the Rocq definitions exactly: CTS._extend_paths is a direct port of extend_paths, paths are maintained in reverse order, and the accumulator reset is harmless by Lemma extend_paths_nil_acc (Algorithm.v). A runtime guard (is_sliding_window_formula) checks whether the input is a well-formed sliding-window CNF; if the predicate holds, the solver follows the verified clause-by-clause path (either the extracted OCaml binary or the Python port), otherwise it falls back to the unverified grouped-window heuristic with a RuntimeWarning. For general 3-CNF the solver delegates to Z3; SAT assignments are verified by the extracted eval_cnf, and UNSAT proofs are checked by the Rocq-extracted Swansea RUP checker [17]. Any verification failure raises RuntimeError; there is no silent fallback. 7.4. Reproducible Build The complete toolchain (Rocq proofs, extracted OCaml code, Python runtime, Z3, Swansea RUP checker, and TLA+ specifications) is available as a curated Zenodo artifact at 10.5281/zenodo.20397950 [19]. The artifact includes a reproducible Dockerfile based on Ubuntu 22.04, which builds all components from source and runs the full test suite. 8. Illustrative Examples (Formal guarantees are summarised in Table 1.) 8.1. Extracted-Code Smoke Tests We exercised the extracted OCaml code and the Python wrapper on three manually constructed instances: a simple SAT clause, an UNSAT formula consisting of all eight possible clauses on three variables, and an overlap-UNSAT case where grouped windows contradict on a shared variable. The first two are sliding-window formulas (verified fragment); the third is a non-sliding-window heuristic example. For the verified sliding-window fragment (k=1k=1 clause per window), the extracted solver is a complete decision procedure with no false positives and no false negatives: soundness follows from the eval_cnf post-check, and completeness from the translation equivalence (Theorem 4.5) together with the verified greedy fallback (sat_assignment_aux), which always succeeds on well-formed sliding-window inputs. We validated the extracted solver exhaustively against a brute-force oracle for all sliding-window formulas with n≤6n≤ 6 variables. 8.2. Heuristic Filter Effectiveness The basic validation tests above exercise the verified fragment. To assess whether the unverified grouped-window heuristic ever yields non-trivial filtration, we generated two classes of structured instances: (i) dense sliding-window CNFs with multiple clauses per consecutive variable window, and (i) highly overlapping groups in which many clauses share the same three variables. On these instances SVI reports False for a measurable fraction of UNSAT cases (between 19% and 100% in small-scale experiments, depending on clause density), because dense forbidding quickly empties tier intersections. On random 3-SAT, by contrast, the filter is empirically ineffective: SVI almost never returns False. These observations are illustrative, not formally guaranteed—they concern the heuristic shell, not the verified fragment. Their purpose is to demonstrate that the architecture can filter structured instances, even if the general 3-CNF pipeline remains a research prototype. On random non-sliding-window 3-CNF (n≤6n≤ 6, 60 instances) the heuristic pipeline agrees with brute force on 100% of cases, confirming that the post-check eliminates all SVI false positives. We do not report larger-scale or competitive benchmarks: the heuristic filter is empirically ineffective on random 3-SAT (SVI almost never returns False), and VFR is not positioned as a competitor to industrial CDCL solvers. 9. Discussion 9.1. What TLS Provides After formalisation, the value proposition of TLS lies not in a complete polynomial-time decision procedure, but rather in a combination of three structural contributions: A provably correct one-sided filter. When SVI reports emptiness, the formula is guaranteed to be unsatisfiable (proved in Rocq for well-formed sliding-window CNF). The running time is polynomial in the size of the structure—O⁡(|V1|⋅|V2|)O(|V_1|·|V_2|), or O⁡(n2k2)O(n^2k^2) for k tiers of size O⁡(n)O(n). We emphasize: the Rocq development proves termination (Theorem 4.9), correctness (Theorem 4.3), and the polynomial bound formally in Complexity.v (quartic for clearing, quadratic for SVI). The earlier asymptotic analysis is now complemented by concrete, mechanised step-count bounds. On random 3-SAT the heuristic filter is empirically ineffective (SVI almost never returns False), so we do not report competitive benchmarks: VFR is a research prototype, not a practical solver (Section 8). For well-formed sliding-window CNF the verified pipeline is complete. Any positive filter rates observed on structured instances outside the verified fragment are empirical properties of the unverified grouped-window heuristic, not formally guaranteed results. 9.2. Scientific Novelty We summarise the concrete contributions that go beyond prior work. 1. First formal mechanisation of Romanov’s framework. Romanov stated the forward direction of SVI (Theorem 4.1) without proof and assumed the converse without justification. We formalise the entire framework in Rocq and prove: • the forward direction for pairs (Theorem 4.1) and for systems of k structures (Theorem 4.2); • the exact boundary where the converse fails (Section 6); • a new bi-implication for aligned intersection (Theorem 4.3), which Romanov did not consider. All proofs are machine-checked; there are zero admitted goals. 2. Aligned intersection equivalence—a new result. Theorem 4.3 (and its systemic extension Theorem 4.4) is entirely absent from Romanov’s work. It establishes that tier-aligned intersection combined with build_paths_allbuild\_paths\_all yields a correct and complete decision procedure for aligned structures. Its value lies in the mechanisation: it certifies that three independently defined concepts—compatible satisfying sets, aligned intersection, and the recursive path-building algorithm—are mutually consistent, enabling verified OCaml extraction. 3. Exact formal counterexamples. We do not merely claim that SVI is incomplete; we provide formal counterexamples in Rocq that mark the exact boundary: • Theorem 4.7 (semantic gap): a CTF can satisfy the weak predicate satisfies_ctfsatisfies\_ctf yet yield no path after clearing; • Theorem 4.8: clearing can destroy valid paths because can_adjoincan\_adjoin requires forward compatibility while build_paths_allbuild\_paths\_all checks only backward compatibility. These are not empirical observations but formally proved existential statements. 4. Verified constructive solver for grouped sliding-window CNF. For grouped sliding-window CNFs with disjoint variable ranges (multiple clauses per consecutive variable window) we prove in Rocq a constructive, extractable solver solve_grouped_sliding with both soundness (Theorem 4.11) and completeness (Theorem 4.12) proved in Rocq. The solver combines verified path finding (find_first_valid_s), a verified greedy assignment constructor (sat_assignment_aux), and a constructive merge of disjoint group assignments. To our knowledge, this is the first verified solver for grouped sliding-window 3-CNF that is both sound and complete and extracts to executable OCaml code. 5. Mechanised polynomial bounds with concrete constants. The Rocq development includes a formal cost model (Complexity.v, approximately 1,000 lines) that assigns unit cost to every cons cell, compatibility check, and list traversal. We prove closed-form inequalities with explicit constants—100n4+100100n^4+100 for generic clearing, 2000n2+20002000n^2+2000 for the single-forbidden fragment, 3n2+73n^2+7 for SVI—by induction on the input structure, not merely asymptotic analysis. For the single-forbidden fragment the bound collapses from quartic to quadratic because clearing is the identity (Corollary 7.1), a fact we also prove formally. Positioning. These contributions do not expand the class of polynomially solvable 3-SAT instances: well-formed sliding-window CNF has primal graph pathwidth ≤2≤ 2, which is already solvable in linear time by classical dynamic programming. Our novelty lies in reconstructing this tractable fragment inside Romanov’s triplet framework with full formal certification and executable extraction. 9.3. Relation to Bounded-Treewidth SAT Well-formed sliding-window CNF has primal graph pathwidth ≤2≤ 2 (each clause covers three consecutive vertices of a path, so the primal graph is a subgraph of the square of a path). SAT for graphs of bounded pathwidth is a classic FPT (Fixed-Parameter Tractable) result: dynamic programming on a path decomposition of width w solves it in time 2O⁡(w)⋅n2^O(w)· n [15]. Our verified polynomial bounds for clearing and SVI therefore do not expand the class of polynomially solvable 3-SAT instances; they reconstruct the same pathwidth-≤2≤ 2 fragment within Romanov’s framework. The connection to the FPT literature is worth making explicit. In a standard path decomposition each bag contains the variables active at that position, and the DP table stores all satisfying assignments of the bag (size 2w+12^w+1). In Romanov’s construction each tier corresponds to a bag of size 3, but instead of enumerating 23=82^3=8 assignments directly, the tier stores the forbidden triplets—those ruled out by the clauses—and the DP step is replaced by a local compatibility check (compatible⁡(t1,t2)compatible(t_1,t_2)) between adjacent bags. Thus a CTS is essentially a nice path decomposition in which • Introduce/forget steps are implicit (the path is uniform, each bag contains exactly three consecutive variables); • Join steps are absent (the graph is a path, not a tree); • the DP table is replaced by an explicit triplet set, and the transition function is replaced by tier-wise intersection and adjacency checking. This equivalence explains why the single-forbidden fragment (where each tier contains exactly one forbidden triplet) admits a quadratic bound: the DP table has constant size 8, and the transition is a simple table lookup. Our contribution is not a new complexity improvement but a formally certified reformulation: we prove in Rocq that Romanov’s triplet constructions yield a correct decision procedure for the pathwidth-≤2≤ 2 fragment, with explicit polynomial bounds and executable extraction. The practical interest of VFR lies not in solving sliding-window formulas (which is already tractable classically), but in using SVI as a fast, auditable filter for harder structured instances that lie outside the verified fragment. A novel structural decomposition. TLS decomposes a formula into independent CTFs based on variable overlap. This natural partitioning supports parallel solving and reveals structural properties of the instance (e.g., tightly coupled vs. loosely coupled variable groups). A geometric interpretation of SAT. Unlike the abstract implication graphs of CDCL, TLS provides a concrete picture: triplets as nodes, compatibility as edges, and satisfying assignments as paths through a layered graph (Figure 1). This makes TLS a valuable pedagogical tool for teaching SAT and constraint satisfaction. 9.4. Comparison with Classical SAT Solving Unlike classical DPLL/CDCL, which operate directly on CNF clauses and rely on clause learning and implication graphs, VFR translates a formula into tiered triplet structures and reduces satisfiability to finding a compatible path. This yields a concrete, visualisable representation and a polynomial one-sided filter (SVI), but completeness requires an exponential post-check and the prototype does not implement clause learning. The main gain is a smaller, mechanically checked trust base for the verified sliding-window fragment. 9.5. Related Work Our work complements a growing body of verified SAT solvers. Maric [9] verified a modern DPLL solver in Isabelle/HOL, proving correctness of unit propagation, conflict analysis, and clause learning. Blanchette et al. [10] extended this to a verified CDCL solver with proof generation, watched literals, and incremental solving. Subsequent work refined this into competitive verified solvers: Fleury et al. [11] formalised IsaSAT, an imperative CDCL solver with watched literals that approaches the performance of unverified solvers on some benchmarks. Complementing solver verification, Lammich [12] developed the GRAT toolchain, a formally verified certificate checker for DRAT proofs that outperforms the unverified reference implementation. Heule et al. [13] verified UNSAT proofs with extended resolution. These works establish a high standard for verified SAT solving; our work is the first to explore an alternative combinatorial foundation, using Romanov’s triplet logic. Structural differences. In DPLL/CDCL, the formula remains a flat set of clauses; the solver reasons via implication graphs, watched literals, and conflict-driven clause learning. A proof of correctness must therefore maintain global invariants over the trail, the learned-clause database, and the watched-literal indices. In contrast, TLS decomposes the formula geometrically into tiers of variable triplets, and satisfiability reduces to finding a compatible path through a layered graph. There is no implication graph, no watched literals, and no learned clauses—the only “conflict” is the emptiness of a tier intersection. Reasoning is local: each tier can be analysed as an independent set of triplets, and global correctness follows from pairwise compatibility. This locality makes TLS proofs compositional (tier-by-tier) rather than trace-based (execution-by-execution). Insights from the alternative mechanisation. The TLS formalisation suggests three lessons that differ from the CDCL experience. First, different data structures yield different proof localities: whereas CDCL reasons about global implication graphs and watched literal indices whose correctness depends on intricate trail invariants, TLS decomposes the formula into tiers of triplets whose adjacency can be checked pairwise. The 424 proved statements in our Rocq development are overwhelmingly lemmas about tier-wise inclusion, compatibility, and intersection—concepts that have direct geometric meaning. Second, a filter architecture offers a different trade-off: the polynomial filter (SVI) can be verified in isolation, but completeness requires an exponential post-check. CDCL solvers are monolithic yet complete; VFR sacrifices completeness for a clean verified boundary (Table 1). Third, concrete counterexamples are easy to construct: because the reasoning is geometric, one can draw a three-tier structure and readily see why clearing is non-conservative (Section 4.5). Why a verified one-sided filter matters. Verified CDCL solvers are complete decision procedures, but they are also heavy: thousands of lines of proof, complex imperative invariants, and aggressive performance engineering. Not every application needs a full solver. A verified one-sided filter answers a different but useful question: “Is this instance definitely outside the easy fragment?” with a proof-backed guarantee. For well-formed sliding-window CNF, the filter is not merely one-sided—it is exactly complete (Theorem 4.12), yet its proof is orders of magnitude smaller than a full CDCL proof. In program analysis or hardware verification, formulas often exhibit bounded pathwidth or sliding structure; a lightweight verified filter can discharge these instances quickly without invoking a heavy solver. The two approaches are complementary: a verified filter can be placed in front of any solver (even unverified) to obtain a sound architecture in which the polynomial stage is proof-carrying and the exponential stage is a standard fallback. Where CDCL verifies “the solver always returns the correct answer,” VFR verifies “the polynomial filter never produces false negatives on the fragment.” The fragment (pathwidth ≤2≤ 2) is classically tractable; our contribution is a geometric reinterpretation with machine-checked polynomial bounds and an extractable implementation, not a new complexity result. Triplet-based representations have appeared in various SAT contexts, although not as a complete solving paradigm. Romanov’s TLS [3] is the first systematic framework built on tier-wise triplet structures and hyperstructure intersection. His insight—decomposing a formula into geometric layers and searching for compatible paths rather than raw assignments—is distinct from both DPLL search and CSP propagation. Our work is the first to subject TLS to mechanised formal verification, identifying the precise conditions under which its Simple Vertex Intersection is correct and where it requires supplementation. The clearing procedure in TLS resembles arc consistency enforcement in constraint satisfaction problems (CSPs) [14]. The difference is that TLS operates on explicit triplet sets rather than general relations. 9.6. Threats to Validity The fundamental gap: grouped-window translation is a one-sided filter. The most serious threat is that our Rocq theorems are proved for a clause-by-clause translation (FormulaTranslation.v), whereas the VFR prototype uses a grouped-window decomposition that merges multiple clauses sharing the same variable triple into a single tier. We have now proven (the group-equivalence and dense-groups lemmas in FormulaTranslation.v) the full forward equivalence: if an assignment satisfies the concatenated CNF, then the grouped CTF is satisfied. The converse, however, is false: satisfies_ctfsatisfies\_ctf checks each tier independently and does not enforce consistency between overlapping windows. A concrete counterexample: group 0 consists of the seven clauses on variables (x0,x1,x2)(x_0,x_1,x_2) whose only satisfying pattern is (0,0,0)(0,0,0), and group 1 consists of the seven clauses on (x1,x2,x3)(x_1,x_2,x_3) whose only satisfying pattern is (1,1,1)(1,1,1). The grouped CTF has two tiers, forbidding all triplets except (0,0,0)(0,0,0) and (1,1,1)(1,1,1) respectively; the sequence =[0,0,0,1,1,1]s=[0,0,0,1,1,1] avoids both forbidden sets, so satisfies_ctf(,ϕ)=satisfies\_ctf(s,φ)= true. Yet the CNF is unsatisfiable: group 0 forces x1=x2=0x_1=x_2=0 while group 1 forces x1=x2=1x_1=x_2=1, so no assignment realises s. This counterexample is formalised in FormulaTranslation.v. Consequently, the grouped-window heuristic is a one-sided (sound but incomplete) filter, not a complete decision procedure. The end-to-end guarantee holds only when the input is a well-formed sliding-window CNF translated clause-by-clause; for all other inputs the pipeline is heuristic. Our empirical evaluation relies on instances derived from 3-CNF formulas, both randomly generated and from the SATLIB benchmark suite. Because the grouped-window translation is unverified, these benchmarks demonstrate operational behaviour of a heuristic, not formally verified correctness. A second threat concerns the scalability of VFR’s post-check: our timeout-based evaluation for n≥100n≥ 100 does not establish an upper bound on the fraction of instances solvable within a practical time limit. Our Rocq formalisation proves termination and a fixed-point characterisation of clearing (Theorem 4.9 and Theorem 4.10), but we do not prove that clearing preserves all satisfying sets—in fact, we prove the opposite: Theorem 4.7 shows that the weak predicate satisfies_ctfsatisfies\_ctf can admit locally consistent assignments that do not correspond to any globally compatible path. TLA+ model-checking limitation. The TLA+ (Temporal Logic of Actions) specifications provide finite-state sanity checks on small instances (MaxVars≤3MaxVars≤ 3). The module TLSSpec exhausts TLC (the TLA+ model checker) memory for MaxVars>2MaxVars>2 because explicit-state model checking of a 3-SAT solver is inherently exponential. This is expected: TLC serves as an auxiliary debugging tool for small illustrative instances, while the general correctness guarantees for arbitrary n are provided entirely by the Rocq proofs (424 lemmas and theorems). No fix is planned: switching to Apalache (a symbolic model checker for TLA+) would extend the feasible bound only marginally and would not add scientific value, since the general theorem is already machine-checked in Rocq for arbitrary n. Users should treat TLC checks as illustrative rather than as formal verification. 9.7. Limitations and Future Work The main practical limitation is the exponential post-check: when SVI returns True, the solver must enumerate partial assignments from each CTS. A second limitation is the absence of a verified CNF-to-CTF translation for grouped-window formulas; even though SVI and clearing are correct, the input may not faithfully represent the original formula. This is the single most important gap in turning the verified core into an end-to-end verified solver. A third limitation is that verified permutation search is exhaustive and hence practical only for n≤8n≤ 8; a verified polynomial-time recognition algorithm for the sliding-window class (membership is decidable in polynomial time; cf. Section 3.1) would widen the verified fragment. A fourth, fundamental limitation is that arbitrary 3-CNF formulas typically admit no sliding-window ordering at all, so formal guarantees for general 3-SAT require external verified solvers or certificates. An important research direction is to use the polynomial clearing procedure on single-forbidden structures as an alternative proof format: showing that CTS derivations map to short DRAT or RUP proofs would let the verified kernel produce certificates rather than merely check them. Engineering refinements such as lazy path generation, CDCL integration, and a native LRAT checker remain natural but secondary next steps for future work. 10. Conclusion We presented the first formal verification of Romanov’s Triplet Logic in Rocq, complemented by empirical validation. Our central findings are: • SVI is a correct one-sided filter: a joint satisfying set implies non-emptiness, but the converse fails when common triplets appear in non-aligned tiers (Section 6). • Aligned intersection yields a true bi-implication (Theorem 4.3), extended systemically to k structures (Theorem 4.4). • The weak predicate satisfies_ctfsatisfies\_ctf is incomplete with respect to global path existence; the strong predicate closes this gap for well-formed sliding-window CNF, where the clause-by-clause CNF-to-CTF translation preserves satisfiability (Section 4). • Clearing and SVI have verified polynomial bounds (Table 2), and the extracted VFR prototype combines the verified filter with an exponential post-check. To explore the structural potential of TLS, we proposed VFR: a hybrid architecture combining SVI’s filter with an exponential post-check. We proved the filter’s correctness formally and implemented the pipeline in Python, validating it against SAT and UNSAT instances, including cases where SVI gives false positives. We observed 100% agreement with a brute-force oracle on random sliding-window instances with n≤6n≤ 6. The entire toolchain is packaged in a reproducible Docker image (Section 7.4) that builds all components from source and passes the full automated test suite. Our work positions TLS as a rigorous combinatorial framework for reasoning about compatible paths in tiered triplet structures, with a provably correct polynomial-time filter as a theoretical building block. Formal Verification All definitions, lemmas, and theorems described in this paper have been formally verified in Rocq 9.1.1. The development comprises more than 23,000 lines of Rocq code across seventeen files with 424 proved lemmas and theorems and zero admitted goals. The source code is available in the curated Zenodo artifact [19]. Acknowledgments This work is an output of a research project implemented as part of the Basic Research Program at the National Research University Higher School of Economics (HSE University). During the preparation of this work, the author used large language models (DeepSeek, GLM, and Kimi Code) for generating and debugging Python, OCaml, TLA+, and Rocq (Coq) code, creating tests and scripts, and optimising algorithms; for language polishing and stylistic refinement of the manuscript; for LaTeX code debugging; and for literature search, review and summarisation. The author reviewed and edited all outputs as needed and takes full responsibility for the content of the published article. The author thanks arXiv for hosting the preprint version of this work (arXiv:2608.18445) [18]. The author is deeply indebted to the late Vladimir Romanov, whose pioneering ideas on triplet structures inspired this formal investigation. References [1] S. A. Cook. The complexity of theorem-proving procedures. In Proc. STOC, pages 151–158. ACM, 1971. [2] L. A. Levin. Universal enumeration problems. Problemy Peredachi Informatsii, 9(3):115–116, 1973. [3] V. F. Romanov. Non-Orthodox Combinatorial Models Based on Discordant Structures. 2011 (arXiv:1011.3944 [v2], revised Jan 2011; orig. Nov 2010). [4] The Rocq Development Team. The Rocq Prover, version 9.1.1. https://coq.inria.fr/, 2026. [5] N. Eén and N. Sórensson. An extensible SAT-solver. In Proc. SAT, pages 502–518. Springer, 2003. [6] G. Audemard and L. Simon. Predicting learnt clauses quality in modern SAT solvers. In Proc. IJCAI, pages 399–404, 2009. [7] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. DAC, pages 530–535. ACM, 2001. [8] A. Biere, M. Heule, H. van Maaren, T. Walsh, editors. Handbook of Satisfiability. IOS Press, 2009. [9] F. Maric. Formalisation and implementation of modern SAT solvers. J. Automated Reasoning, 43(1):81–119, 2009. [10] J. C. Blanchette, M. Fleury, C. Weidenbach. A verified SAT solver framework with learn, forget, restart, and incrementality. J. Automated Reasoning, 61(1–4):333–365, 2018. [11] M. Fleury, J. C. Blanchette, P. Lammich. A verified SAT solver with watched literals using imperative HOL. In Proc. CPP, pages 158–171. ACM, 2018. [12] P. Lammich. Efficient verified (UN)SAT certificate checking. J. Automated Reasoning, 64(3):513–532, 2020. [13] M. J. H. Heule, W. A. Hunt Jr., N. Wetzler. Verifying refutations with extended resolution. In Proc. CADE, pages 345–359. Springer, 2013. [14] C. Bessiere. Constraint propagation. In Handbook of Constraint Programming, pages 29–82. Elsevier, 2006. [15] M. Alekhnovich and A. A. Razborov. Satisfiability, branch-width and Tseitin tautologies. In Proc. FOCS, pages 593–603. IEEE, 2002. [16] K. S. Booth and G. S. Lueker. Testing for the consecutive ones property, interval graphs, and graph planarity using PQ-tree algorithms. J. Comput. System Sci., 13(3):335–379, 1976. [17] H. Bryant, A. Lawrence, M. Seisenberger, and A. Setzer. Verification of Z3 RUP proofs in Coq-Rocq and Agda. https://github.com/HarryBryant99/Verification-of-Z3-RUP-Proofs-in-Coq-Rocq-and-Agda, 2025. [18] D. V. Alexandrov. Formal verification of Romanov’s triplet logic: A verified filter for sliding-window 3-CNF with application to structured formulas. arXiv preprint arXiv:2608.18445, 2026. [19] D. V. Alexandrov. Formal verification of Romanov’s triplet logic: artifacts and reproducible build. https://doi.org/10.5281/zenodo.20397950, 2026.

Instant research discovery