論文の概要: Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic
- arxiv url: http://arxiv.org/abs/2603.22877v1
- Date: Tue, 24 Mar 2026 07:22:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-25 19:53:37.354922
- Title: Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic
- Title（参考訳）: リニアリアル算術に基づく満足度モード理論の連続最適化
- Authors: Yunuo Cen, Daniel Ebler, Xuanyao Fong,
- Abstract要約: 本稿では,FourierSMTを拡張性と並列性の高い連続変数最適化フレームワークとして導入する。
このフレームワークは、最大10,000変数と70万の制約で大規模なスケジューリングと配置の問題に対してベンチマークされており、8倍のスピードアップを実現している。
- 参考スコア（独自算出の注目度）: 2.8037951156321377
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Efficient solutions for satisfiability modulo theories (SMT) are integral in industrial applications such as hardware verification and design automation. Existing approaches are predominantly based on conflict-driven clause learning, which is structurally difficult to parallelize and therefore scales poorly. In this work, we introduce FourierSMT as a scalable and highly parallelizable continuous-variable optimization framework for SMT. We generalize the Walsh-Fourier expansion (WFE), called extended WFE (xWFE), from the Boolean domain to a mixed Boolean-real domain, which allows the use of gradient methods for SMT. This addresses the challenge of finding satisfying variable assignments to high-arity constraints by local updates of discrete variables. To reduce the evaluation complexity of xWFE, we present the extended binary decision diagram (xBDD) and map the constraints from xWFE to xBDDs. We then show that sampling the circuit-output probability (COP) of xBDDs under randomized rounding is equivalent to the expectation value of the xWFEs. This allows for efficient computation of the constraints. We show that the reduced problem is guaranteed to converge and preserves satisfiability, ensuring the soundness of the solutions. The framework is benchmarked for large-scale scheduling and placement problems with up to 10,000 variables and 700,000 constraints, achieving 8-fold speedups compared to state-of-the-art SMT solvers. These results pave the way for GPU-based optimization of SMTs with continuous systems.
- Abstract（参考訳）: 満足度モジュロ理論(SMT)の効率的な解は、ハードウェア検証や設計自動化といった産業応用において不可欠である。
既存のアプローチは、主にコンフリクト駆動の節学習に基づいており、これは構造的に並列化が難しいため、スケールが不十分である。
本稿では,SMTのスケーラブルかつ並列化性の高い連続変数最適化フレームワークとしてFourierSMTを紹介する。
We generalize the Walsh-Fourier expansion (WFE) called extended WFE (xWFE) from the Boolean domain to a mixed Boolean-real domain。
これは、離散変数の局所的な更新による高純度制約に対する変数の割り当てを満たすという課題に対処する。
xWFEの評価複雑性を低減するため、拡張バイナリ決定図(xBDD)を示し、制約をxWFEからxBDDにマッピングする。
次に、ランダムなラウンドリングの下でxBDDの回路出力確率(COP)をサンプリングすることは、xWFEの期待値と等価であることを示す。
これにより、制約の効率的な計算が可能になる。
低減された問題は収束することが保証され、満足度を保ち、解の健全性を保証する。
このフレームワークは、最大10,000変数と70,000の制約を持つ大規模スケジューリングおよび配置問題に対してベンチマークされており、最先端のSMTソルバと比較して8倍のスピードアップを実現している。
これらの結果は、連続システムによるSMTのGPUベースの最適化の道を開くものである。
関連論文リスト
- DRAFTO: Decoupled Reduced-space and Adaptive Feasibility-repair Trajectory Optimization for Robotic Manipulators [4.0407133618465005]
本稿では、トラジェクトリ最適化のための新しいアルゴリズム、Decoupled Reduced-spaceとAdaptive Feasibility-Repair Trajectory Optimization (DRAFTO)を提案する。
連立限界実現性を扱いながら繰り返し制約された最適化の回数を減らすため、最適化を低空間ガウスニュートン(Gass-Newton, GN)降下に分離する。
CHOMP, TrajOpt, GPMP2, FACTOなどの最適化型プランナに対するベンチマークテストの結果, 様々なシナリオやタスクにおいて高い効率性と信頼性が検証された。
論文 参考訳（メタデータ） (2026-03-10T20:24:42Z) - The Theory and Practice of MAP Inference over Non-Convex Constraints [11.058494098615576]
安全クリティカルな設定では、確率的MLシステムは代数的制約の下で予測を行う必要がある。
これにより、制約された最大値 (MAP) の予測を効率的にかつ確実に行うことができる。
この抽出可能なフラグメントに対して,スケーラブルなメッセージパッシングアルゴリズムを考案する。
そこで我々は,領域を凸可能な領域に分割する一般的なMAP戦略を考案した。
論文 参考訳（メタデータ） (2026-02-09T14:05:58Z) - Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。
提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
論文 参考訳（メタデータ） (2025-10-02T15:15:50Z) - PT$^2$-LLM: Post-Training Ternarization for Large Language Models [52.4629647715623]
大きな言語モデル(LLM)は、様々なタスクにまたがる印象的な機能を示しているが、その大きなメモリと計算能力は、デプロイメントを妨げている。
PT$2$-LLMを提案する。
その中核は2段精製パイプラインを備えた非対称3次量子化器である。
論文 参考訳（メタデータ） (2025-09-27T03:01:48Z) - FMIP: Joint Continuous-Integer Flow For Mixed-Integer Linear Programming [52.52020895303244]
Mixed-Integer Linear Programming (MILP)は、複雑な意思決定問題の基本的なツールである。
混合整数線形計画法(FMIP)のための連立連続整数フローを提案する。これはMILPソリューションにおける整数変数と連続変数の共分散をモデル化する最初の生成フレームワークである。
FMIPは任意のバックボーンネットワークや様々なダウンストリームソルバと完全に互換性があり、現実世界のMILPアプリケーションにも適している。
論文 参考訳（メタデータ） (2025-07-31T10:03:30Z) - Decentralized Nonconvex Composite Federated Learning with Gradient Tracking and Momentum [78.27945336558987]
分散サーバ(DFL)はクライアント・クライアント・アーキテクチャへの依存をなくす。
非滑らかな正規化はしばしば機械学習タスクに組み込まれる。
本稿では,これらの問題を解決する新しいDNCFLアルゴリズムを提案する。
論文 参考訳（メタデータ） (2025-04-17T08:32:25Z) - Optimizing LLM Inference: Fluid-Guided Online Scheduling with Memory Constraints [14.341123057506827]
大規模言語モデル(LLM)は、今日のアプリケーションでは必須であるが、推論手順は重要な計算資源を必要とする。
本稿では,多段階オンラインスケジューリング問題としてLLM推論最適化を定式化する。
我々は,アルゴリズム設計をガイドするトラクタブルなベンチマークを提供するために,流体力学近似を開発した。
論文 参考訳（メタデータ） (2025-04-15T16:00:21Z) - Taming Flow Matching with Unbalanced Optimal Transport into Fast Pansharpening [10.23957420290553]
本稿では,一段階の高品位パンシャーピングを実現するための最適輸送フローマッチングフレームワークを提案する。
OTFMフレームワークは、パンシャーピング制約の厳格な遵守を維持しつつ、シミュレーション不要なトレーニングとシングルステップ推論を可能にする。
論文 参考訳（メタデータ） (2025-03-19T08:10:49Z) - Efficiently Training Deep-Learning Parametric Policies using Lagrangian Duality [55.06411438416805]
制約付きマルコフ決定プロセス(CMDP)は、多くの高度な応用において重要である。
本稿では,パラメトリックアクターポリシーを効率的に訓練するための2段階深度決定規則(TS-DDR)を提案する。
現状の手法と比較して, 解の質を高め, 数桁の計算時間を削減できることが示されている。
論文 参考訳（メタデータ） (2024-05-23T18:19:47Z) - Stochastic Inexact Augmented Lagrangian Method for Nonconvex Expectation
Constrained Optimization [88.0031283949404]
多くの実世界の問題は複雑な非機能的制約を持ち、多くのデータポイントを使用する。
提案手法は,従来最もよく知られた結果で既存手法よりも優れた性能を示す。
論文 参考訳（メタデータ） (2022-12-19T14:48:54Z) - Federated Expectation Maximization with heterogeneity mitigation and
variance reduction [0.0]
本稿では、潜在変数モデルに対する期待最大化(EM)アルゴリズムの最初の拡張であるFedEMを紹介する。
通信の複雑さを軽減するため、FedEMは十分なデータ統計を適切に定義した。
その結果,生物多様性モニタリングに欠落した値の計算処理を応用した理論的知見が得られた。
論文 参考訳（メタデータ） (2021-11-03T09:14:34Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。