論文の概要: How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization

• arxiv url: http://arxiv.org/abs/2411.07955v1
• Date: Tue, 12 Nov 2024 17:31:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-13 13:21:33.857996
• Title: How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization
• Title（参考訳）: 短所, 短所, 短所, 短所の発見方法: 分枝・境界法による長さ最小化法
• Authors: Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, Mathijs de Weerdt, Emir Demirović,
• Abstract要約: 本稿では,最短解法を見つけるための分岐結合アルゴリズムを提案する。 この表現はすべての置換対称性を破り、それによって最先端の対称性の破れを改善する。 本実験により, SATコンペティション2002の事例では30～60%, 小型合成式では25～50%の短縮が可能であることが示唆された。
• 参考スコア（独自算出の注目度）: 1.4796543791607086
• License:
• Abstract: Modern software for propositional satisfiability problems gives a powerful automated reasoning toolkit, capable of outputting not only a satisfiable/unsatisfiable signal but also a justification of unsatisfiability in the form of resolution proof (or a more expressive proof), which is commonly used for verification purposes. Empirically, modern SAT solvers produce relatively short proofs, however, there are no inherent guarantees that these proofs cannot be significantly reduced. This paper proposes a novel branch-and-bound algorithm for finding the shortest resolution proofs; to this end, we introduce a layer list representation of proofs that groups clauses by their level of indirection. As we show, this representation breaks all permutational symmetries, thereby improving upon the state-of-the-art symmetry-breaking and informing the design of a novel workflow for proof minimization. In addition to that, we design pruning procedures that reason on proof length lower bound, clause subsumption, and dominance. Our experiments suggest that the proofs from state-of-the-art solvers could be shortened by 30-60% on the instances from SAT Competition 2002 and by 25-50% on small synthetic formulas. When treated as an algorithm for finding the shortest proof, our approach solves twice as many instances as the previous work based on SAT solving and reduces the time to optimality by orders of magnitude for the instances solved by both approaches.
• Abstract（参考訳）: 命題的満足度問題のための現代のソフトウェアは強力な自動推論ツールキットを提供し、満足できる/不満足な信号だけでなく、検証目的によく用いられる解決証明(あるいはより表現力のある証明)の形で不満足性の正当化を出力することができる。 経験的に、現代のSATソルバは比較的短い証明を生成するが、これらの証明を著しく還元できないという固有の保証はない。 本稿では,最短解法を見つけるための分岐結合アルゴリズムを提案する。 示すように、この表現はすべての置換対称性を破り、最先端の対称性を破り、証明最小化のための新しいワークフローの設計を知らせる。 それに加えて、証明長の下限、節の置換、支配を理由とするプルーニング手順を設計する。 本実験により, SATコンペティション2002の事例では30～60%, 小型合成式では25～50%の短縮が可能であることが示唆された。 最短証明を求めるアルゴリズムとして扱われる場合,本手法はSATの解法に基づく従来の2倍の時間を解き,両手法が解いたインスタンスの次数による最適化時間を短縮する。

関連論文リスト

• ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
  リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。 我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
  論文  参考訳（メタデータ） (2024-10-07T05:14:18Z)
• Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
  満足度に基づく自動推論は、ソフトウェア工学において複雑なソフトウェアを検証するのに成功している。 我々は、FOL*不満足な結果の正しさを検証するという課題に取り組む。 我々は,不満足の原因を説明するために,証明に基づく診断法を開発した。
  論文  参考訳（メタデータ） (2024-09-13T22:25:58Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• Forward LTLf Synthesis: DPLL At Work [1.370633147306388]
  有限トレース(LTLf)上での線形時間論理の合成のための新しいAND-ORグラフ探索フレームワークを提案する。 このようなフレームワーク内では、Davis-Putnam-Logemann-Loveland (DPLL)アルゴリズムにインスパイアされたプロシージャを考案し、次に利用可能なエージェント環境の動きを生成する。 また,状態公式の構文的等価性に基づく探索ノードの等価性チェックも提案する。
  論文  参考訳（メタデータ） (2023-02-27T14:33:50Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
  凸最適化における総和係数法に着想を得て,広範な分岐関数を持つネットワーク上での検証クエリを解析するための新しい手法を提案する。 標準ケース分析に基づく完全探索手順の拡張は、各検索状態で実行される凸手順をDeepSoIに置き換えることによって達成できる。
  論文  参考訳（メタデータ） (2022-03-19T15:05:09Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。 8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
  論文  参考訳（メタデータ） (2020-06-05T10:56:52Z)
• Understanding the QuickXPlain Algorithm: Simple Explanation and Formal Proof [0.0]
  本稿では,Ulrich Junker の QuickXPlain アルゴリズムの正当性を示す。 他のアルゴリズムを証明するためのガイダンスとして使用できる。 また、QuickXPlainによって計算された結果に依存するシステムの"ギャップレス"な正しさを提供する可能性も提供する。
  論文  参考訳（メタデータ） (2020-01-07T01:37:41Z)
• The Simulator: Understanding Adaptive Sampling in the Moderate-Confidence Regime [52.38455827779212]
  エミュレータと呼ばれる適応サンプリングを解析するための新しい手法を提案する。 適切なログファクタを組み込んだトップk問題の最初のインスタンスベースの下位境界を証明します。 我々の新しい分析は、後者の問題に対するこの種の最初のエミュレータであるベストアームとトップkの識別に、シンプルでほぼ最適であることを示した。
  論文  参考訳（メタデータ） (2017-02-16T23:42:02Z)

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

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