Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations

Foundational optimization embeddings, such as FORGE, have recently emerged as powerful pre-trained representations for mixed-integer programming (MIP) problems. Prior work showed these embeddings can transfer across optimization problem domains while reducing reliance on solver-generated labels. In this work, we investigate whether such representations generalize beyond optimization to decision problems, focusing on Boolean satisfiability (SAT). We adapt the foundational optimization architecture to SAT by mapping conjunctive normal form (CNF) formulas into the same bipartite constraint–variable graph representation used for MIPs. This enables us to study both direct transfer of MIP-pretrained representations and FORGE-SAT, a variant of the same architecture pretrained directly on SAT instances. Our results show that these embeddings capture structural regularities in SAT instances and support unsupervised tasks such as instance clustering and distribution identification. Beyond clustering, we analyze what the learned discrete codewords encode by generating semantic descriptions, validating them on held-out nodes, and testing whether the same interpretations transfer across SAT difficulty levels. We further evaluate the downstream utility of these representations for satisfiability prediction under held-out distribution shift, showing that frozen FORGE-SAT representations provide useful task-relevant signal. Our findings are a step toward a unified representational framework across optimization and decision problems.