Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations

TL;DR

This paper demonstrates that foundational optimization embeddings can be adapted to SAT problems, enabling unsupervised analysis and transfer across decision and optimization domains.

Contribution

It introduces a method to reuse pre-trained optimization embeddings for SAT, showing their effectiveness without architectural changes or fine-tuning.

Findings

Embeddings capture structural regularities in SAT instances.

Supports unsupervised tasks like clustering and distribution identification.

First demonstration of transfer from optimization to decision problems.

Abstract

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.