A Common Type Framework for 2-SAT and 3-SAT

At present, the 2-SAT and 3-SAT problems in n Boolean variables and m clauses straddle a computational gulf. The 2-SAT problem has worst-case polynomial deterministic computational costs of O(n + m), [APT79]. The 3-SAT problem has been analyzed as having exponential deterministic computational costs of O*(1.32793n ) [LIU18]. Here, we do not weigh in on that apparent gulf. Instead, we create and analyze structures of k-SAT generally, for fixed kSAT with k in (2, 3). Our motivation is to discern common k-based types and structures for 2-SAT and 3-SAT, which we build bottom-up. To do so we propose a common set of types to describe 2-SAT and 3-SAT clauses, k-ary assignments to clauses, clause pairs, and recursively composed triangular types over m in (3, 4) clauses, called T3 and T4 types. We use those features to describe a new measure of problem hardness, propose finite state automata of clauses, and give a computationally feasible algorithm to enumerate and evaluate satisfiability of all 2-SAT and 3- SAT problems in m in (3, 4) clauses, each of which is a T3 or T4 triangle type or kernel. We show how each k-SAT problem in m clauses is a Tm triangle, recursively composed of overlapping sub-triangles and composed of types of T4 triangles. Based on those properties, we analyze the clique-structure and composition of such triangles. Finally, we describe a set of problems that are structurally between 2-SAT and 3-SAT. One goals are to illuminate k-based similarities and differences of 2-SAT and 3-SAT and to provide a common domain under which machine learning may analyze 2-SAT and 3-SAT problems, e.g., to leverage 2-SAT solvability to discern 3-SAT algorithmic approaches or structures. Recent advances on hard problems suggest benefits of that approach [see ALON26]