論文の概要: Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization

• arxiv url: http://arxiv.org/abs/2506.00674v1
• Date: Sat, 31 May 2025 18:58:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-04 21:47:33.477555
• Title: Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
• Title（参考訳）: 箱から考える:制約のない連続最適化によるハイブリッドSAT解決
• Authors: Zhiwei Zhang, Samy Wu Fung, Anastasios Kyrillidis, Stanley Osher, Moshe Y. Vardi,
• Abstract要約: ペナルティ項によるハイブリッドSAT問題の非制約連続最適化を提案する。 本結果は,効率的なハイブリッドSAT解決のための連続最適化と機械学習に基づく手法を組み合わせる可能性を強調した。
• 参考スコア（独自算出の注目度）: 25.30924681709063
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.
• Abstract（参考訳）: ブール満足度(SAT)問題は、組合せ最適化、ソフトウェア検証、暗号、機械学習における多くのアプリケーションの中核にある。 最先端の解法は、共役正規形(CNF)の公式を扱う上で高い効率性を示しているが、多くの応用では、XOR、濃度、不等式といった非CNF(ハイブリド)制約を必要とする。 最近の研究は、このようなハイブリッドな制約を表現するために多項式表現を利用するが、強力な制約のないオプティマイザの使用を制限することができるボックス制約に依存している。 本稿では,ハイブリッドSAT問題に対するペナルティ項による非拘束型連続最適化法を提案する。 これらのペナルティ項がいつ必要かの理論的な洞察を与え、制約のない最適化器(例えばAdam)がハイブリッドベンチマーク上でSATの解法を強化することを実証的に示す。 本結果は,効率的なハイブリッドSAT解決のための連続最適化と機械学習に基づく手法を組み合わせる可能性を強調した。

関連論文リスト

• Efficient QAOA Architecture for Solving Multi-Constrained Optimization Problems [3.757262277494307]
  本稿では,量子近似最適化アンサッツのための制約符号化手法の新たな組み合わせを提案する。 ワンホット制約は、検索空間を実現可能なサブ空間に自然に制限する$XY$-mixerによって強制される。 確立されたQUBOの定式化と組み合わせた手法をベンチマークし、最適解をサンプリングする確率と解の質を向上した。
  論文  参考訳（メタデータ） (2025-06-03T17:46:53Z)
• A Novel Unified Parametric Assumption for Nonconvex Optimization [53.943470475510196]
  非最適化は機械学習の中心であるが、一般の非凸性は弱い収束を保証するため、他方に比べて悲観的すぎる。 非凸アルゴリズムに新しい統一仮定を導入する。
  論文  参考訳（メタデータ） (2025-02-17T21:25:31Z)
• No-Regret Constrained Bayesian Optimization of Noisy and Expensive Hybrid Models using Differentiable Quantile Function Approximations [0.0]
  Constrained Upper Quantile Bound (CUQB) は、制約近似を避けるための概念的に単純で決定論的アプローチである。 CUQBは制約のある場合と制約のない場合の両方において従来のベイズ最適化よりも著しく優れることを示す。
  論文  参考訳（メタデータ） (2023-05-05T19:57:36Z)
• Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints [39.96302127802424]
  量子コンピューティングで発生するハイブリッドブール制約の新しい応用について検討する。 この問題は、エッジカラーグラフにおける制約付き完全マッチングに関連している。 本稿では,ハイブリッド制約による制約マッチング問題の直接符号化が不十分であり,特殊な手法が依然として必要であることを示す。
  論文  参考訳（メタデータ） (2023-01-24T06:14:24Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。 これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。 本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
  論文  参考訳（メタデータ） (2022-11-16T18:59:54Z)
• Learning Proximal Operators to Discover Multiple Optima [66.98045013486794]
  非家族問題における近位演算子を学習するためのエンドツーエンド手法を提案する。 本手法は,弱い目的と穏やかな条件下では,世界規模で収束することを示す。
  論文  参考訳（メタデータ） (2022-01-28T05:53:28Z)
• Multi-Objective Constrained Optimization for Energy Applications via Tree Ensembles [55.23285485923913]
  エネルギーシステムの最適化問題は、強い非線形系の挙動と複数の競合する目的のために複雑である。 場合によっては、提案された最適解は、物理的性質や安全クリティカルな操作条件に関連する明示的な入力制約に従う必要がある。 本稿では,ブラックボックス問題に対する制約付き多目的最適化のためのツリーアンサンブルを用いた新しいデータ駆動戦略を提案する。
  論文  参考訳（メタデータ） (2021-11-04T20:18:55Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。