論文の概要: Arjun: An Efficient Independent Support Computation Technique and its
Applications to Counting and Sampling
- arxiv url: http://arxiv.org/abs/2110.09026v1
- Date: Mon, 18 Oct 2021 05:54:42 GMT
- ステータス: 処理完了
- システム内更新日: 2021-10-19 21:06:38.385139
- Title: Arjun: An Efficient Independent Support Computation Technique and its
Applications to Counting and Sampling
- Title（参考訳）: Arjun: 効率的な独立支援計算手法とそのカウントとサンプリングへの応用
- Authors: Mate Soos and Kuldeep S. Meel
- Abstract要約: 本稿では,実世界のベンチマークから得られる公式を処理できる,効率的でスケーラブルな独立支援手法を設計する。
私たちのフレームワークはArjunと呼ばれ、暗黙的で明示的な定義可能性の概念を採用しています。
特に、Arjunで強化されたApproxMC4は1896年から387のベンチマークを数え、Arjunで強化されたUniGen3は319のベンチマークを同じ時間内に追加する。
- 参考スコア（独自算出の注目度）: 30.20469343138151
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Given a Boolean formula $\varphi$ over the set of variables $X$ and a
projection set $\mathcal{P} \subseteq X$, a subset of variables $\mathcal{I}$
is independent support of $\mathcal{P}$ if two solutions agree on
$\mathcal{I}$, then they also agree on $\mathcal{P}$. The notion of independent
support is related to the classical notion of definability dating back to 1901,
and have been studied over the decades. Recently, the computational problem of
determining independent support for a given formula has attained importance
owing to the crucial importance of independent support for hashing-based
counting and sampling techniques.
In this paper, we design an efficient and scalable independent support
computation technique that can handle formulas arising from real-world
benchmarks. Our algorithmic framework, called Arjun, employs implicit and
explicit definability notions, and is based on a tight integration of
gate-identification techniques and assumption-based framework. We demonstrate
that augmenting the state of the art model counter ApproxMC4 and sampler
UniGen3 with Arjun leads to significant performance improvements. In
particular, ApproxMC4 augmented with Arjun counts 387 more benchmarks out of
1896 while UniGen3 augmented with Arjun samples 319 more benchmarks within the
same time limit.
- Abstract（参考訳）: x$ と射影集合 $\mathcal{p} \subseteq x$ 上のブール式 $\varphi$ が与えられたとき、変数のサブセット $\mathcal{i}$ が$\mathcal{p}$ の独立サポートであるなら、2つの解が$\mathcal{i}$ に一致するなら、$\mathcal{p}$ についても同意する。
独立支持の概念は1901年にさかのぼる古典的な定義と関係しており、数十年にわたって研究されてきた。
近年,ハッシュに基づくカウント・サンプリング手法の独立サポートの重要性から,与えられた式に対する独立サポートを決定する計算問題の重要性が高まっている。
本稿では,実世界のベンチマークから生じる公式を処理可能な効率的でスケーラブルな独立サポート計算手法を考案する。
我々のアルゴリズムフレームワークはArjunと呼ばれ、暗黙的かつ明示的な定義可能性の概念を採用しており、ゲート識別技術と仮定に基づくフレームワークの密接な統合に基づいている。
我々は,arjun による art model counter approxmc4 と sampler unigen3 の強化により,性能が大幅に向上することを示す。
特に、Arjunで強化されたApproxMC4は1896年から387のベンチマークを数え、Arjunで強化されたUniGen3は319のベンチマークを同じ時間内に追加する。
関連論文リスト
- Making Multi-Axis Gaussian Graphical Models Scalable to Millions of Samples and Features [0.30723404270319693]
我々は独立性を仮定することなく、$O(n2)$ランタイムと$O(n)$スペース複雑性を持つメソッドを導入する。
我々は,実世界の1000,000セルのscRNA-seqデータセットなど,前例のない大規模なデータセットに対して,我々のアプローチが適用可能であることを実証した。
論文 参考訳（メタデータ） (2024-07-29T11:15:25Z) - Computational-Statistical Gaps in Gaussian Single-Index Models [77.1473134227844]
単次元モデル(Single-Index Models)は、植木構造における高次元回帰問題である。
我々は,統計的クエリ (SQ) と低遅延多項式 (LDP) フレームワークの両方において,計算効率のよいアルゴリズムが必ずしも$Omega(dkstar/2)$サンプルを必要とすることを示した。
論文 参考訳（メタデータ） (2024-03-08T18:50:19Z) - Combinatorial Stochastic-Greedy Bandit [79.1700188160944]
我々は,選択した$n$のアームセットのジョイント報酬以外の余分な情報が観測されない場合に,マルチアームのバンディット問題に対する新規グリーディ・バンディット(SGB)アルゴリズムを提案する。
SGBは最適化された拡張型コミットアプローチを採用しており、ベースアームの大きなセットを持つシナリオ用に特別に設計されている。
論文 参考訳（メタデータ） (2023-12-13T11:08:25Z) - Magnushammer: A Transformer-Based Approach to Premise Selection [20.445974111113223]
我々は、(保護状態、関連する前提)ペアのテキスト表現を含む、前提選択のための新しいデータセットを開発し、オープンソース化する。
我々の手法であるMagnushammerは、Sledgehammerと呼ばれるインタラクティブな定理の証明において、最も先進的で広く使われている自動化ツールより優れています。
さらに、PISAベンチマークでは、最先端の証明成功率を57.0%から71.0%に改善し、パラメータを4ドル減らした。
論文 参考訳（メタデータ） (2023-03-08T10:22:00Z) - Nystr\"om $M$-Hilbert-Schmidt Independence Criterion [0.0]
カーネルをユビキタスにする主な特徴は、 (i) 設計された領域の数、 (ii) カーネルに関連する関数クラスのヒルベルト構造、 (iii) 情報を失うことなく確率分布を表現する能力である。
我々は、Mge 2$のケースを処理し、その一貫性を証明し、その適用性を実証する代替のNystr"omベースのHSIC推定器を提案する。
論文 参考訳（メタデータ） (2023-02-20T11:51:58Z) - Unitarity estimation for quantum channels [7.323367190336826]
ユニタリティ推定は、量子デバイス認証とベンチマークにおいて基礎的で重要な問題である。
我々は、アンシラ効率のアルゴリズムを誘導するユニタリティ推定のための統一的なフレームワークを提供する。
アルゴリズムの$d$-dependenceと$epsilon$-dependenceの両方が最適であることを示す。
論文 参考訳（メタデータ） (2022-12-19T09:36:33Z) - Permutation Compressors for Provably Faster Distributed Nonconvex
Optimization [68.8204255655161]
本稿では,Gorbunov et al (2021) の MARINA 法が,理論的な通信複雑性の観点から最先端の手法とみなすことができることを示す。
MARINAの理論は、古典的な独立圧縮機設定を超えて、潜在的にエミュレートされた圧縮機の理論を支持するものである。
論文 参考訳（メタデータ） (2021-10-07T09:38:15Z) - An Online Riemannian PCA for Stochastic Canonical Correlation Analysis [37.8212762083567]
投影行列の再パラメータ化を用いた正準相関解析(CCA)のための効率的なアルゴリズム(RSG+)を提案する。
本論文は,その特性の定式化と技術的解析に主眼を置いているが,本実験により,一般的なデータセットに対する経験的挙動が極めて有望であることが確認された。
論文 参考訳（メタデータ） (2021-06-08T23:38:29Z) - Top-$k$ eXtreme Contextual Bandits with Arm Hierarchy [71.17938026619068]
我々は、腕の総数が膨大であることができるトップ$ k$極端な文脈的包帯問題を研究します。
まず,Inverse Gap Weighting戦略を用いて,非極端に実現可能な設定のアルゴリズムを提案する。
我々のアルゴリズムは、$O(ksqrt(A-k+1)T log (|mathcalF|T))$である。
論文 参考訳（メタデータ） (2021-02-15T19:10:52Z) - Neural Bayes: A Generic Parameterization Method for Unsupervised
Representation Learning [175.34232468746245]
本稿ではニューラルベイズと呼ばれるパラメータ化手法を提案する。
これは一般に計算が難しい統計量の計算を可能にする。
このパラメータ化のための2つの独立したユースケースを示す。
論文 参考訳（メタデータ） (2020-02-20T22:28:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。