電腦科學與資訊工程科 Computer Science & Information Engineering
190002 Taiwan
確定性導向之可循跡核心演算法 Deterministic Switching to Trackable Core
This study proposes the Deterministic Switching to Trackable Core (DSTC) algorithm, a deterministic framework designed to address the Boolean Satisfiability Problem (SAT). We introduce a five-dimensional potential function, \Phi (comprising clause count, length weight, co-occurrence, polarity bias, and time steps), to model the SAT solving process as a potential descent dynamical system. By partitioning the problem space into distinct phases—Dense, Heavy, and Sparse-Light—we analyze the systematic reduction of \Phi in non-terminal states. Our theoretical framework incorporates three key innovations: (1) Literal Triplet Graph theory, which models 3-literal clauses through 3D hypergraph structures; (2) a dual-assignment strategy that leverages synergistic gains to facilitate variable flips; and (3) the Penetration Theorem, which demonstrates how assignments can propagate from low-coupling regions to high-coupling areas via ""third vertices."" Preliminary complexity analysis suggests that the DSTC algorithm terminates within O\left(n^3m\log{n}\log{m}\right) steps, yielding either a satisfying assignment or a DRAT-verifiable UNSAT proof. This work offers a novel methodological perspective on SAT complexity and bridges theoretical potential-based dynamics with practical solver heuristics.