論文の概要: 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インスタンスの本来の構造を予測するための特徴と重要性をアブレーション研究で比較した。
関連論文リスト
- Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。
これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。
私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文 参考訳(メタデータ) (2024-10-18T22:25:54Z) - GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。
我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。
生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
論文 参考訳(メタデータ) (2024-05-17T18:00:50Z) - Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
分解硬度(d硬度)の概念を導入する。
d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
論文 参考訳(メタデータ) (2023-12-16T12:44:36Z) - W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。