Negative Result and Reproducibility Artifact for a Pebbling-CDCL Policy Experiment

ABSTRACT This record is a negative result together with the artifact needed to checkit. The question was whether a fully specified deterministic CDCLtrajectory — chronological decisions, file-order propagation, first-UIPlearning, no restarts, no clause deletion — on pyramid pebblingcontradictions can support a policy-dependent complexity separation betweenthe decision orders pi_up and pi_down. It was not established. Theinvariant the attempt rested on is neither proved nor refuted, and theworking note records that state explicitly as a deadlock. What the recorddoes contain is the whole trail: encodings that collapsed at decision levelzero, legality predicates that turned out degenerate in both directions,measurements that were later superseded, claims that were withdrawn bytheir author, and the point at which the quantity being measured was foundto differ from the quantity defined in the literature — the paper's spacemeasure is a maximum over a whole pebbling trajectory, minimized overstrategies, whereas the predicate used here measures a singleconfiguration. Every reported number is produced by a command given infull, and the commands reproduce those numbers as printed. FULL DESCRIPTION This dataset investigates whether a precisely specified CDCL trajectory ongraph pebbling contradictions can support a claim of policy-dependentcomplexity separation for the decision orders pi_up and pi_down. Theexperiments considered pyramid formulas with chronological decisions,file-order propagation, first-UIP learning, no restarts, and no clausedeletion. The goal was to test the instrument and specific invariants, notto make any claim about P versus NP. The dataset includes experiment sources, serialized JSON results, completetraces, provenance checks, variable-identifier checks, human-readabletraces, and working research documentation. The investigated lines includethe original pebbling contradiction formulation, black-and-white statesemantics, a local CDCL tool on random 3-CNF instances, a correctedencoding with source/sink gadgets, and a separate front-predicatemeasurement line. Early tool defects were explicitly documented and corrected where possible.Two are load-bearing for reading the results. First, the flat encoding withunit source axioms collapsed at decision level zero: every run reached aroot-level conflict with zero decisions and zero learned clauses, so nolearning trajectory existed to measure. Second, an arbitrary-removallegality rule admitted all 2^|V| configurations and therefore rejectednothing; it was replaced by a temporary no-removal rule, which is itselfdegenerate in the opposite direction — it declares illegal theconfiguration consisting of a single pebble on the sink, that is, the goalposition of the pebble game. The corrected run on 12 instances (heights 2 to 4) reached UNSAT in everycase and contains 54 learned clauses, of which 9 are illegal projectionsunder that temporary no-removal predicate. This refutes the narrower lemma"every learned clause projection is legal" only for the corrected encoding,that predicate, and the tested height range; it is not a statement aboutthe pebble game's standard legality notion. A separate and broader front-predicate line covers 24 runs for heights 2 to7 and contains 153 learned clauses, of which 6 were rejected; the recordedpredicate is the height-derived occupied-front bound with threshold h-1,and it has colour_sensitive: false, so the sign of a literal is computedbut does not enter the verdict. A full black-and-white state-space searchat height 2 found all 729 configurations reachable from the empty one, soreachability alone rejects nothing under the standard four-move rules. Thelocal CDCL stress line contains 1200 samples and is reported as anexplicitly bounded experiment, not an asymptotic measurement. The checks confirm consistency among the JSON results, artifact copies,variable identifiers, and human-readable traces. Each command in theaccompanying write-up is given in full and can be run as printed. The required polynomial-exponential separation between the policies pi_upand pi_down was not established. The finite computational observationsreported here do not constitute a proof of the projection lemma, anasymptotic complexity separation, or any claim about P versus NP.