Prime Implicates and Prime Implicants: From Propositional to Modal Logic
プライム含意とプライム含意：命題論理から様相論理へ
Prime implicates and prime implicants have proven relevant to a number of areas of artificial intelligence, most notably abductive reasoning and knowledge compilation. The purpose of this paper is to examine how these notions might be appropriately extended from propositional logic to the modal logic K. We begin the paper by considering a number of potential definitions of clauses and terms for K. The different definitions are evaluated with respect to a set of syntactic, semantic, and complexity-theoretic properties characteristic of the propositional definition. We then compare the definitions with respect to the properties of the notions of prime implicates and prime implicants that they induce. While there is no definition that perfectly generalizes the propositional notions, we show that there does exist one definition which satisfies many of the desirable properties of the propositional case. In the second half of the paper, we consider the computational properties of the selected definition. To this end, we provide sound and complete algorithms for generating and recognizing prime implicates, and we show the prime implicate recognition task to be PSPACE-complete. We also prove upper and lower bounds on the size and number of prime implicates. While the paper focuses on the logic K, all of our results hold equally well for multi-modal K and for concept expressions in the description logic ALC.
プライム含意とプライム含意項は、人工知能の多くの分野、特にアブダクション推論と知識コンパイルに関連していることが証明されています。本論文の目的は、これらの概念が命題論理から様相論理Kへどのように適切に拡張できるかを検証することです。本論文ではまず、Kの節と項のいくつかの潜在的な定義を検討します。異なる定義は、命題定義に特徴的な統語的、意味的、および計算量理論的特性の集合に関して評価されます。次に、プライム含意とプライム含意項の概念が誘導する特性に関して、それらの定義を比較します。命題概念を完全に一般化する定義はないが、命題ケースの望ましい特性の多くを満たす定義が1つ存在することを示す。本論文の後半では、選択した定義の計算特性を検討します。この目的のため、我々はプライム含意を生成および認識するための健全かつ完全なアルゴリズムを提供し、プライム含意の認識タスクがPSPACE完全であることを示す。また、プライム含意のサイズと数の上限と下限も証明します。本論文は論理Kに焦点を当てているが、我々の結果はすべて、マルチモーダルKおよび記述論理ALCの概念表現にも同様に当てはまる。
Soft Goals Can Be Compiled Away
ソフトゴールはコンパイルによって除去可能
Soft goals extend the classical model of planning with a simple model of preferences. The best plans are then not the ones with least cost but the ones with maximum utility, where the utility of a plan is the sum of the utilities of the soft goals achieved minus the plan cost. Finding plans with high utility appears to involve two linked problems: choosing a subset of soft goals to achieve and finding a low-cost plan to achieve them. New search algorithms and heuristics have been developed for planning with soft goals, and a new track has been introduced in the International Planning Competition (IPC) to test their performance. In this note, we show however that these extensions are not needed: soft goals do not increase the expressive power of the basic model of planning with action costs, as they can easily be compiled away. We apply this compilation to the problems of the net-benefit track of the most recent IPC, and show that optimal and satisficing cost-based planners do better on the compiled problems than optimal and satisficing net-benefit planners on the original problems with explicit soft goals. Furthermore, we show that penalties, or negative preferences expressing conditions to avoid, can also be compiled away using a similar idea.
ソフト ゴールは、単純な選好モデルを使用して古典的な計画モデルを拡張します。したがって、最適な計画はコストが最小の計画ではなく、効用が最大の計画になります。計画の効用は、達成されたソフト ゴールの効用の合計から計画コストを差し引いたものです。高い効用を持つ計画を見つけることは、達成すべきソフトゴールのサブセットを選択することと、それらを達成するための低コストの計画を見つけることという、2つの関連した問題を伴うようです。ソフトゴールを持つ計画のための新しい探索アルゴリズムとヒューリスティックが開発され、そのパフォーマンスをテストするための新しいトラックが国際計画コンペティション(IPC)に導入されました。しかし、このノートでは、これらの拡張は必要ないことを示します。ソフトゴールは簡単にコンパイルできるため、行動コストを持つ計画の基本モデルの表現力を高めません。このコンパイルを最新のIPCの純便益トラックの問題に適用し、コンパイルされた問題では、明示的なソフトゴールを持つ元の問題での最適かつ満足度の高い純便益プランナーよりも、最適かつ満足度の高いコストベースプランナーの方が優れた結果を示すことを示します。さらに、ペナルティ、つまり回避すべき条件を表す否定的な選好も、同様のアイデアを使用してコンパイルして削除できることを示します。
RoxyBot-06: Stochastic Prediction and Optimization in TAC Travel
RoxyBot-06: TAC移動における確率的予測と最適化
In this paper, we describe our autonomous bidding agent, RoxyBot, who emerged victorious in the travel division of the 2006 Trading Agent Competition in a photo finish. At a high level, the design of many successful trading agents can be summarized as follows: (i) price prediction: build a model of market prices; and (ii) optimization: solve for an approximately optimal set of bids, given this model. To predict, RoxyBot builds a stochastic model of market prices by simulating simultaneous ascending auctions. To optimize, RoxyBot relies on the sample average approximation method, a stochastic optimization technique.
本稿では、2006年のTrading Agentコンペティションの旅行部門で写真判定の末に優勝した自律入札エージェントRoxyBotについて説明します。多くの成功した取引エージェントの設計は、大まかに次のようにまとめることができます。(i)価格予測:市場価格のモデルを構築します。(ii)最適化:このモデルに基づいて、ほぼ最適な入札セットを解く。予測を行うために、RoxyBotは同時上昇オークションをシミュレートすることで市場価格の確率モデルを構築します。最適化を行うために、RoxyBotは確率的最適化手法であるサンプル平均近似法に依存しています。
The Role of Macros in Tractable Planning
扱いやすい計画におけるマクロの役割
This paper presents several new tractability results for planning based on macros. We describe an algorithm that optimally solves planning problems in a class that we call inverted tree reducible, and is provably tractable for several subclasses of this class. By using macros to store partial plans that recur frequently in the solution, the algorithm is polynomial in time and space even for exponentially long plans. We generalize the inverted tree reducible class in several ways and describe modifications of the algorithm to deal with these new classes. Theoretical results are validated in experiments.
本論文では、マクロに基づくプランニングのいくつかの新しい扱いやすさの結果を示します。逆木縮約可能と呼ぶクラスのプランニング問題を最適に解決し、このクラスのいくつかのサブクラスに対して証明可能に扱いやすいアルゴリズムについて説明します。解に頻繁に出現する部分プランをマクロに格納することで、指数関数的に長いプランであっても、アルゴリズムは時間と空間に関して多項式的となります。我々は、逆木可約クラスをいくつかの方法で一般化し、これらの新しいクラスに対応するためのアルゴリズムの修正について述べる。理論結果は実験によって検証されます。
Friends or Foes? On Planning as Satisfiability and Abstract CNF Encodings
味方か敵か？充足可能性としての計画と抽象CNFエンコーディングについて
Planning as satisfiability, as implemented in, for instance, the SATPLAN tool, is a highly competitive method for finding parallel step-optimal plans. A bottleneck in this approach is to *prove the absence* of plans of a certain length. Specifically, if the optimal plan has N steps, then it is typically very costly to prove that there is no plan of length N-1. We pursue the idea of leading this proof within solution length preserving abstractions (over-approximations) of the original planning task. This is promising because the abstraction may have a much smaller state space; related methods are highly successful in model checking. In particular, we design a novel abstraction technique based on which one can, in several widely used planning benchmarks, construct abstractions that have exponentially smaller state spaces while preserving the length of an optimal plan.Surprisingly, the idea turns out to appear quite hopeless in the context of planning as satisfiability. Evaluating our idea empirically, we run experiments on almost all benchmarks of the international planning competitions up to IPC 2004, and find that even hand-made abstractions do not tend to improve the performance of SATPLAN. Exploring these findings from a theoretical point of view, we identify an interesting phenomenon that may cause this behavior. We compare various planning-graph based CNF encodings F of the original planning task with the CNF encodings F_abs of the abstracted planning task. We prove that, in many cases, the shortest resolution refutation for F_abs can never be shorter than that for F. This suggests a fundamental weakness of the approach, and motivates further investigation of the interplay between declarative transition-systems, over-approximating abstractions, and SAT encodings.
例えばSATPLANツールに実装されているような、充足可能性としての計画は、並列ステップ最適計画を見つけるための非常に競争力のある手法です。このアプローチのボトルネックは、特定の長さの計画が*存在しないことを証明*することです。具体的には、最適計画がNステップの場合、長さN-1の計画が存在しないことを証明するのは通常非常にコストがかかります。我々は、元の計画タスクの解の長さを保存した抽象化（過剰近似）内でこの証明を導くというアイデアを追求します。この抽象化は状態空間がはるかに小さくなる可能性があるため、これは有望です。関連手法はモデル検査において非常に成功しています。特に、我々は、広く使用されているいくつかの計画ベンチマークにおいて、最適計画の長さを保存しながら、指数関数的に小さい状態空間を持つ抽象化を構築できる、新しい抽象化手法を設計します。驚くべきことに、充足可能性としての計画という文脈では、このアイデアは全く役に立たないことが判明しました。このアイデアを経験的に評価するため、IPC 2004までの国際プランニングコンペティションのほぼすべてのベンチマークで実験を行い、手作業で作成した抽象化でさえSATPLANのパフォーマンスを向上させる傾向がないことがわかりました。これらの発見を理論的な観点から調査し、この動作の原因となる可能性のある興味深い現象を特定しました。元のプランニングタスクのさまざまなプランニンググラフベースのCNFエンコーディングFと、抽象化されたプランニングタスクのCNFエンコーディングF_absを比較します。多くの場合、F_absの最短解像度反証がFのそれよりも短くなることはないことを証明します。これは、このアプローチの根本的な弱点を示唆しており、宣言的遷移システム、過剰近似抽象化、およびSATエンコーディングの相互作用についてさらに調査する動機となります。
Approximate Strong Equilibrium in Job Scheduling Games
ジョブスケジューリングゲームにおける近似強均衡
A Nash Equilibrium (NE) is a strategy profile resilient to unilateral deviations, and is predominantly used in the analysis of multiagent systems. A downside of NE is that it is not necessarily stable against deviations by coalitions. Yet, as we show in this paper, in some cases, NE does exhibit stability against coalitional deviations, in that the benefits from a joint deviation are bounded. In this sense, NE approximates strong equilibrium.Coalition formation is a key issue in multiagent systems. We provide a framework for quantifying the stability and the performance of various assignment policies and solution concepts in the face of coalitional deviations. Within this framework we evaluate a given configuration according to three measures: (i) IR_min: the maximal number alpha, such that there exists a coalition in which the minimal improvement ratio among the coalition members is alpha, (ii) IR_max: the maximal number alpha, such that there exists a coalition in which the maximal improvement ratio among the coalition members is alpha, and (iii) DR_max: the maximal possible damage ratio of an agent outside the coalition.We analyze these measures in job scheduling games on identical machines. In particular, we provide upper and lower bounds for the above three measures for both NE and the well-known assignment rule Longest Processing Time (LPT).Our results indicate that LPT performs better than a general NE. However, LPT is not the best possible approximation. In particular, we present a polynomial time approximation scheme (PTAS) for the makespan minimization problem which provides a schedule with IR_min of 1+epsilon for any given epsilon. With respect to computational complexity, we show that given an NE on m >= 3 identical machines or m >= 2 unrelated machines, it is NP-hard to determine whether a given coalition can deviate such that every member decreases its cost.
ナッシュ均衡（NE）は、一方的な逸脱に対して耐性のある戦略プロファイルであり、主にマルチエージェントシステムの分析で用いられます。NEの欠点は、必ずしも提携による逸脱に対して安定ではないことです。しかしながら、本論文で示すように、場合によってはNEは提携による逸脱に対して安定性を示し、共同逸脱による利益が限定されます。この意味で、NEは強均衡に近似します。提携形成はマルチエージェントシステムにおける重要な問題です。本稿では、提携による逸脱に直面した際の様々な割り当てポリシーとソリューションコンセプトの安定性とパフォーマンスを定量化するための枠組みを提供します。この枠組みにおいて、与えられた構成を3つの尺度に基づいて評価します。(i) IR_min：提携メンバー間の改善率が最小となる提携が存在するような、最大数のα、(ii) IR_max：提携メンバー間の改善率が最大となる提携が存在するような、最大数のα、(iii) DR_max：提携外のエージェントの最大可能損害率。これらの尺度を、同一マシン上のジョブスケジューリングゲームで分析します。特に、NEとよく知られている割り当て規則である最長処理時間（LPT）の両方について、上記3つの指標の上限と下限を示します。結果は、LPTが一般的なNEよりも優れた性能を発揮することを示しています。しかし、LPTは最良の近似法ではありません。特に、メイクスパン最小化問題に対する多項式時間近似スキーム（PTAS）を提示し、任意のイプシロンに対してIR_minが1+イプシロンとなるスケジュールを提供します。計算量に関しては、m >= 3台の同一マシンまたはm >= 2台の無関係なマシン上のNEが与えられた場合、特定の連合がすべてのメンバーのコストを削減するように逸脱できるかどうかを判断することはNP困難であることを示します。
Multilingual Part-of-Speech Tagging: Two Unsupervised Approaches
多言語品詞タグ付け：2つの教師なしアプローチ
We demonstrate the effectiveness of multilingual learning for unsupervised part-of-speech tagging. The central assumption of our work is that by combining cues from multiple languages, the structure of each becomes more apparent. We consider two ways of applying this intuition to the problem of unsupervised part-of-speech tagging: a model that directly merges tag structures for a pair of languages into a single sequence and a second model which instead incorporates multilingual context using latent variables. Both approaches are formulated as hierarchical Bayesian models, using Markov Chain Monte Carlo sampling techniques for inference. Our results demonstrate that by incorporating multilingual evidence we can achieve impressive performance gains across a range of scenarios. We also found that performance improves steadily as the number of available languages increases.
教師なし品詞タグ付けにおける多言語学習の有効性を実証します。本研究の中心的な仮定は、複数言語からの手がかりを組み合わせることで、それぞれの言語の構造がより明確になるというものです。この直感を教師なし品詞タグ付けの問題に適用する2つの方法を検討します。1つは、2つの言語のタグ構造を単一のシーケンスに直接統合するモデル、もう1つは、潜在変数を用いて多言語コンテキストを組み込むモデルです。どちらのアプローチも、推論にマルコフ連鎖モンテカルロサンプリング手法を用いた階層的ベイズモデルとして定式化されています。本研究の結果は、多言語的証拠を組み込むことで、様々なシナリオにおいて目覚ましいパフォーマンス向上を達成できることを示す。また、利用可能な言語の数が増えるにつれて、パフォーマンスが着実に向上することもわかった。
Cross-lingual Annotation Projection for Semantic Roles
意味役割のためのクロスリンガルアノテーション投影
This article considers the task of automatically inducing role-semantic annotations in the FrameNet paradigm for new languages. We propose a general framework that is based on annotation projection, phrased as a graph optimization problem. It is relatively inexpensive and has the potential to reduce the human effort involved in creating role-semantic resources. Within this framework, we present projection models that exploit lexical and syntactic information. We provide an experimental evaluation on an English-German parallel corpus which demonstrates the feasibility of inducing high-precision German semantic role annotation both for manually and automatically annotated English data.
本稿では、新しい言語のFrameNetパラダイムにおいて、役割意味アノテーションを自動的に誘導するタスクについて考察します。グラフ最適化問題として表現されるアノテーション投影に基づく一般的なフレームワークを提案します。これは比較的低コストであり、役割意味リソースの作成に伴う人的労力を削減する可能性を秘めています。このフレームワークにおいて、語彙情報と統語情報を活用する投影モデルを提示します。英語-ドイツ語対訳コーパスを用いた実験的評価を行い、手動および自動でアノテーションされた英語データの両方に対して、高精度なドイツ語意味役割アノテーションを誘導できることを示す。
ParamILS: An Automatic Algorithm Configuration Framework
ParamILS：自動アルゴリズム設定フレームワーク
The identification of performance-optimizing parameter settings is an important part of the development and application of algorithms. We describe an automatic framework for this algorithm configuration problem. More formally, we provide methods for optimizing a target algorithms performance on a given class of problem instances by varying a set of ordinal and/or categorical parameters. We review a family of local-search-based algorithm configuration procedures and present novel techniques for accelerating them by adaptively limiting the time spent for evaluating individual configurations. We describe the results of a comprehensive experimental evaluation of our methods, based on the configuration of prominent complete and incomplete algorithms for SAT. We also present what is, to our knowledge, the first published work on automatically configuring the CPLEX mixed integer programming solver. All the algorithms we considered had default parameter settings that were manually identified with considerable effort. Nevertheless, using our automated algorithm configuration procedures, we achieved substantial and consistent performance improvements.
パフォーマンスを最適化するパラメータ設定の特定は、アルゴリズムの開発と応用において重要な部分です。本稿では、このアルゴリズム設定問題に対する自動フレームワークについて説明します。より正式には、順序パラメータおよび／またはカテゴリパラメータのセットを変化させることで、特定の問題インスタンスクラスにおける対象アルゴリズムのパフォーマンスを最適化する手法を提供します。局所探索ベースのアルゴリズム設定手順のファミリーをレビューし、個々の設定の評価にかかる時間を適応的に制限することで、これらの手順を高速化する新しい手法を紹介します。SATにおける主要な完全アルゴリズムと不完全アルゴリズムの設定に基づいて、本手法の包括的な実験評価結果について説明します。また、CPLEX混合整数計画ソルバーの自動設定に関する、我々の知る限り初の公開された研究成果も紹介します。検討したすべてのアルゴリズムは、デフォルトのパラメータ設定を手動でかなりの労力をかけて特定していました。それでも、自動化されたアルゴリズム設定手順を使用することで、大幅かつ一貫したパフォーマンス向上を達成しました。
Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem
重み付き最大満足度問題のための緩和サーベイ伝播法
The survey propagation (SP) algorithm has been shown to work well on large instances of the random 3-SAT problem near its phase transition. It was shown that SP estimates marginals over covers that represent clusters of solutions. The SP-y algorithm generalizes SP to work on the maximum satisfiability (Max-SAT) problem, but the cover interpretation of SP does not generalize to SP-y. In this paper, we formulate the relaxed survey propagation (RSP) algorithm, which extends the SP algorithm to apply to the weighted Max-SAT problem. We show that RSP has an interpretation of estimating marginals over covers violating a set of clauses with minimal weight. This naturally generalizes the cover interpretation of SP. Empirically, we show that RSP outperforms SP-y and other state-of-the-art Max-SAT solvers on random Max-SAT instances. RSP also outperforms state-of-the-art weighted Max-SAT solvers on random weighted Max-SAT instances.
調査伝播(SP)アルゴリズムは、ランダム3-SAT問題の相転移付近の大規模なインスタンスでうまく機能することが示されています。SPは、解のクラスターを表す被覆の周辺値を推定することが示されました。SP-yアルゴリズムは、SPを一般化して最大充足可能性(Max-SAT)問題で機能するようにするが、SPの被覆解釈はSP-yには一般化されない。本稿では、SPアルゴリズムを拡張して重み付きMax-SAT問題に適用する、緩和調査伝播(RSP)アルゴリズムを定式化します。RSPには、最小の重みを持つ節のセットに違反する被覆の周辺値を推定するという解釈があることを示す。これにより、SPの被覆解釈が自然に一般化されます。経験的に、RSPは、ランダムMax-SATインスタンスでSP-yやその他の最先端のMax-SATソルバーよりも性能が優れていることを示す。RSPは、ランダムな重み付きMax-SATインスタンスでも最先端の重み付きMax-SATソルバーよりも性能が優れている
Hypertableau Reasoning for Description Logics
記述論理のためのハイパータブロー推論
We present a novel reasoning calculus for the description logic SHOIQ^+—a knowledge representation formalism with applications in areas such as the Semantic Web. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions—a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies.
我々は、セマンティックウェブなどの分野で応用されている知識表現形式である記述論理SHOIQ^+のための新しい推論計算法を提示します。不必要な非決定性と大規模モデルの構築は、最先端の推論システムで使用されているタブローベースの推論計算法における非効率性の2つの主な原因です。非決定性を削減するために、我々はハイパータブロー計算法とハイパーレゾリューション計算法をベースに計算法を構築し、これらをブロッキング条件で拡張して停止を保証します。構築されたモデルのサイズを縮小するために、どこでもペアワイズブロッキングを導入します。また、名詞、逆役割、および数制限が存在する場合でも停止を保証する、改良された名詞導入規則も提示します。これらは、取り扱いが非常に難しいことが証明されているDL構成要素の組み合わせです。我々の実装は、いくつかのよく知られたオントロジー上の最先端の推論システムに比べて大幅なパフォーマンスの向上を示しています。
Content Modeling Using Latent Permutations
潜在順列を用いたコンテンツモデリング
We present a novel Bayesian topic model for learning discourse-level document structure. Our model leverages insights from discourse theory to constrain latent topic assignments in a way that reflects the underlying organization of document topics. We propose a global model in which both topic selection and ordering are biased to be similar across a collection of related documents. We show that this space of orderings can be effectively represented using a distribution over permutations called the Generalized Mallows Model. We apply our method to three complementary discourse-level tasks: cross-document alignment, document segmentation, and information ordering. Our experiments show that incorporating our permutation-based model in these applications yields substantial improvements in performance over previously proposed methods.
談話レベルの文書構造を学習するための新たなベイズトピックモデルを提示します。本モデルは談話理論の知見を活用し、文書トピックの根底にある構成を反映するように、潜在的なトピック割り当てを制約します。本モデルでは、関連文書群全体にわたってトピック選択と順序付けの両方が類似するようにバイアスをかけるグローバルモデルを提案します。この順序付け空間は、一般化マロウズモデルと呼ばれる順列分布を用いて効果的に表現できることを示す。本手法を、文書間アライメント、文書セグメンテーション、情報順序付けという3つの補完的な談話レベルタスクに適用します。実験では、これらのアプリケーションに順列ベースモデルを組み込むことで、従来提案されている手法と比較して大幅な性能向上が得られることが示されました。
The DL-Lite Family and Relations
DL-Liteファミリーと関係
The recently introduced series of description logics under the common moniker `DL-Lite’ has attracted attention of the description logic and semantic web communities due to the low computational complexity of inference, on the one hand, and the ability to represent conceptual modeling formalisms, on the other. The main aim of this article is to carry out a thorough and systematic investigation of inference in extensions of the original DL-Lite logics along five axes: by (i) adding the Boolean connectives and (ii) number restrictions to concept constructs, (iii) allowing role hierarchies, (iv) allowing role disjointness, symmetry, asymmetry, reflexivity, irreflexivity and transitivity constraints, and (v) adopting or dropping the unique same assumption. We analyze the combined complexity of satisfiability for the resulting logics, as well as the data complexity of instance checking and answering positive existential queries. Our approach is based on embedding DL-Lite logics in suitable fragments of the one-variable first-order logic, which provides useful insights into their properties and, in particular, computational behavior.
「DL-Lite」という共通名称で最近導入された一連の記述論理は、推論の計算複雑度の低さと、概念モデリング形式を表現できることから、記述論理およびセマンティックウェブコミュニティの注目を集めています。本稿の主な目的は、オリジナルのDL-Lite論理を拡張した推論を、(i)ブール接続詞の追加、(ii)概念構成への数制限、(iii)役割階層の許容、(iv)役割の素性、対称性、非対称性、反射性、非反射性、推移性の制約の許容、(v)一意な同一性仮定の採用または削除という5つの軸に沿って、徹底的かつ体系的に調査することです。得られた論理の充足可能性の複合的な複雑性と、インスタンスチェックと肯定的存在クエリへの回答におけるデータ複雑性を分析します。本アプローチは、DL-Lite論理を一変数一階述語論理の適切な断片に埋め込むことに基づいており、これにより、論理の特性、特に計算動作に関する有用な知見が得られます。