DRCC Runtime Analysis (DRCC-V3.1)

Abstract

This work presents DRCC (Dimensional Reduction via Controlled Combinatorics), a structural preprocessing and reconstruction framework for satisfiability problems represented in conjunctive normal form (CNF). DRCC transforms an input formula into a solver-facing representation through controlled reconstruction steps governed by a processing order and a task-specific reconstruction rule. The framework separates structural reduction from subsequent solver search and makes the relevant assumptions explicit. The formal development distinguishes the elementary reduction maps from their composition and introduces two complementary structural measures. DRCC width measures the maximum active structural interface that must be retained during processing, whereas DRCC work counts the reachable partial reconstructions across all stages. These quantities describe structural and combinatorial properties; they are not themselves machine-level runtime measures. The Pigeonhole Principle family serves as a concrete example. Under the specified PHP encoding, pigeon-block processing order, and deterministic reconstruction rule, the analysis yields quadratic DRCC width and linear DRCC work. The resulting reconstruction path exposes the contradiction in the reduced representation, allowing the downstream solver to detect unsatisfiability without branching on the tested reduced instances. The experimental evaluation compares the original and DRCC-augmented representations using a reference DPLL solver, MiniSat 2.2, and Glucose 3. It reports measured runtime, solver statistics, and a prospective test of an empirical runtime model. The observed advantages are specific to the tested benchmark family, solver versions, implementation, hardware, and measurement configuration. Empirical fourth-power runtime behavior is reported only as a phenomenological fit over the evaluated interval, not as a general asymptotic complexity law for DRCC. Classical resolution and DPLL lower bounds for the original PHP representation are therefore not claimed to be refuted.

Keywords