論文の概要: MatSat: a matrix-based differentiable SAT solver
- arxiv url: http://arxiv.org/abs/2108.06481v1
- Date: Sat, 14 Aug 2021 07:38:06 GMT
- ステータス: 処理完了
- システム内更新日: 2021-08-17 15:17:27.134209
- Title: MatSat: a matrix-based differentiable SAT solver
- Title（参考訳）: MatSat: 行列ベースの微分可能なSATソルバ
- Authors: Taisuke Sato (1) and Ryosuke Kojima (2) ((1) National Institute of
Informatics (NII), (2) Graduate School of Medicine, Kyoto University)
- Abstract要約: 本稿では,非負の微分可能コスト関数 Jsat のコスト最小化問題として,ベクトル空間におけるSAT問題の解法を提案する。
このアプローチでは、n変数のSAT問題に対する代入を満足する解は、Jsat(u) をゼロにする 0,1n のバイナリベクトル u で表される。
本手法は行列型微分SATソルバであるMatSatとして実装する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We propose a new approach to SAT solving which solves SAT problems in vector
spaces as a cost minimization problem of a non-negative differentiable cost
function J^sat. In our approach, a solution, i.e., satisfying assignment, for a
SAT problem in n variables is represented by a binary vector u in {0,1}^n that
makes J^sat(u) zero. We search for such u in a vector space R^n by cost
minimization, i.e., starting from an initial u_0 and minimizing J to zero while
iteratively updating u by Newton's method. We implemented our approach as a
matrix-based differential SAT solver MatSat. Although existing main-stream SAT
solvers decide each bit of a solution assignment one by one, be they of
conflict driven clause learning (CDCL) type or of stochastic local search (SLS)
type, MatSat fundamentally differs from them in that it continuously approach a
solution in a vector space. We conducted an experiment to measure the
scalability of MatSat with random 3-SAT problems in which MatSat could find a
solution up to n=10^5 variables. We also compared MatSat with four
state-of-the-art SAT solvers including winners of SAT competition 2018 and SAT
Race 2019 in terms of time for finding a solution, using a random benchmark set
from SAT 2018 competition and an artificial random 3-SAT instance set. The
result shows that MatSat comes in second in both test sets and outperforms all
the CDCL type solvers.
- Abstract（参考訳）: 本稿では,非負の微分可能コスト関数 J^sat のコスト最小化問題として,ベクトル空間におけるSAT問題の解法を提案する。
このアプローチでは、n変数のSAT問題に対する代入を満足する解は、J^sat(u) をゼロにする {0,1}^n のバイナリベクトル u で表される。
ベクトル空間 R^n においてそのような u をコスト最小化、すなわち初期 u_0 から J を 0 に最小化し、ニュートン法により u を反復的に更新する。
行列型微分SATソルバMatSatとして提案手法を実装した。
既存の主ストリームsatソルバは、コンフリクト駆動節学習(cdcl)型や確率的局所探索(sls)型など、解割り当ての各ビットを一つずつ決定するが、マサットはベクトル空間内の解に連続的に近づくという点で、それらと根本的に異なる。
そこで我々は,MateSatがn=10^5変数まで解を見つけることのできるランダム3SAT問題を用いて,MateSatのスケーラビリティを測定する実験を行った。
私たちはまた、SAT 2018コンペティションとSAT Race 2019の勝者を含む4つの最先端SATソルバと比較し、SAT 2018コンペティションと人工ランダム3SATインスタンスセットのランダムベンチマークセットを使用して、ソリューションを見つける時間の観点から比較した。
その結果、MateSatは両方のテストセットで2位となり、CDCLの型解決器よりも優れています。
関連論文リスト
- Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。
これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。
私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文 参考訳（メタデータ） (2024-10-18T22:25:54Z) - Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。
本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。
我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
論文 参考訳（メタデータ） (2024-10-11T18:20:08Z) - General Method for Solving Four Types of SAT Problems [12.28597116379225]
既存の方法は、様々なタイプのブール適合性問題(SAT)に対して様々なアルゴリズムを提供する。
本研究では,整数計画法と強化学習法(RL)に基づく統合フレームワークDCSATを提案する。
論文 参考訳（メタデータ） (2023-12-27T06:09:48Z) - Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
分解硬度(d硬度)の概念を導入する。
d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
論文 参考訳（メタデータ） (2023-12-16T12:44:36Z) - Near-Optimal Bounds for Learning Gaussian Halfspaces with Random
Classification Noise [50.64137465792738]
この問題に対する効率的なSQアルゴリズムは、少なくとも$Omega(d1/2/(maxp, epsilon)2)$. のサンプル複雑性を必要とする。
我々の下限は、この1/epsilon$に対する二次的依存は、効率的なアルゴリズムに固有のものであることを示唆している。
論文 参考訳（メタデータ） (2023-07-13T18:59:28Z) - A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。
この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
論文 参考訳（メタデータ） (2023-06-07T12:19:22Z) - 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) - 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) - NLocalSAT: Boosting Local Search with Solution Prediction [36.69915361918781]
SAT問題の解決に有効な方法は局所探索 (SLS) である。
この方法はランダムな方法で割り振られ、SLSソルバの有効性に影響を与える。
NLocalSATは、SLSとソリューション予測モデルを組み合わせることで、ニューラルネットワークによる初期化割り当てを変更することで、SLSを向上する。
NLocalSATのソルバは元のSLSソルバよりも27% 62%改善した。
論文 参考訳（メタデータ） (2020-01-26T04:22:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。