Fugu-MT 論文翻訳(概要): Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts

論文の概要: Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts

arxiv url: http://arxiv.org/abs/2606.31878v1
Date: Tue, 30 Jun 2026 15:58:08 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-01 18:27:19.308061
Title: Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts
Title（参考訳）: RECARと解像度ベースSATショートカットを用いたモードCEGAR-tableaux
Abstract要約: 本稿では,従来のRECAR手法を用いて,SATショートカットを用いてCEGAR-tableauxを拡張する2つの手法について検討する。 CEGAR-tableauxのC++実装であるCEGARBox++を用いた実験は、RECAR SAT-shortcutsを使用したCEGARBox++が競合しないことを示している。 SAT, tableaux, and resolution method for modal satisfiability, which is a first effective integration of SAT, tableaux and resolution method which are excellent performance than its parts。
参考スコア（独自算出の注目度）: 1.2031796234206138
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR but also a totally new approach using the modal resolution theorem prover KSP as an oracle. Our experiments using our C++ implementation CEGARBox++ of CEGAR-tableaux show that: (1) CEGARBox++ with RECAR SAT-shortcuts is not competitive (2) CEGARBox++ using KSP to provide SAT-shortcuts is superior to both CEGARBox++ and KSP, particularly on large satisfiable problems. As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts.
Abstract（参考訳）: 本稿では,従来のRECARを用いたSATショートカットを用いた CEGAR-tableaux の拡張手法と,モーダル分解定理証明器 KSP をオラクルとして用いた全く新しいアプローチについて検討する。 CEGAR-tableauxのC++実装であるCEGARBox++を用いた実験では,(1) RECAR SAT-shortcutsを使用したCEGARBox++は競争力がない (2) SAT-shortcutsを提供するためにKSPを使用したCEGARBox++は,CEGARBox++とKSPの両方よりも優れている。われわれが知る限り、これはSAT、テーブルローおよび解決法を効果的に統合する最初の方法であり、その部品よりも性能が良い。

関連論文リスト

A Customized SAT-based Solver for Graph Coloring [1.8051006704301766]
本稿では,ZykovColorという新しいSATベースのアルゴリズムを導入し,グラフの着色問題を解く。 H'ebrard と Katsirelos (2020) のアプローチに基づく。 SATソルバの基盤となる利点を生かした新機能を提案する。
論文参考訳（メタデータ） (2025-04-07T08:22:00Z)
Anytime Cooperative Implicit Hitting Set Solving [46.010796136659536]
Implicit Hitting Set (HS)アプローチは、MaxSAT、Pseudo-boolean最適化、その他のフレームワークに非常に効果的であることが示されている。いずれのコンポーネントによって発見されたコアが利用できるマルチスレッドアーキテクチャにおいて、どのように簡単に組み合わせられるかを示す。その結果,HS-lub は HS-lb と HS-ub のどちらよりも独立に優れていることがわかった。
論文参考訳（メタデータ） (2025-01-14T07:23:52Z)
Empirical Evaluation of the Implicit Hitting Set Approach for Weighted CSPs [46.010796136659536]
重み付きCSP問題に対する既存の参照アルゴリズムの代替策について検討する。我々の実証研究は、WCSPにとって最良の選択肢を特定するのは容易ではないことを示している。
論文参考訳（メタデータ） (2025-01-13T15:59:28Z)
Applying the quantum approximate optimization algorithm to general constraint satisfaction problems [0.0]
ランダム制約満足度問題(CSP)に適用した場合に量子近似最適化(QAOA)の性能を解析するための理論的手法を開発する。提案手法により,ランダムに生成されたCSPのインスタンスに適用した場合に,各レイヤとパラメータを用いてQAOAの成功確率を計算することができる。ランダムな$k$-SATは、QAOAを用いた量子古典的分離を示す上で、これらのCSPの中で最も有望であると考えられる。
論文参考訳（メタデータ） (2024-11-26T14:00:34Z)
A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem [14.693394941317843]
本稿では,ブール充足可能性解法と計算機代数システムを組み合わせた検証可能な新しい証明生成法を提案する。提案手法は、3次元のKS系が少なくとも24個のベクトルを含む必要があることを示す。また, KS問題に対して, 順序23の40.3 TiBの低い値のコンピュータ検証証明を初めて提供した。
論文参考訳（メタデータ） (2023-06-23T06:42:59Z)
General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
任意の切削平面制約を加えることができるような境界伝搬手順を一般化する。 MIPソルバは、境界プロパゲーションベースの検証器を強化するために高品質な切削面を生成することができる。本手法は,oval20ベンチマークを完全解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器である。
論文参考訳（メタデータ） (2022-08-11T10:31:28Z)
Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文参考訳（メタデータ） (2021-07-15T04:47:35Z)
AutoRC: Improving BERT Based Relation Classification Models via Architecture Search [50.349407334562045]
BERTに基づく関係分類(RC)モデルは、従来のディープラーニングモデルよりも大幅に改善されている。最適なアーキテクチャとは何かという合意は得られない。 BERTをベースとしたRCモデルのための包括的検索空間を設計し、設計選択を自動的に検出するためにNAS(Neural Architecture Search)手法を用いる。
論文参考訳（メタデータ） (2020-09-22T16:55:49Z)
Improved Algorithms for Conservative Exploration in Bandits [113.55554483194832]
文脈線形帯域設定における保守的学習問題について検討し、新しいアルゴリズムである保守的制約付きLinUCB(CLUCB2)を導入する。我々は、既存の結果と一致したCLUCB2に対する後悔の限界を導き、多くの合成および実世界の問題において、最先端の保守的バンディットアルゴリズムよりも優れていることを実証的に示す。
論文参考訳（メタデータ） (2020-02-08T19:35:01Z)
Testing Unsatisfiability of Constraint Satisfaction Problems via Tensor Products [0.8528384027684192]
本稿では, テンソル分解法を用いて, 効率よく並列に不満足性の証明を計算する方法を示す。 1つの分解は、品質を犠牲にすることなく、半分の時間で不満足な証明をもたらす。この方法は、任意のCSPからバイナリCSPへの、よく知られた双対および隠れ変数変換を用いて、任意のCSPに適用できる。
論文参考訳（メタデータ） (2020-01-31T18:06:52Z)

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