論文の概要: Bounds on the size of PC and URC formulas
- arxiv url: http://arxiv.org/abs/2001.00819v3
- Date: Wed, 11 Mar 2020 13:40:47 GMT
- ステータス: 処理完了
- システム内更新日: 2023-01-14 17:54:34.327878
- Title: Bounds on the size of PC and URC formulas
- Title(参考訳): PC および URC 式のサイズに関する境界
- Authors: Petr Ku\v{c}era, Petr Savick\'y
- Abstract要約: 式が存在量化された補助変数を使って関数を表す場合、それは関数の符号化と呼ばれる。
我々はPC と URC の公式とエンコーディングのサイズについていくつかの結果を示した。
任意のq-Horn式に対して、補助変数を用いて同じ関数を符号化する大きさのURCを示す。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this paper we investigate CNF formulas, for which the unit propagation is
strong enough to derive a contradiction if the formula together with a partial
assignment of the variables is unsatisfiable (unit refutation complete or URC
formulas) or additionally to derive all implied literals if the formula is
satisfiable (propagation complete or PC formulas). If a formula represents a
function using existentially quantified auxiliary variables, it is called an
encoding of the function. We prove several results on the sizes of PC and URC
formulas and encodings. One of them are separations between the sizes of
formulas of different types. Namely, we prove an exponential separation between
the size of URC formulas and PC formulas and between the size of PC encodings
using auxiliary variables and URC formulas. Besides of this, we prove that the
sizes of any two irredundant PC formulas for the same function differ at most
by a factor polynomial in the number of the variables and present an example of
a function demonstrating that a similar statement is not true for URC formulas.
One of the separations above implies that a q-Horn formula may require an
exponential number of additional clauses to become a URC formula. On the other
hand, for every q-Horn formula, we present a polynomial size URC encoding of
the same function using auxiliary variables. This encoding is not q-Horn in
general.
- Abstract(参考訳): 本稿では,CNF式について,各変数の部分的割り当てとともに式が満足できない場合(単位拡散完全あるいはURC式)や,その式が満足できる場合(伝播完全あるいはPC式)にすべてのインプリートリテラルを導出する場合に矛盾を導出するほど,単位伝搬が強いCNF式について検討する。
式が存在量化された補助変数を用いて関数を表す場合、関数のエンコーディングと呼ばれる。
我々はPC と URC の公式とエンコーディングのサイズについていくつかの結果を示した。
そのうちの1つは、異なる種類の式の大きさの分離である。
すなわち, urc 式と pc 式の大きさと, 補助変数と urc 式を用いた pc エンコーディングのサイズとを指数関数的に分離することを示す。
これに加えて、同一関数に対する任意の2つの既約なpc公式のサイズが変数数における係数多項式によって最大に異なることを証明し、同様のステートメントがurc公式に対して真でないことを示す関数の例を示す。
上記の分離の一つは、q-ホルンの公式が URC 公式となるために指数的な数の追加節を必要とする可能性があることを意味する。
一方、任意のq-Horn公式に対して、補助変数を用いて同じ関数の多項式サイズ URC 符号化を行う。
この符号化は一般にq-Hornではない。
関連論文リスト
- Computational-Statistical Gaps in Gaussian Single-Index Models [77.1473134227844]
単次元モデル(Single-Index Models)は、植木構造における高次元回帰問題である。
我々は,統計的クエリ (SQ) と低遅延多項式 (LDP) フレームワークの両方において,計算効率のよいアルゴリズムが必ずしも$Omega(dkstar/2)$サンプルを必要とすることを示した。
論文 参考訳(メタデータ) (2024-03-08T18:50:19Z) - FormulaQA: A Question Answering Dataset for Formula-Based Numerical
Reasoning [14.850316791298614]
中学校理科試験におけるフォーミュラQAと呼ばれる式に基づく数値推論のための質問応答データセットを提案する。
また,ゼロショットおよび少数ショットチェーン・オブ・ソート法を用いて,サイズが7Bから100Bを超えるLCMの評価を行った。
我々の経験的発見は、我々の複雑な式駆動型フォーミュラQAに適用した場合、既存のモデルの改善の有意な可能性を裏付けるものである。
論文 参考訳(メタデータ) (2024-02-20T03:39:49Z) - Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。
最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。
シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
論文 参考訳(メタデータ) (2023-10-05T07:10:40Z) - On CNF formulas irredundant with respect to unit clause propagation [0.0]
2つのCNF式はucp-等価(ucp-equivalent)と呼ばれ、単位節の伝搬(UCP)に関して同じように振る舞う。
公式がucp-irredundant(英語版)と呼ばれるのは、任意の節を削除すると、元の句と等価でない公式が導かれるからである。
論文 参考訳(メタデータ) (2023-09-04T18:15:34Z) - Superredundancy: A tool for Boolean formula minimization complexity
analysis [0.0]
超冗長節 (superredundant clause) は、公式の解法閉鎖において冗長な節である。
逆の超冗長性の概念は、与えられたものと同値であるすべての最小のCNF式における節のメンバシップを保証する。
論文 参考訳(メタデータ) (2022-05-02T09:17:52Z) - Analytical calculation formulas for capacities of classical and
classical-quantum channels [61.12008553173672]
我々は,古典チャネルのチャネル容量を反復なく解析的に計算する公式を導出する。
拡張解析アルゴリズムもイテレーションがなく、正確な最適値が出力される。
論文 参考訳(メタデータ) (2022-01-07T13:39:09Z) - Statistically Meaningful Approximation: a Case Study on Approximating
Turing Machines with Transformers [50.85524803885483]
本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。
回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
論文 参考訳(メタデータ) (2021-07-28T04:28:55Z) - Learning Aggregation Functions [78.47770735205134]
任意の濃度の集合に対する学習可能なアグリゲータであるLAF(Learning Aggregation Function)を紹介する。
半合成および実データを用いて,LAFが最先端の和(max-)分解アーキテクチャより優れていることを示す実験を報告する。
論文 参考訳(メタデータ) (2020-12-15T18:28:53Z) - One head is better than two: a polynomial restriction for propositional
definite Horn forgetting [0.0]
忘れることは、命題ホルンの公式の単純な場合でさえ np-完全である。
いくつかの公式はシングルヘッドではなく、忘れるのを簡単にするために作成することができる。
論文 参考訳(メタデータ) (2020-09-16T06:49:08Z) - Common equivalence and size after forgetting [0.0]
命題式からの変数の取得は、そのサイズを増大させる可能性がある。
新しい変数の導入は、それを短くする方法である。
共通同値は、空間における共通同値を忘れたり、確認したりするという点で表すことができる。
論文 参考訳(メタデータ) (2020-06-19T14:27:51Z) - Automatic Differentiation in ROOT [62.997667081978825]
数学と計算機代数において、自動微分 (AD) は、コンピュータプログラムによって指定された関数の微分を評価するための一連の技術である。
本稿では、任意のC/C++関数の導関数を生成するために、ClingがサポートするROOTで利用可能なAD技術を提案する。
論文 参考訳(メタデータ) (2020-04-09T09:18:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。