論文の概要: Orbitopal Fixing in SAT

• arxiv url: http://arxiv.org/abs/2601.16855v1
• Date: Fri, 23 Jan 2026 16:01:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-26 14:27:27.755648
• Title: Orbitopal Fixing in SAT
• Title（参考訳）: SATにおける眼窩固定
• Authors: Markus Anders, Cayden Codel, Marijn J. H. Heule,
• Abstract要約: 本稿では,軌道上固定に基づく実用的な静的対称性破壊手法を提案する。 提案手法は,対称性に富むベンチマークにおいて,非無視回帰を伴う一貫した高速化を実現する。
• 参考スコア（独自算出の注目度）: 0.688204255655161
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Despite their sophisticated heuristics, boolean satisfiability (SAT) solvers are still vulnerable to symmetry, causing them to visit search regions that are symmetric to ones already explored. While symmetry handling is routine in other solving paradigms, integrating it into state-of-the-art proof-producing SAT solvers is difficult: added reasoning must be fast, non-interfering with solver heuristics, and compatible with formal proof logging. To address these issues, we present a practical static symmetry breaking approach based on orbitopal fixing, a technique adapted from mixed-integer programming. Our approach adds only unit clauses, which minimizes downstream slowdowns, and it emits succinct proof certificates in the substitution redundancy proof system. Implemented in the satsuma tool, our methods deliver consistent speedups on symmetry-rich benchmarks with negligible regressions elsewhere.
• Abstract（参考訳）: 洗練されたヒューリスティック技術にもかかわらず、ブール整合性 (SAT) の解法はまだ対称性に弱いため、既に探索されたものと対称な探索領域を訪れることになる。 他の解決パラダイムでは対称性のハンドリングは日常的であるが、それを最先端の証明生成SATソルバに統合することは難しい: 追加の推論は高速で、ソルバヒューリスティックスと非干渉し、形式的な証明ロギングと互換性がある。 これらの問題に対処するため、我々は、混合整数計画法に適応した軌道修正に基づく実用的な静的対称性破壊手法を提案する。 提案手法では,下流のスローダウンを最小限に抑える単位節のみを追加し,置換冗長性証明システムに簡潔な証明証明書を出力する。 サスマツールで実装された我々の手法は、他の場所では無視できない回帰を伴う対称性に富んだベンチマークで一貫したスピードアップを提供する。

関連論文リスト

• Verifying Closed-Loop Contractivity of Learning-Based Controllers via Partitioning [52.23804865017831]
  本稿では,ニューラルネットワークによるパラメータ化を行う非線形制御系における閉ループ収縮の検証問題に対処する。 我々は、対称メッツラー行列の優越的固有値が非正であることを確かめるために、閉ループの縮約性に対するトラクタブルでスケーラブルな十分条件を導出する。
  論文  参考訳（メタデータ） (2025-12-01T23:06:56Z)
• Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables [11.274339621648565]
  バグに対処する最も成功したアプローチは、標準フォーマットで正確性の数学的証明を出力するように、ソルバを認証することである。 これは証明の中で対称性の推論を正当化する必要があるが、このための効率的な方法の開発は長年のオープン・チャレンジのままである。 証明ロギングの実験を行い,SAT対称性の破れをチェックすることによって,理論と実践の両面でのオーダー・オブ・マグニチュード・スピードアップにつながることを示す。
  論文  参考訳（メタデータ） (2025-11-20T18:43:05Z)
• Exploiting Symmetries in MUS Computation (Extended version) [11.266189935383476]
  eXplainable Constraint Solving (XCS) では、満足できない制約の集合から最小不満足な部分集合(MUS)を抽出することが一般的である。 MUSの発見は、高度に対称的な問題に対して計算コストがかかる。 本稿では、既存の対称性処理技術からインスピレーションを得て、よく知られたMUS計算手法を適用して仕様の対称性を利用する。
  論文  参考訳（メタデータ） (2024-12-18T08:34:32Z)
• How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization [1.4796543791607086]
  本稿では,最短解法を見つけるための分岐結合アルゴリズムを提案する。 この表現はすべての置換対称性を破り、それによって最先端の対称性の破れを改善する。 本実験により, SATコンペティション2002の事例では30～60%, 小型合成式では25～50%の短縮が可能であることが示唆された。
  論文  参考訳（メタデータ） (2024-11-12T17:31:35Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。 そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
  論文  参考訳（メタデータ） (2022-10-04T09:19:13Z)
• Certified Symmetry and Dominance Breaking for Combinatorial Optimisation [13.333957453318744]
  本研究では,対称性と支配的破壊が容易に表現可能な最適化問題に対する認証手法を開発した。 提案手法は,提案手法が幅広い問題に適用可能であることを示す概念実証として,最大斜め解法と制約法に適用する。
  論文  参考訳（メタデータ） (2022-03-23T08:45:35Z)
• E-detectors: a nonparametric framework for sequential change detection [86.15115654324488]
  逐次的変化検出のための基本的かつ汎用的なフレームワークを開発する。 私たちの手順は、平均走行距離のクリーンで無症状な境界が伴います。 統計的および計算効率の両方を達成するために,これらの混合物を設計する方法を示す。
  論文  参考訳（メタデータ） (2022-03-07T17:25:02Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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