論文の概要: 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ではない。
関連論文リスト
- Shape Arithmetic Expressions: Advancing Scientific Discovery Beyond Closed-Form Equations [56.78271181959529]
GAM(Generalized Additive Models)は、変数とターゲットの間の非線形関係をキャプチャできるが、複雑な特徴相互作用をキャプチャすることはできない。
本稿では,GAMのフレキシブルな形状関数と,数学的表現に見られる複雑な特徴相互作用を融合させる形状表現算術(SHARE)を提案する。
また、標準制約を超えた表現の透明性を保証するSHAREを構築するための一連のルールを設計する。
論文 参考訳（メタデータ） (2024-04-15T13:44:01Z) - Computational-Statistical Gaps in Gaussian Single-Index Models [77.1473134227844]
単次元モデル(Single-Index Models)は、植木構造における高次元回帰問題である。
我々は,統計的クエリ (SQ) と低遅延多項式 (LDP) フレームワークの両方において,計算効率のよいアルゴリズムが必ずしも$Omega(dkstar/2)$サンプルを必要とすることを示した。
論文 参考訳（メタデータ） (2024-03-08T18:50:19Z) - 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 [1.9580473532948401]
2つのCNF式はucp-等価(ucp-equivalent)と呼ばれ、単位節の伝搬(UCP)に関して同じように振る舞う。
公式がucp-irredundant(英語版)と呼ばれるのは、任意の節を削除すると、元の句と等価でない公式が導かれるからである。
論文 参考訳（メタデータ） (2023-09-04T18:15:34Z) - Symbolic Recovery of Differential Equations: The Identifiability Problem [52.158782751264205]
微分方程式の記号的回復は、支配方程式の導出を自動化する野心的な試みである。
関数が対応する微分方程式を一意に決定するために必要な条件と十分な条件の両方を提供する。
この結果を用いて、関数が微分方程式を一意に解くかどうかを判定する数値アルゴリズムを考案する。
論文 参考訳（メタデータ） (2022-10-15T17:32:49Z) - Are Hitting Formulas Hard for Resolution? [26.575053800551633]
打球公式の解の複雑さは、いわゆる既約打球公式に支配されていることを示す。
最大14節のヒット式を列挙する効率的なアルゴリズムを実装した。
論文 参考訳（メタデータ） (2022-06-30T12:13:26Z) - Superredundancy: A tool for Boolean formula minimization complexity
analysis [0.0]
超冗長節 (superredundant clause) は、公式の解法閉鎖において冗長な節である。
逆の超冗長性の概念は、与えられたものと同値であるすべての最小のCNF式における節のメンバシップを保証する。
論文 参考訳（メタデータ） (2022-05-02T09:17:52Z) - Statistically Meaningful Approximation: a Case Study on Approximating
Turing Machines with Transformers [50.85524803885483]
本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。
回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
論文 参考訳（メタデータ） (2021-07-28T04:28:55Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。