Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations
For researchers in SAT and constraint satisfaction, this work demonstrates cross-domain transfer from optimization to decision problems, but the results are preliminary and lack quantitative benchmarks.
The paper shows that foundational optimization embeddings pre-trained on MIP problems can be directly reused for unsupervised SAT tasks like instance clustering and distribution identification, without architectural changes or supervised fine-tuning.
Foundational optimization embeddings have recently emerged as powerful pre-trained representations for mixed-integer programming (MIP) problems. These embeddings were shown to enable cross-domain transfer and reduce 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 CNF formulas into the same bipartite constraint-variable graph representation used for MIPs. This allows direct reuse of the pre-trained embedding model without architectural changes or supervised fine-tuning. Our results show that these embeddings capture structural regularities in SAT instances and support unsupervised tasks such as instance clustering and distribution identification. We demonstrate, for the first time, that foundational optimization embeddings can transfer to constraint satisfaction domains. Our findings is a step toward a unified representational framework for both optimization and decision problems.