用无约束优化解决混合型逻辑问题，提升求解效率。
Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
- 用惩罚项替代盒约束，实现无约束连续优化求解
- 实验证明Adam等优化器在混合基准上表现更优
- 适合对混合约束求解感兴趣的算法与系统研究者
布尔可满足性（SAT）问题在组合优化、软件验证、密码学和机器学习中具有核心地位。尽管当前顶尖求解器在合取范式（CNF）公式上表现高效，但许多应用需要处理非CNF（混合）约束，如XOR、基数和非全等约束。近期工作采用多项式表示来建模这些混合约束，但依赖于盒约束，限制了强大无约束优化器的使用。本文提出基于惩罚项的无约束连续优化公式来求解混合SAT问题。我们提供了理论分析，说明何时需引入惩罚项，并通过实验证明，无约束优化器（如Adam）在混合基准测试中可显著提升SAT求解性能。结果表明，将连续优化与基于机器学习的方法结合，有望实现高效的混合SAT求解。
原文摘要 · Abstract (English)
The Boolean satisfiability (SAT) problem lies at the core of many applications in combinatorial optimization, software verification, cryptography, and machine learning. While state-of-the-art solvers have demonstrated high efficiency in handling conjunctive normal form (CNF) formulas, numerous applications require non-CNF (hybrid) constraints, such as XOR, cardinality, and Not-All-Equal constraints. Recent work leverages polynomial representations to represent such hybrid constraints, but it relies on box constraints that can limit the use of powerful unconstrained optimizers. In this paper, we propose unconstrained continuous optimization formulations for hybrid SAT solving by penalty terms. We provide theoretical insights into when these penalty terms are necessary and demonstrate empirically that unconstrained optimizers (e.g., Adam) can enhance SAT solving on hybrid benchmarks. Our results highlight the potential of combining continuous optimization and machine-learning-based methods for effective hybrid SAT solving.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。