Structured and Compact: A Novel Encoding and Enhancement Paradigm for ML-based SAT Solving

Machine Learning for SAT (ML4SAT) offers a data-driven alternative to traditional solvers.However, existing flat-vector paradigms face scalability bottlenecks, feature redundancy, and struggle to exploit the intrinsic logical structures of clauses.To address these deficiencies, a novel encoding and enhancement paradigm is proposed, comprising: (1) a lightweight Prime-Product Clause Encoding (PPCE) scheme leveraging unique prime factorization for mathematically lossless dimensionality compression;(2) a Structure-Aware Enhancement (SAE) module incorporating a localized subnetwork (ClauseNet) to better capture intraclause logic; and (3) a controlled benchmark evaluating four canonical models-Logistic Regression, Support Vector Machine, Multi-Layer Perceptron, and Transformer-under unified variables.Empirical results on two large-scale CNF datasets (183k and 480k samples) reveal high-dimensional semi-sparsity (S ranging from 73.81% to 75.20%).PPCE reduces feature dimensionality by 75%, while the SAE module can improve accuracy across models without inference overhead.These findings validate specialized encoding and structural modules in ML4SAT, providing practical, data-driven selection guidelines for exploring accuracy-efficiency trade-offs in industrial formal verification.