論文の概要: Orthologic for SAT Solving

• arxiv url: http://arxiv.org/abs/2605.16421v1
• Date: Thu, 14 May 2026 13:05:57 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-19 17:57:46.391541
• Title: Orthologic for SAT Solving
• Title（参考訳）: SATソルビングのオーソロジー
• Authors: Vladislas de Haldat, Simon Guilloud, Viktor Kunčak,
• Abstract要約: 我々は,任意の式に対して,等式$leftrightarrow MathrmNF_mathrmOL()$はタウトロジーである,という観測に基づいて,SATベンチマークの族を紹介する。 本研究では, オーソロジー正規化を前処理ステップとして用いることで, SAT解決時間を短縮できることを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: We present a new algorithm for deciding formula entailment in orthologic (a sound approximation of classical logic) that avoids the costly preprocessing phase of prior implementations while retaining the same $\mathcal{O}(n^2(1+|A|))$ worst-case complexity. We then introduce a family of synthetic SAT benchmarks based on the observation that, for any formula $φ$, the equivalence $φ\leftrightarrow \mathrm{NF}_{\mathrm{OL}}(φ)$ is a tautology whose Tseitin encoding yields unsatisfiable instances that are hard for state-of-the-art SAT solvers yet have short orthologic proofs. Applied to EPFL arithmetic circuits, our algorithm solves these instances efficiently while Kissat times out on a significant fraction. Finally, we show that using orthologic normalization as a preprocessing step can improve SAT solving time on some hard problems.
• Abstract（参考訳）: 本稿では,従来の実装のコストのかかる前処理フェーズを回避し,同じ$\mathcal{O}(n^2(1+|A|))=最悪の場合の複雑性を保ちながら,論理学(古典論理の音響近似)における公式の包含を決定するアルゴリズムを提案する。 次に、任意の式$φ$に対して、同値$φ\leftrightarrow \mathrm{NF}_{\mathrm{OL}}(φ)$は、Tseitinエンコーディングが、最先端のSATソルバでは困難でありながら、短いオーソロジー証明を持つという観測に基づいて、合成SATベンチマークの族を導入する。 EPFL演算回路に応用して,Kissatが有意な分数で出力するのに対して,我々のアルゴリズムはこれらのインスタンスを効率的に解く。 最後に, オーソロジー正規化を前処理ステップとして用いることで, SAT解決時間を短縮できることを示す。

関連論文リスト

• A parallel and distributed fixed-point quantum search algorithm for solving SAT problems [6.341973606434514]
  SAT問題の解決には$mathcalO(sqrt2n)$クエリが必要です。 SAT問題を解くために並列固定点探索アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2026-04-11T01:28:20Z)
• Provable Scaling Laws for the Test-Time Compute of Large Language Models [84.00141420901038]
  本研究では,大規模言語モデルのテスト時間計算において,証明可能なスケーリング法則を享受する2つのアルゴリズムを提案する。 1つは2段階ノックアウト方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。 もう1つは2段階のリーグ方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。
  論文  参考訳（メタデータ） (2024-11-29T05:29:47Z)
• Can Transformers Reason Logically? A Study in SAT Solving [17.15701291424892]
  本研究では,デコーダのみのトランスフォーマーの論理的推論能力について,SAT問題の観点から検討する。 我々は,デコーダのみのトランスフォーマーが,Chain-of-Thought (CoT) によるバックトラックとデダクションを用いて,一様でない計算モデルで 3-SAT を決定できることを示す。
  論文  参考訳（メタデータ） (2024-10-09T21:01:52Z)
• Sum-of-Squares inspired Quantum Metaheuristic for Polynomial Optimization with the Hadamard Test and Approximate Amplitude Constraints [76.53316706600717]
  最近提案された量子アルゴリズムarXiv:2206.14999は半定値プログラミング(SDP)に基づいている SDPにインスパイアされた量子アルゴリズムを2乗和に一般化する。 この結果から,本アルゴリズムは大きな問題に適応し,最もよく知られた古典学に近似することが示唆された。
  論文  参考訳（メタデータ） (2024-08-14T19:04:13Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• Longest Common Substring and Longest Palindromic Substring in $\tilde{\mathcal{O}}(\sqrt{n})$ Time [0.0]
  LCS(Longest Common Substring)とLPS(Longest Palindromic Substring)は、コンピュータ科学における古典的な問題である。 計算回路モデルにおいて, LCS と LPS の双方に対する量子アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2023-09-03T19:27:57Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• Accelerating Inexact HyperGradient Descent for Bilevel Optimization [84.00488779515206]
  本稿では,一般的な非コンケーブ二段階最適化問題の解法を提案する。 また,非コンケーブ問題における2次定常点を求める際の既存の複雑性も改善した。
  論文  参考訳（メタデータ） (2023-06-30T20:36:44Z)
• 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)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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