論文の概要: SATfeatPy -- A Python-based Feature Extraction System for Satisfiability
- arxiv url: http://arxiv.org/abs/2204.14116v1
- Date: Fri, 29 Apr 2022 14:10:01 GMT
- ステータス: 処理完了
- システム内更新日: 2022-05-02 14:43:03.844511
- Title: SATfeatPy -- A Python-based Feature Extraction System for Satisfiability
- Title(参考訳): SATfeatPy - 満足度のためのPythonベースの特徴抽出システム
- Authors: Benjamin Provan-Bessell, Marco Dalla, Andrea Visentin, Barry
O'Sullivan
- Abstract要約: 本稿では,CNF形式のSAT問題に対する特徴抽出技術を提供するSATfeatPyを紹介する。
ライブラリは、詳細な機能説明とともに、最新の、使いやすいPythonパッケージで提供される。
本稿では,SAT/UNSATの精度と問題分類の精度を,ライブラリを用いて生成した5つの特徴セットを用いて示す。
- 参考スコア(独自算出の注目度): 2.236663830879273
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Feature extraction is a fundamental task in the application of machine
learning methods to SAT solving. It is used in algorithm selection and
configuration for solver portfolios and satisfiability classification. Many
approaches have been proposed to extract meaningful attributes from CNF
instances. Most of them lack a working/updated implementation, and the limited
descriptions lack clarity affecting the reproducibility. Furthermore, the
literature misses a comparison among the features. This paper introduces
SATfeatPy, a library that offers feature extraction techniques for SAT problems
in the CNF form. This package offers the implementation of all the structural
and statistical features from there major papers in the field. The library is
provided in an up-to-date, easy-to-use Python package alongside a detailed
feature description. We show the high accuracy of SAT/UNSAT and problem
category classification, using five sets of features generated using our
library from a dataset of 3000 SAT and UNSAT instances, over ten different
classes of problems. Finally, we compare the usefulness of the features and
importance for predicting a SAT instance's original structure in an ablation
study.
- Abstract(参考訳): 特徴抽出は、SAT解決への機械学習手法の適用における基本的な課題である。
解法ポートフォリオと満足度分類のアルゴリズム選択と構成に使用される。
cnfインスタンスから有意義な属性を抽出するための多くのアプローチが提案されている。
多くは動作/更新された実装がなく、限定的な記述は再現性に影響を与える明快さを欠いている。
さらに、文献は特徴の比較を欠いている。
本稿では,CNF形式のSAT問題に対する特徴抽出技術を提供するSATfeatPyを紹介する。
このパッケージは、この分野の主要な論文から得られるすべての構造的および統計的特徴の実装を提供する。
ライブラリは、詳細な機能説明とともに、最新の、使いやすいPythonパッケージで提供される。
3000のSATインスタンスとUNSATインスタンスのデータセットから,ライブラリを用いて生成した5つの特徴セットを用いて,SAT/UNSATの高精度な分類と問題カテゴリ分類を示す。
最後に,SATインスタンスの本来の構造を予測するための特徴と重要性をアブレーション研究で比較した。
関連論文リスト
- 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) - Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
本稿では、繰り返しニューラルネットワークを統合したGNNベースのアーキテクチャであるAsymSATを提案し、可変代入に対する依存予測を生成する。
実験結果から,大規模テストセット上でのSATインスタンスの解数を改善することにより,依存変数予測がGNN方式の解解能力を拡張できることが示唆された。
論文 参考訳(メタデータ) (2023-04-18T05:33:33Z) - W2SAT: Learning to generate SAT instances from Weighted Literal
Incidence Graphs [13.173307471333619]
W2SATは、現実世界/産業インスタンスから固有の構造と特性を学ぶことによってSAT式を生成するフレームワークである。
Weighted Literal Incidence Graph (WLIG)と呼ばれる新しいSAT表現を導入する。
WLIGからSAT問題への復号化は、新しい丘登り最適化法で重なり合う斜角を見つけることをモデル化する。
論文 参考訳(メタデータ) (2023-02-01T06:30:41Z) - 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) - SATformer: Transformer-Based UNSAT Core Learning [0.0]
本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。
SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。
SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。
実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
論文 参考訳(メタデータ) (2022-09-02T11:17:39Z) - 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) - Scikit-dimension: a Python package for intrinsic dimension estimation [58.8599521537]
この技術ノートは、固有次元推定のためのオープンソースのPythonパッケージであるtextttscikit-dimensionを紹介している。
textttscikit-dimensionパッケージは、Scikit-learnアプリケーションプログラミングインターフェイスに基づいて、既知のID推定子のほとんどを均一に実装する。
パッケージを簡潔に記述し、実生活と合成データにおけるID推定手法の大規模(500以上のデータセット)ベンチマークでその使用を実証する。
論文 参考訳(メタデータ) (2021-09-06T16:46:38Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Captum: A unified and generic model interpretability library for PyTorch [49.72749684393332]
我々は,PyTorch用の新しい,統一されたオープンソースモデル解釈可能性ライブラリを紹介する。
このライブラリには、多くの勾配と摂動に基づく属性アルゴリズムの汎用的な実装が含まれている。
分類モデルと非分類モデルの両方に使用できる。
論文 参考訳(メタデータ) (2020-09-16T18:57:57Z) - Multi-layer Optimizations for End-to-End Data Analytics [71.05611866288196]
代替アプローチを実現するフレームワークであるIFAQ(Iterative Functional Aggregate Queries)を紹介する。
IFAQは、特徴抽出クエリと学習タスクを、IFAQのドメイン固有言語で与えられた1つのプログラムとして扱う。
IFAQ の Scala 実装が mlpack,Scikit,特殊化を数桁で上回り,線形回帰木モデルや回帰木モデルを複数の関係データセット上で処理可能であることを示す。
論文 参考訳(メタデータ) (2020-01-10T16:14:44Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。