論文の概要: Decomposing Hard SAT Instances with Metaheuristic Optimization
- arxiv url: http://arxiv.org/abs/2312.10436v1
- Date: Sat, 16 Dec 2023 12:44:36 GMT
- ステータス: 処理完了
- システム内更新日: 2023-12-19 16:27:26.279386
- Title: Decomposing Hard SAT Instances with Metaheuristic Optimization
- Title（参考訳）: メタヒューリスティック最適化によるハードSATインスタンスの分解
- Authors: Daniil Chivilikhin and Artem Pavlenko and Alexander Semenov
- Abstract要約: 分解硬度(d硬度)の概念を導入する。
d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
- 参考スコア（独自算出の注目度）: 52.03315747221343
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In the article, within the framework of the Boolean Satisfiability problem
(SAT), the problem of estimating the hardness of specific Boolean formulas
w.r.t. a specific complete SAT solving algorithm is considered. Based on the
well-known Strong Backdoor Set (SBS) concept, we introduce the notion of
decomposition hardness (d-hardness). If $B$ is an arbitrary subset of the set
of variables occurring in a SAT formula $C$, and $A$ is an arbitrary complete
SAT solver , then the d-hardness expresses an estimate of the hardness of $C$
w.r.t. $A$ and $B$. We show that the d-hardness of $C$ w.r.t. a particular $B$
can be expressed in terms of the expected value of a special random variable
associated with $A$, $B$, and $C$. For its computational evaluation, algorithms
based on the Monte Carlo method can be used. The problem of finding $B$ with
the minimum value of d-hardness is formulated as an optimization problem for a
pseudo-Boolean function whose values are calculated as a result of a
probabilistic experiment. To minimize this function, we use evolutionary
algorithms. In the experimental part, we demonstrate the applicability of the
concept of d-hardness and the methods of its estimation to solving hard
unsatisfiable SAT instances.
- Abstract（参考訳）: 本稿では、ブール満足度問題(SAT)の枠組みの中で、特定のブール公式の硬さを推定する問題を考える。
良く知られたSBS(Strong Backdoor Set)の概念に基づいて,分解硬度(d-hardness)の概念を導入する。
B$ が SAT 式に現れる変数の集合の任意の部分集合で、$A$ が任意の完全 SAT ソルバーであれば、d-ハードネスは $C$ w.r.t.$A$ と $B$ の硬さを推定する。
特定の$B$のd-hardnessは、$A$、$B$、$C$に関連付けられた特別な確率変数の期待値の観点から表現できることを示す。
計算評価にはモンテカルロ法に基づくアルゴリズムを用いることができる。
d-ハードネスの最小値を持つ$b$を求める問題は、確率実験の結果値が計算される擬似ボア関数の最適化問題として定式化される。
この機能を最小化するために、進化的アルゴリズムを用いる。
実験では,d-hardnessの概念の適用可能性と,satインスタンスの難解性に対する推定手法を示す。
関連論文リスト
- 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) - Contextual Combinatorial Bandits with Probabilistically Triggered Arms [55.9237004478033]
確率的に誘発される腕(C$2$MAB-T)を様々な滑らかさ条件下で検討した。
トリガー変調 (TPM) 条件の下では、C$2$-UC-Tアルゴリズムを考案し、後悔すべき$tildeO(dsqrtT)$を導出する。
論文 参考訳（メタデータ） (2023-03-30T02:51:00Z) - Deterministic Nonsmooth Nonconvex Optimization [94.01526844386977]
次元自由な次元自由アルゴリズムを得るにはランダム化が必要であることを示す。
我々のアルゴリズムは、ReLUネットワークを最適化する最初の決定論的次元自由アルゴリズムを得る。
論文 参考訳（メタデータ） (2023-02-16T13:57:19Z) - 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) - Multi-block-Single-probe Variance Reduced Estimator for Coupled
Compositional Optimization [49.58290066287418]
構成問題の複雑さを軽減するために,MSVR (Multi-block-probe Variance Reduced) という新しい手法を提案する。
本研究の結果は, 試料の複雑さの順序や強靭性への依存など, 様々な面で先行して改善された。
論文 参考訳（メタデータ） (2022-07-18T12:03:26Z) - MAJORITY-3SAT (and Related Problems) in Polynomial Time [4.035753155957698]
与えられた$k$-CNFが有界分母を持つ少なくとも$rho in (0,1)$を持つか否かを決定するアルゴリズムを与える。
我々のアルゴリズムは、複雑性と推論の複雑さを数えることに興味深いポジティブな意味を持っている。
論文 参考訳（メタデータ） (2021-07-06T17:24:04Z) - diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT
and Answer Set Programming [0.0]
diff-SATは正規解と確率的節、事実、ルールを使用する能力を組み合わせる。
サンプリングプロセスは、ユーザ定義の微分可能目的関数を最小化する。
論文 参考訳（メタデータ） (2021-01-03T09:04:31Z) - Learning from Survey Propagation: a Neural Network for MAX-E-$3$-SAT [0.0]
本稿では,最大3-Stisfiability (MAX-E-$3$-SAT) 問題に対して$Theta(N)$で近似解を計算するアルゴリズムを提案する。
論文 参考訳（メタデータ） (2020-12-10T07:59:54Z) - List-Decodable Mean Estimation in Nearly-PCA Time [50.79691056481693]
高次元におけるリストデコタブル平均推定の基本的な課題について検討する。
我々のアルゴリズムは、すべての$k = O(sqrtd) cup Omega(d)$に対して$widetildeO(ndk)$で実行されます。
我々のアルゴリズムの変種は、すべての$k$に対してランタイム$widetildeO(ndk)$を持ち、リカバリ保証の$O(sqrtlog k)$ Factorを犠牲にしている。
論文 参考訳（メタデータ） (2020-11-19T17:21:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。