論文の概要: Scalable Floating-Point Satisfiability via Staged Optimization

• arxiv url: http://arxiv.org/abs/2601.04492v1
• Date: Thu, 08 Jan 2026 01:51:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-09 17:01:52.977328
• Title: Scalable Floating-Point Satisfiability via Staged Optimization
• Title（参考訳）: 段階最適化によるスケーラブル浮動小数点満足度
• Authors: Yuanzhuo Zhang, Zhoulai Fu, Binoy Ravindran,
• Abstract要約: この研究は浮動小数点満足度を解くための新しいアプローチであるStageSATを導入している。 StageSATは、浮動小数点公式を、精度の向上の3段階における一連の最適化問題として再設定する。
• 参考スコア（独自算出の注目度）: 4.212975258164135
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This work introduces StageSAT, a new approach to solving floating-point satisfiability that bridges SMT solving with numerical optimization. StageSAT reframes a floating-point formula as a series of optimization problems in three stages of increasing precision. It begins with a fast, projection-aided descent objective to guide the search toward a feasible region, proceeding to bit-level accuracy with ULP$^2$ optimization and a final $n$-ULP lattice refinement. By construction, the final stage uses a representing function that is zero if and only if a candidate satisfies all constraints. Thus, when optimization drives the objective to zero, the resulting assignment is a valid solution, providing a built-in guarantee of soundness. To improve search, StageSAT introduces a partial monotone descent property on linear constraints via orthogonal projection, preventing the optimizer from stalling on flat or misleading landscapes. Critically, this solver requires no heavy bit-level reasoning or specialized abstractions; it treats complex arithmetic as a black-box, using runtime evaluations to navigate the input space. We implement StageSAT and evaluate it on extensive benchmarks, including SMT-COMP'25 suites and difficult cases from prior work. StageSAT proved more scalable and accurate than state-of-the-art optimization-based alternatives. It solved strictly more formulas than any competing solver under the same time budget, finding most satisfiable instances without producing spurious models. This amounts to 99.4% recall on satisfiable cases with 0% false SAT, exceeding the reliability of prior optimization-based solvers. StageSAT also delivered significant speedups (often 5--10$\times$) over traditional bit-precise SMT and numeric solvers. These results demonstrate that staged optimization significantly improves performance and correctness of floating-point satisfiability solving.
• Abstract（参考訳）: この研究は、SMTの解法を数値最適化で橋渡しする浮動小数点整合性(floating-point satisfiability)を解くための新しいアプローチであるStageSATを導入する。 StageSATは、浮動小数点公式を、精度の向上の3段階における一連の最適化問題として再設定する。 ULP$^2$最適化と最終的な$n$-ULP格子改質によってビットレベルの精度に進む。 構成により、最終段階は、候補がすべての制約を満たす場合に限って、ゼロである表現関数を使用する。 したがって、最適化が目的をゼロにすると、結果の割り当ては有効な解となり、音質の保証が組み込まれている。 探索を改善するため、StageSATは直交射影を介して線形制約に対する部分的な単調降下特性を導入し、最適化器が平坦な風景や誤解を招く風景で停止するのを防ぐ。 複雑な算術をブラックボックスとして扱い、実行時評価を用いて入力空間をナビゲートする。 われわれはStageSATを実装し,SMT-COMP'25スイートや先行作業の難しいケースなど,広範なベンチマークで評価する。 StageSATは最先端の最適化方式よりもスケーラブルで正確であることが証明された。 これは、同じ時間予算で競合する解法よりも厳密に多くの公式を解き、スプリアスモデルを作らずに最も満足できる例を見いだした。 これは、0%の偽SATを持つ満足なケースでの99.4%のリコールであり、以前の最適化ベースの解決器の信頼性を上回る。 また、StageSATは従来のビット精度のSMTや数値ソルバよりも大きなスピードアップ(しばしば5～10$\times$)を実現した。 これらの結果から, ステージ最適化は浮動小数点解法の性能と正確性を大幅に向上させることが示された。

関連論文リスト

• Advancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints [0.0]
  NP完全満足度問題 3-SAT の局所探索を導入,ベンチマークする。 私たちの建設は、WalkSATのような確立した従来のアプローチが、地元のミニマで立ち往生する傾向にあるという決定的な観察に基づいています。 我々は,N=15000までの様々な問題サイズを持つ3SATインスタンスをランダムに生成したサンプルを用いて,アルゴリズムを解析・ベンチマークする。
  論文  参考訳（メタデータ） (2025-06-18T18:00:01Z)
• Bayesian Optimization with Inexact Acquisition: Is Random Grid Search Sufficient? [12.182108642150103]
  我々は,不正確なBOアルゴリズムがいまだにサブ線形累積後悔を達成可能であることを示す。 このような知見により,ランダムグリッド探索の理論的正当化と数値検証の両立を図った。
  論文  参考訳（メタデータ） (2025-06-13T14:35:39Z)
• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。 本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。 我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
  論文  参考訳（メタデータ） (2024-10-11T18:20:08Z)
• Stochastic Zeroth-Order Optimization under Strongly Convexity and Lipschitz Hessian: Minimax Sample Complexity [59.75300530380427]
  本稿では,アルゴリズムが検索対象関数の雑音評価にのみアクセス可能な2次スムーズかつ強い凸関数を最適化する問題を考察する。 本研究は, ミニマックス単純後悔率について, 一致した上界と下界を発達させることにより, 初めて厳密な評価を行ったものである。
  論文  参考訳（メタデータ） (2024-06-28T02:56:22Z)
• qPOTS: Efficient batch multiobjective Bayesian optimization via Pareto optimal Thompson sampling [0.0]
  多目的最適化を解くためのサンプル効率のアプローチは、プロセス・オラクル・サロゲート(GP)とMOBOOTS$である。 我々はトンプソンサンプリング(TS)に基づくアプローチ(qtextttPOTS$)を提案する。 $qtextttPOTS$は、GP後部の安価な多目的最適化を進化的アプローチで解決する。
  論文  参考訳（メタデータ） (2023-10-24T12:35:15Z)
• Landscape Surrogate: Learning Decision Losses for Mathematical Optimization Under Partial Information [48.784330281177446]
  学習統合最適化の最近の研究は、最適化が部分的にのみ観察される場合や、専門家のチューニングなしに汎用性が不十分な環境では有望であることを示している。 本稿では,$fcirc mathbfg$の代替として,スムーズで学習可能なランドスケープサロゲートを提案する。 このサロゲートはニューラルネットワークによって学習可能で、$mathbfg$ソルバよりも高速に計算でき、トレーニング中に密度が高く滑らかな勾配を提供し、目に見えない最適化問題に一般化でき、交互最適化によって効率的に学習される。
  論文  参考訳（メタデータ） (2023-07-18T04:29:16Z)
• An Algorithm with Optimal Dimension-Dependence for Zero-Order Nonsmooth Nonconvex Stochastic Optimization [37.300102993926046]
  リプシッツの目的の滑らかな点も凸点も生成しない点の複雑さについて検討する。 私たちの分析は単純だが強力だ。 Goldstein-subdifferential set, これは最近の進歩を可能にする。 非滑らかな非最適化
  論文  参考訳（メタデータ） (2023-07-10T11:56:04Z)
• Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
  構成問題の複雑さを軽減するために,MSVR (Multi-block-probe Variance Reduced) という新しい手法を提案する。 本研究の結果は, 試料の複雑さの順序や強靭性への依存など, 様々な面で先行して改善された。
  論文  参考訳（メタデータ） (2022-07-18T12:03:26Z)
• A Momentum-Assisted Single-Timescale Stochastic Approximation Algorithm for Bilevel Optimization [112.59170319105971]
  問題に対処するための新しいアルゴリズム - Momentum- Single-timescale Approximation (MSTSA) を提案する。 MSTSAでは、低いレベルのサブプロブレムに対する不正確な解決策のため、反復でエラーを制御することができます。
  論文  参考訳（メタデータ） (2021-02-15T07:10:33Z)
• Convergence of adaptive algorithms for weakly convex constrained optimization [59.36386973876765]
  モローエンベロープの勾配のノルムに対して$mathcaltilde O(t-1/4)$収束率を証明する。 我々の分析では、最小バッチサイズが1ドル、定数が1位と2位のモーメントパラメータが1ドル、そしておそらくスムーズな最適化ドメインで機能する。
  論文  参考訳（メタデータ） (2020-06-11T17:43:19Z)
• Self-Directed Online Machine Learning for Topology Optimization [58.920693413667216]
  自己指向型オンライン学習最適化は、ディープニューラルネットワーク(DNN)と有限要素法(FEM)計算を統合している。 本アルゴリズムは, コンプライアンスの最小化, 流体構造最適化, 伝熱促進, トラス最適化の4種類の問題によって検証された。 その結果, 直接使用法と比較して計算時間を2～5桁削減し, 実験で検証した全ての最先端アルゴリズムより優れていた。
  論文  参考訳（メタデータ） (2020-02-04T20:00:28Z)

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

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