将优化嵌入迁移至SAT问题,实现无监督建模。
Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations

- 用与MIP相同的图结构表示CNF公式,复用预训练嵌入模型。
- 嵌入能捕捉SAT实例结构规律,支持聚类与分布识别。
- 首次实现优化嵌入向决策问题的跨域迁移,适合算法研究者。
近年来,基础优化嵌入作为混合整数规划(MIP)问题的强大预训练表示被提出,可实现跨领域迁移并减少对求解器标签的依赖。本文研究此类表示是否能推广到决策问题,聚焦布尔满足性(SAT)。通过将合取范式(CNF)公式映射为与MIP相同的二分约束-变量图结构,我们直接复用预训练嵌入模型,无需架构修改或有监督微调。结果表明,这些嵌入能捕捉SAT实例的结构规律,支持无监督任务如实例聚类和分布识别。这是首次证明基础优化嵌入可迁移至约束满足领域,迈向优化与决策问题统一表征框架的重要一步。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。