論文の概要: Estimating the hardness of SAT encodings for Logical Equivalence
Checking of Boolean circuits
- arxiv url: http://arxiv.org/abs/2210.01484v1
- Date: Tue, 4 Oct 2022 09:19:13 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-05 14:14:56.382213
- Title: Estimating the hardness of SAT encodings for Logical Equivalence
Checking of Boolean circuits
- Title（参考訳）: ブール回路の論理等価チェックのためのSAT符号化の硬さの推定
- Authors: Alexander Semenov, Konstantin Chukharev, Egor Tarasov, Daniil
Chivilikhin and Viktor Kondratiev
- Abstract要約: LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。
そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
- 参考スコア（独自算出の注目度）: 58.83758257568434
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this paper we investigate how to estimate the hardness of Boolean
satisfiability (SAT) encodings for the Logical Equivalence Checking problem
(LEC). Meaningful estimates of hardness are important in cases when a
conventional SAT solver cannot solve a SAT instance in a reasonable time. We
show that the hardness of SAT encodings for LEC instances can be estimated
\textit{w.r.t.} some SAT partitioning. We also demonstrate the dependence of
the accuracy of the resulting estimates on the probabilistic characteristics of
a specially defined random variable associated with the considered
partitioning. The paper proposes several methods for constructing
partitionings, which, when used in practice, allow one to estimate the hardness
of SAT encodings for LEC with good accuracy. In the experimental part we
propose a class of scalable LEC tests that give extremely complex instances
with a relatively small input size $n$ of the considered circuits. For example,
for $n = 40$, none of the state-of-the-art SAT solvers can cope with the
considered tests in a reasonable time. However, these tests can be solved in
parallel using the proposed partitioning methods.
- Abstract（参考訳）: 本稿では,論理等価チェック問題 (LEC) に対して, Boolean satisfiability (SAT) エンコーディングの硬さを推定する方法を検討する。
従来のSATソルバがSATインスタンスを妥当な時間で解けない場合、難易度の平均的な推定は重要である。
LEC インスタンスに対する SAT エンコーディングの硬さは、いくつかの SAT パーティショニングにおいて \textit{w.r.t.} と推定できることを示す。
また, 推定結果の精度は, 分割を考慮した特殊に定義された確率変数の確率的特性に依存することを示した。
そこで本研究では, SAT符号化の難易度を精度良く推定できる分割構成法を提案する。
実験的な部分では、比較的小さな入力サイズを持つ非常に複雑なインスタンスを考慮された回路の$n$で提供するスケーラブルなLECテストのクラスを提案する。
例えば、$n = 40$の場合、最先端のSATソルバは、考慮されたテストに妥当な時間で対処できない。
しかし、これらのテストは、提案手法を用いて並列に解決できる。
関連論文リスト
- Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。
これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。
私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文 参考訳（メタデータ） (2024-10-18T22:25:54Z) - ParaICL: Towards Robust Parallel In-Context Learning [74.38022919598443]
大規模言語モデル(LLM)が自然言語処理の標準となっている。
インコンテキスト・ラーニング(ICL)は、いくつかの実演例の選択に依存している。
パラレルインコンテキスト学習(ParaICL)という新しい手法を提案する。
論文 参考訳（メタデータ） (2024-03-31T05:56:15Z) - Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
分解硬度(d硬度)の概念を導入する。
d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
論文 参考訳（メタデータ） (2023-12-16T12:44:36Z) - Using deep learning to construct stochastic local search SAT solvers
with performance bounds [0.0]
グラフニューラルネットワークを用いてオーラクルを訓練し、2つのSLSソルバ上で、様々な難易度を持つランダムSATインスタンス上でそれらを評価する。
GNNベースのオラクルへのアクセスは,両者のパフォーマンスを著しく向上させることがわかった。
論文 参考訳（メタデータ） (2023-09-20T16:27:52Z) - Machine Learning for SAT: Restricted Heuristics and New Graph
Representations [0.8870188183999854]
SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。
大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。
我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
論文 参考訳（メタデータ） (2023-07-18T10:46:28Z) - Sequential Permutation Testing of Random Forest Variable Importance
Measures [68.8204255655161]
そこで本研究では、逐次置換テストと逐次p値推定を用いて、従来の置換テストに関連する高い計算コストを削減することを提案する。
シミュレーション研究の結果、シーケンシャルテストの理論的性質が当てはまることを確認した。
本手法の数値安定性を2つの応用研究で検討した。
論文 参考訳（メタデータ） (2022-06-02T20:16:50Z) - DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
We present DeepSAT, a novel-to-end learning framework for the Boolean satisfiability (SAT) problem。
DeepSATは最先端の学習ベースSATソリューションに対して,大幅な精度向上を実現している。
論文 参考訳（メタデータ） (2022-05-27T03:20:42Z) - Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。
ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
論文 参考訳（メタデータ） (2022-03-02T05:14:12Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳（メタデータ） (2021-07-15T04:47:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。