PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Dmitry V. Alexandrov

arXiv:2608.18445v1cs.LOcs.AIcs.CCcs.PL

TL;DR

Romanov’s Triplet Logic lacked mechanised formal foundations and an exactly established correctness boundary. This paper formalises TLS in Rocq and shows that SVI is a one-sided filter generally, while aligned intersection restores equivalence with compatible joint satisfying sets.

  • Problem

    Romanov’s Triplet Logic lacked mechanised formal foundations and an exactly established correctness boundary for its automated-reasoning framework.

  • Method

    The paper formalises TLS in Rocq, translating clauses into triplet structures and applying fixed-point clearing to remove incompatible triplets.

  • Results

    SVI is a correct one-sided filter, while aligned intersection yields a bi-implication and strong satisfiability closes the weak predicate’s global-consistency gap.

  • Takeaways & Limitations

    The mechanised development provides certified foundations for TLS and clarifies which structural conditions support complete reasoning about compatible paths.

  • Takeaways & Limitations

    The VFR prototype’s grouped-window translation is sound only one way because its independently checked tiers do not enforce consistency across overlapping windows.

Abstract

from arXiv · show

We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a triplet-based combinatorial framework for reasoning about compatible paths through layered triplet structures, called Compact Triplets Structures (CTS), and their intersection via Romanov's Effective Procedure, which we refer to as Simple Vertex Intersection (SVI). Originally motivated by Boolean satisfiability, TLS constitutes a self-contained mathematical theory whose formal properties had not been previously established. We formalise the core of TLS in Rocq, including Compact Triplets Formulas (CTF), CTS, hyperstructures, clearing, and SVI. For the well-formed sliding-window fragment we verify a clause-by-clause CNF-to-CTF translation, the clearing procedure, and aligned intersection, and we prove explicit polynomial-time bounds for the filter stages. Our main contribution is a precise correctness boundary: the existence of a joint satisfying set implies non-emptiness of SVI, but the converse does not hold in general; for aligned structures we recover a complete bi-implication, extended to systems of structures. We also formalise soundness of grouped-window translation and exhibit a formal counterexample to its completeness. We introduce VFR, an extracted OCaml prototype that provides a verified decision procedure for the sliding-window fragment and a sound one-sided filter for general 3-CNF, with a Python runtime and reproducible Docker packaging. Benchmarks on random and structured instances confirm the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises more than 23,000 lines of code across seventeen files, with 427 proved lemmas and theorems and zero admitted goals.

1 Introduction

The paper mechanises Romanov’s Triplet Logic in Rocq and precisely establishes where its SVI filter is sound, incomplete, or complete for aligned structures. It also defines a verified sliding-window fragment while separating formally verified components from heuristic general-3-CNF processing.

  • Formalisation: Rocq formalises CTF, CTS, hyperstructures, SVI, path construction, and compatibility, supported by exhaustive model checking.The development uses Rocq 9.1.1 and proves basic correctness lemmas for the TLS core.
  • Correctness boundary: JSS implies non-emptiness of SVI for non-empty structures, but the converse fails in general, as shown by Rocq counterexamples and exhaustive Python model checking.Thus SVI is a sound one-sided filter rather than a complete decision procedure; emptiness guarantees unsatisfiability.
  • Prototype and scope: VFR implements the verified sliding-window pipeline while using an unverified grouped-window heuristic for general 3-CNF; agreement is 100% on the verified fragment, but general random-instance filtering is ineffective.The paper positions TLS as a mechanised, structurally transparent framework rather than a faster alternative to CDCL.
  • Aligned completeness: Aligned CTS intersection contains a full-length path if and only if a compatible JSS exists, and this equivalence extends to systems of k aligned structures.These theorems provide the formal foundation for the post-check and the systemic tier-wise intersection.
  • Structural reasoning: Clearing terminates via a tight CTS-size measure and reaches a fixed point where every surviving triplet has compatible neighbours in adjacent tiers.The formalisation also identifies a gap between independently satisfied 3-bit windows and globally compatible paths after clearing.
  • Trust boundary: The verified pipeline covers clause-by-clause CNF-to-CTF translation, clearing, aligned intersection, path-existence theorems, SVI soundness, and polynomial-time bounds.The grouped-window decomposition, general 3-CNF heuristic pipeline, and associated benchmarks remain unverified empirical material.

2 Background: Romanov’s Triplet Logic

Romanov’s Triplet Logic represents 3-CNF clauses as triplets organized into Compact Triplets Formulas and Structures, with compatibility enabling consistent sliding-window paths. Its verified core covers the clause-by-clause pipeline and aligned SVI for well-formed formulas, while broader grouped and general 3-CNF procedures remain heuristic.

  • Verification boundary: For well-formed sliding-window CNF, clause translation, clearing, aligned intersection, and SVI are formally verified, whereas grouped-window decomposition and general 3-CNF processing are unverified heuristics.Only the clause-by-clause pipeline is formally verified; greedy permutation search, overlapping-group handling, post-check backtracking, and the general pipeline have no formal guarantee.
  • Representation: A 3-CNF clause becomes a triplet in {0, 1}^3 over an ordered variable triple, and tiers group triplets by shared variable indices.A Compact Triplets Formula is a list of tiers, each tier being a set of triplets.
  • Construction pipeline: The construction translates each clause into a forbidden negation-pattern triplet, complements tiers to form a CTS, and clears incompatible triplets.The CTS contains triplets not forbidden by the corresponding clause group; clearing is applied after raw CTS construction.
  • Compatibility and paths: Sliding-window compatibility requires agreement on overlapping positions, allowing paths through adjacent tiers to induce consistent variable assignments.Adjacent windows overlap by two variables, and a valid path such as 011 →110 →101 induces x0 = 0, x1 = 1, x2 = 1, x3 = 1, x4 = 0.
  • Intersection: SVI constructs a hyperstructure from triplets common to two CTS graphs, while systemic SVI extends common-vertex computation to k ≥2 structures.The common triplet need not occur at the same tier index; for systems, non-emptiness implies pairwise common triplets.

3 Heuristic Pipeline

The heuristic pipeline decomposes 3-CNF clauses into CTFs, constructs raw CTS by complementation, and clears incompatible triplets through fixed-point filtering. This grouped-window procedure is operational rather than Rocq-verified, while the verified fragment is restricted to well-formed sliding-window CNF.

  • Verification boundary: The grouped-window pipeline used by VFR is not formally verified; Rocq mechanises only the clause-by-clause translation for well-formed sliding-window CNF.The verified fragment requires clauses containing three consecutive variables, whereas grouped decomposition is an unverified heuristic for general 3-CNF.
  • Pipeline overview: Three phases—decomposition, tier construction, and clearing—transform a 3-CNF formula into a cleared CTS.Decomposition groups clauses by variable sets, tier construction complements forbidden triplets, and clearing removes incompatible lines.
  • Decomposition: Clause grouping encodes each clause as a triplet in a CTF annotated with its three variable indices, producing at most m CTFs.For each variable group {i, j, k}, the remaining variables extend a permutation, while literal negation determines each triplet bit.
  • Clearing: Clearing repeatedly retains only triplets with compatible neighbours in both adjacent tiers, using all 2^3 = 8 triplets as the boundary condition.Each pass builds a fresh list and repeats until no further triplets are eliminated.
  • Permutation search: Finding a variable ordering that makes arbitrary 3-CNF sliding-window is NP-complete, but exhaustive permutation search is verified to find one whenever it exists.The ordering problem is equivalent to testing whether the associated 3-uniform hypergraph has pathwidth at most 2.

4 Formalisation in Rocq

The Rocq formalisation defines the triplet-based structures and verifies their core path, translation, clearing, and aligned-intersection properties. It establishes completeness for aligned structures while identifying limits for weak satisfiability and grouped constructions.

  • 4.1 Key Definitions: A triplet is a Boolean triple, tiers are lists of triplets, CTS are lists of tiers, and satisfying sets flatten paths into Boolean lists.The local extractor retrieves triplet i from positions 3i, 3i + 1, and 3i + 2 when available.
  • 4.3 Proved Lemmas: 427 lemmas and theorems across seventeen files formalise path construction, intersection, translation, clearing, and satisfiability relationships.The development required nested inductions and arithmetic reasoning about nth error and tier lengths.
  • 4.3 Proved Lemmas: A compatible satisfying set implies non-empty SVI, while aligned structures recover the converse through full-length path equivalence.For systems of k aligned structures, systemic tier-wise intersection has a full-length path iff a compatible joint satisfying set exists for the entire system.
  • 4.4 Translation Correctness: Clearing preserves soundness of produced paths, while raw-tier emptiness occurs exactly when the corresponding formula tier contains all 8 triplets.The construction also proves relabeling preserves satisfiability and dense grouped-window translation is sound.
  • 4.3 Proved Lemmas: Path construction is equivalent to compatible satisfying-set existence for a non-empty structure, and cleared CTF strong completeness links compatibility-aware satisfiability to non-empty paths.Raw construction completeness provides the corresponding implication before clearing.
  • 4.5 Counterexamples and Formal Limits: Weak local satisfiability does not guarantee a compatible path after clearing, and formal counterexamples delimit the framework’s completeness claims.Completeness is recovered for aligned intersection, whereas grouped-window results establish soundness rather than general completeness.
  • 4.4 Translation Correctness: For well-formed sliding-window CNF, standard satisfiability is equivalent to satisfiability of the clause-by-clause translated CTF.Each clause becomes a separate tier containing one forbidden triplet, and produced paths yield assignments satisfying the original formula.

5 Empirical Validation via Exhaustive Enumeration

Exhaustive model checking tested four SVI variants across 787,244 exhaustive cases and 500 random instances. Every claimed reverse implication failed, with counterexamples arising when SVI matches triplets across misaligned tiers.

  • Enumeration: 787,244 exhaustive cases plus 500 random instances were enumerated using a Python-based model checker.The enumeration covered all CTS-structure pairs within small bounds.
  • Reverse implication: Four SVI variants were checked, and every claimed reverse implication had a counterexample.This result motivated caution before undertaking Rocq proofs of the reverse direction.
  • Counterexample pattern: Counterexamples consistently occurred when SVI matched a triplet from tier i of S1 with tier j ≠ i of S2, producing a non-empty hyperstructure.The shared pattern was cross-tier rather than aligned-tier intersection.

6 The Correctness Boundary: False Positives in SVI

SVI non-emptiness is only a one-sided soundness result in general: it may report false positives from cross-tier or partial matches. Additional semantic gaps arise because local CTF satisfaction and clearing do not preserve global path realizability, while aligned structures recover completeness.

  • Correctness boundary: Only the forward implication from a joint satisfying set to non-empty SVI is proved; the converse fails in general.Theorem 4.1 establishes the forward direction, while non-emptiness alone does not imply a joint satisfying set.
  • Semantic gaps: Local CTF satisfaction can accept assignments whose independently inspected windows disagree on overlapping bits and cannot form compatible paths.Theorem 4.7 gives tiers permitting (false, true, true) and (true, false, true), causing conflicting overlap values despite satisfies ctf returning true.
  • Clearing: Clearing may remove triplets from valid paths because it requires both predecessor and successor compatibility, although it never creates new full-length paths.This non-conservativity differs from reverse monotonicity: surviving paths were already present, and aligned intersection restores completeness without relying on clearing to preserve paths.
  • SVI false positives: Cross-tier matching makes SVI non-empty when triplets match different tiers, even though every aligned tier pair may be disjoint.In the shifted example, (0, 0, 0) and (1, 1, 1) match across tiers, but neither corresponding tier pair shares a triplet.
  • SVI false positives: Partial tier matches likewise produce non-empty SVI despite an unmatched tier preventing any aligned joint satisfying set.The example shares (0, 0, 0) in tier 0 but has no common triplet in tier 1, so the formula is unsatisfiable while SVI reports non-empty.

7 VFR: A Prototype Solver with Post-Checking

VFR uses SVI as a fast, one-sided filter followed by exhaustive post-checking and final CNF verification. Rocq proves explicit polynomial bounds for the filter stages, while the complete decision procedure remains exponential in the worst case.

  • Pipeline: VFR decomposes 3-CNF into CTFs, constructs CTSs through complementation and clearing, applies SVI, and verifies any post-check candidate against the original CNF.An SVI False result guarantees unsatisfiability; an SVI True result triggers backtracking for a globally consistent assignment.
  • Verified complexity: 200n4 + 200 bounds the full SVI pipeline, combining intersection clearing with the quadratic SVI cost.The bound is proved by induction and arithmetic reasoning in Rocq.
  • Post-check: The post-check is exponential: path enumeration can reach O(8m), and backtracking explores O(∏k_j=1 p_j) time with O(n · k) space.The exponential worst case applies to the complete decision procedure, not the clearing and SVI filter stages.
  • Sliding-window fragment: Clearing is the identity for single-forbidden tiers, including well-formed sliding-window CNF formulas where each clause contributes exactly one forbidden triplet.Every allowed triplet has at least one compatible predecessor and successor, so no triplet is removed.

8 Illustrative Examples

The examples validate SVI exhaustively on the verified sliding-window fragment and test its heuristic behaviour on structured and random non-sliding-window instances. SVI is complete for the verified fragment, while post-checking removes heuristic false positives on the tested random cases.

  • Manual examples: Three manually constructed instances exercise the extracted OCaml code and Python wrapper: two verified sliding-window formulas and one non-sliding-window heuristic example.These instances are listed in Table 4.
  • Verified fragment: For k = 1 sliding-window formulas, SVI detects every UNSAT instance with no false positives or false negatives.The result was validated exhaustively against a brute-force oracle for all formulas with n ≤6 variables.
  • Grouped-window heuristic: Structured instances produced SVI=False for 19%–100% of UNSAT cases in small-scale experiments.The tested classes were dense sliding-window CNFs with multiple clauses per window and highly overlapping groups sharing the same three variables.
  • Random non-sliding-window tests: On 60 random non-sliding-window 3-CNF instances with n ≤6, the heuristic pipeline agreed with brute force on 100% of cases.The post-check eliminated all SVI false positives in this test set.
  • Scope and limitations: The heuristic filter was empirically ineffective on random 3-SAT, where SVI almost never returned False, and no larger-scale or competitive benchmarks were reported.VFR was not positioned as a competitor to industrial CDCL solvers.

9 Discussion

The discussion positions TLS as a mechanised, structurally decomposed framework that provides a verified one-sided filter and a complete procedure for aligned structures, while formally exposing its limits. It also contributes constructive grouped-window solving, explicit complexity bounds, counterexamples, and a distinct geometric alternative to conventional verified SAT solvers.

  • Core contribution: TLS’s central value is a provably correct polynomial-time one-sided filter rather than a complete general decision procedure.For well-formed sliding-window CNF, SVI emptiness guarantees unsatisfiability; the formal bounds include O(|V1|·|V2|) and O(n2k2).
  • Formalisation and aligned structures: The Rocq formalisation proves TLS’s forward SVI directions, establishes complete bi-implication for aligned intersection, and contains zero admitted goals.The results cover pairs and systems of k structures, while aligned intersection supports verified OCaml extraction.
  • Correctness boundary: Formal counterexamples identify the exact failure boundary: weak CTF satisfaction may yield no cleared path, and clearing may destroy valid paths.The second failure arises because can adjoin requires forward compatibility whereas build paths all checks only backward compatibility; both are formally proved existential statements.
  • Constructive solving: The grouped sliding-window solver is constructive, extractable, and formally proved both sound and complete for disjoint variable ranges.It combines verified path finding, greedy assignment construction, and constructive merging of disjoint groups.
  • Complexity and extraction: 100n4+100, 2000n2+2000, and 3n2 + 7 are explicit formal cost bounds for generic clearing, the single-forbidden fragment, and SVI.The bounds come from induction in a Rocq cost model rather than asymptotic analysis alone; the single-forbidden case has constant-size DP-table behavior.
  • Positioning and limitations: TLS offers a geometric, auditable alternative to monolithic complete DPLL/CDCL solvers, trading completeness for an isolatable verified filter and exposing parallel structural decomposition.VFR targets harder structured instances outside the verified fragment, while TLS partitions formulas into independent CTFs based on variable overlap.

10 Conclusion

The paper establishes a formally verified Rocq foundation for Romanov’s Triplet Logic, clarifying when SVI is sound, when aligned intersection is complete, and how TLS supports sliding-window CNF decision procedures. VFR demonstrates an executable, reproducible implementation while remaining a research prototype rather than a practically competitive SAT solver.

  • Formalisation: The work presents the first formal verification of Romanov’s Triplet Logic in Rocq, complemented by empirical validation.The development formalises TLS and reports machine-checked results alongside experiments.
  • Correctness boundary: SVI is a correct one-sided filter: a joint satisfying set implies non-emptiness, but non-emptiness does not imply satisfiability for non-aligned tiers.The converse fails when common triplets occur between non-aligned tiers.
  • Correctness boundary: Aligned intersection is complete, with a non-empty full-length path if and only if a compatible joint satisfying set exists, including systems of k aligned structures.Theorem 4.3 establishes the single-structure bi-implication, while Theorem 4.4 extends it systemically.
  • Correctness boundary: The weak satisfies ctf predicate is incomplete for global path existence because it checks windows independently without enforcing agreement on overlapping bits.A formal counterexample shows that satisfies ctf can admit a locally consistent assignment while ctf-to-cts yields an empty structure; build paths all requires global compatibility.
  • Verified procedures: The clearing procedure terminates with a tight cts size measure and has a semantic fixed-point characterisation, while well-formed sliding-window CNF translation preserves satisfiability.The translation uses one forbidden triplet per clause and a greedy assignment to enforce consistency across overlapping variables.
  • Scope and performance: SVI is not a general preprocessor for random 3-SAT, but it is a complete decision procedure for clause-by-clause sliding-window CNF.The heuristic filter almost never returns False on random 3-SAT, whereas completeness is proved for windows containing exactly one clause.
  • Implementation and validation: VFR combines SVI with an exponential post-check and achieved 100% agreement with a brute-force oracle on random sliding-window instances with n ≤6.The Python pipeline was validated on SAT and UNSAT cases, including SVI false positives, and packaged in a reproducible Docker image.
  • Scope and limitations: VFR is a research prototype focused on verifiability rather than practical competitiveness, because its exponential post-check lacks modern CDCL features and efficient data structures.The paper identifies grouped-window decomposition, CDCL certificate integration, and Rocq-native proof production as next steps.

Formal Verification

The paper’s definitions, lemmas, and theorems are fully verified in Rocq 9.1.1, with a substantial development and no admitted goals.

  • Development scale: 23,000+ lines of Rocq code span seventeen files.The development comprises more than 23,000 lines across seventeen files.
  • Verification completeness: 427 lemmas and theorems are proved, with zero admitted goals.All definitions, lemmas, and theorems described in the paper have been formally verified.
  • Verification environment: The formalisation uses Rocq 9.1.1.The verification covers all definitions, lemmas, and theorems described in the paper.
  • Artifact availability: The source code is publicly available at DOI 10.5281/zenodo.20397950.The cited Zenodo record provides access to the Rocq development.
Loading 2608.18445v1…