CUI Networks: A Graphical Representation for Conditional Utility Independence
CUIネットワーク：条件付き効用独立性のグラフィカル表現
We introduce CUI networks, a compact graphical representation of utility functions over multiple attributes. CUI networks model multiattribute utility functions using the well-studied and widely applicable utility independence concept. We show how conditional utility independence leads to an effective functional decomposition that can be exhibited graphically, and how local, compact data at the graph nodes can be used to calculate joint utility. We discuss aspects of elicitation, network construction, and optimization, and contrast our new representation with previous graphical preference modeling.
我々は、複数属性にわたる効用関数を簡潔にグラフィカルに表現するCUIネットワークを導入します。CUIネットワークは、広く研究され、広く適用されている効用独立性の概念を用いて、複数属性の効用関数をモデル化します。条件付き効用独立性が、グラフィカルに表示可能な効果的な機能分解にどのようにつながるか、そしてグラフノードにおける局所的でコンパクトなデータを用いて共同効用を計算する方法を示す。また、誘導、ネットワーク構築、最適化の側面について議論し、我々の新しい表現を従来のグラフィカル選好モデリングと比較します。
A Multiagent Approach to Autonomous Intersection Management
自律交差点管理のためのマルチエージェントアプローチ
Artificial intelligence research is ushering in a new era of sophisticated, mass-market transportation technology. While computers can already fly a passenger jet better than a trained human pilot, people are still faced with the dangerous yet tedious task of driving automobiles. Intelligent Transportation Systems (ITS) is the field that focuses on integrating information technology with vehicles and transportation infrastructure to make transportation safer, cheaper, and more efficient. Recent advances in ITS point to a future in which vehicles themselves handle the vast majority of the driving task. Once autonomous vehicles become popular, autonomous interactions amongst multiple vehicles will be possible. Current methods of vehicle coordination, which are all designed to work with human drivers, will be outdated. The bottleneck for roadway efficiency will no longer be the drivers, but rather the mechanism by which those drivers’ actions are coordinated. While open-road driving is a well-studied and more-or-less-solved problem, urban traffic scenarios, especially intersections, are much more challenging. We believe current methods for controlling traffic, specifically at intersections, will not be able to take advantage of the increased sensitivity and precision of autonomous vehicles as compared to human drivers. In this article, we suggest an alternative mechanism for coordinating the movement of autonomous vehicles through intersections. Drivers and intersections in this mechanism are treated as autonomous agents in a multiagent system. In this multiagent system, intersections use a new reservation-based approach built around a detailed communication protocol, which we also present. We demonstrate in simulation that our new mechanism has the potential to significantly outperform current intersection control technology — traffic lights and stop signs. Because our mechanism can emulate a traffic light or stop sign, it subsumes the most popular current methods of intersection control. This article also presents two extensions to the mechanism. The first extension allows the system to control human-driven vehicles in addition to autonomous vehicles. The second gives priority to emergency vehicles without significant cost to civilian vehicles. The mechanism, including both extensions, is implemented and tested in simulation, and we present experimental results that strongly attest to the efficacy of this approach.
人工知能の研究は、洗練された大衆向け交通技術の新たな時代を切り開きつつあります。コンピューターは既に訓練を受けた人間のパイロットよりも優れた旅客機の操縦を可能にしていますが、自動車の運転という危険で退屈な作業は依然として人間が担っています。高度道路交通システム（ITS）は、情報技術を車両や交通インフラに統合し、交通をより安全、安価、そして効率的にすることに焦点を当てた分野です。ITSの近年の進歩は、車両自体が運転タスクの大部分を処理する未来を示しています。自動運転車が普及すれば、複数の車両間の自律的な相互作用が可能になります。人間のドライバーと連携するように設計された現在の車両協調方法は時代遅れになるでしょう。道路の効率性におけるボトルネックはもはやドライバーではなく、ドライバーの行動を調整するメカニズムになるでしょう。一般道での運転は十分に研究され、ほぼ解決済みの問題ですが、都市交通、特に交差点でははるかに困難な状況が存在します。特に交差点における現在の交通制御方法では、人間のドライバーに比べて自動運転車が持つ高い感度と精度を活用できないと考えています。本稿では、交差点における自動運転車の動きを調整するための代替メカニズムを提案します。このメカニズムでは、ドライバーと交差点は、マルチエージェントシステムにおける自律エージェントとして扱われます。このマルチエージェントシステムでは、交差点は、詳細な通信プロトコルを基盤とした新しい予約ベースのアプローチを採用します。このプロトコルについても解説します。シミュレーションにより、この新しいメカニズムが、現在の交差点制御技術（信号機や一時停止標識）を大幅に上回る性能を発揮する可能性を実証します。このメカニズムは信号機や一時停止標識をエミュレートできるため、現在最も一般的な交差点制御手法を包含します。本稿では、このメカニズムの2つの拡張についても紹介します。1つ目の拡張は、システムが自動運転車に加えて人間が運転する車両も制御できるようにするものです。2つ目の拡張は、民間車両に大きな負担をかけることなく、緊急車両を優先させるものです。この2つの拡張を含むメカニズムは、シミュレーションで実装・テストされ、このアプローチの有効性を強く証明する実験結果を示します。
Creating Relational Data from Unstructured and Ungrammatical Data Sources
非構造化および非文法的データソースからの関係データの作成
In order for agents to act on behalf of users, they will have to retrieve and integrate vast amounts of textual data on the World Wide Web. However, much of the useful data on the Web is neither grammatical nor formally structured, making querying difficult. Examples of these types of data sources are online classifieds like Craigslist and auction item listings like eBay. We call this unstructured, ungrammatical data “posts.” The unstructured nature of posts makes query and integration difficult because the attributes are embedded within the text. Also, these attributes do not conform to standardized values, which prevents queries based on a common attribute value. The schema is unknown and the values may vary dramatically making accurate search difficult. Creating relational data for easy querying requires that we define a schema for the embedded attributes and extract values from the posts while standardizing these values. Traditional information extraction (IE) is inadequate to perform this task because it relies on clues from the data, such as structure or natural language, neither of which are found in posts. Furthermore, traditional information extraction does not incorporate data cleaning, which is necessary to accurately query and integrate the source. The two-step approach described in this paper creates relational data sets from unstructured and ungrammatical text by addressing both issues. To do this, we require a set of known entities called a “reference set.” The first step aligns each post to each member of each reference set. This allows our algorithm to define a schema over the post and include standard values for the attributes defined by this schema. The second step performs information extraction for the attributes, including attributes not easily represented by reference sets, such as a price. In this manner we create a relational structure over previously unstructured data, supporting deep and accurate queries over the data as well as standard values for integration. Our experimental results show that our technique matches the posts to the reference set accurately and efficiently and outperforms state-of-the-art extraction systems on the extraction task from posts.
エージェントがユーザーに代わって行動するためには、ワールドワイドウェブ上の膨大な量のテキストデータを取得し、統合する必要があります。しかし、Web上の有用なデータの多くは文法的にも形式的にも構造化されておらず、クエリの実行が困難です。このようなデータソースの例としては、Craigslistのようなオンラインクラシファイド広告やeBayのようなオークション商品リストなどが挙げられます。私たちは、この非構造化かつ非文法的データを「投稿」と呼びます。投稿の非構造化の性質により、属性がテキスト内に埋め込まれているため、クエリの実行と統合が困難になります。また、これらの属性は標準化された値に準拠していないため、共通の属性値に基づくクエリの実行が困難になります。スキーマが不明で、値が大きく変化する可能性があるため、正確な検索が困難です。クエリを容易に実行できるリレーショナルデータを作成するには、埋め込まれた属性のスキーマを定義し、投稿から値を抽出する際にこれらの値を標準化する必要があります。従来の情報抽出（IE）は、構造や自然言語といったデータからの手がかりに依存しており、投稿にはこれらの手がかりがないため、このタスクを実行するには不十分です。さらに、従来の情報抽出には、ソースを正確にクエリして統合するために必要なデータクリーニングが組み込まれていません。本論文で説明する2段階アプローチは、非構造化かつ非文法的テキストの両方の問題に対処することで、リレーショナルデータセットを作成します。そのためには、「参照セット」と呼ばれる既知のエンティティの集合が必要です。最初のステップでは、各投稿を各参照セットの各メンバーにアラインメントします。これにより、アルゴリズムは投稿のスキーマを定義し、このスキーマによって定義された属性の標準値を含めることができます。2番目のステップでは、価格など参照セットでは簡単に表現できない属性も含め、属性の情報抽出を行います。このようにして、以前は非構造化されていたデータにリレーショナル構造を作成し、データに対する深く正確なクエリと統合のための標準値をサポートします。実験結果では、この手法が投稿を参照セットに正確かつ効率的にマッチングし、投稿からの抽出タスクにおいて最先端の抽出システムよりも優れた性能を発揮することがわかりました。
Exploiting Subgraph Structure in Multi-Robot Path Planning
マルチロボット経路計画におけるサブグラフ構造の活用
Multi-robot path planning is difficult due to the combinatorial explosion of the search space with every new robot added. Complete search of the combined state-space soon becomes intractable. In this paper we present a novel form of abstraction that allows us to plan much more efficiently. The key to this abstraction is the partitioning of the map into subgraphs of known structure with entry and exit restrictions which we can represent compactly. Planning then becomes a search in the much smaller space of subgraph configurations. Once an abstract plan is found, it can be quickly resolved into a correct (but possibly sub-optimal) concrete plan without the need for further search. We prove that this technique is sound and complete and demonstrate its practical effectiveness on a real map.A contending solution, prioritised planning, is also evaluated and shown to have similar performance albeit at the cost of completeness. The two approaches are not necessarily conflicting; we demonstrate how they can be combined into a single algorithm which outperforms either approach alone.
マルチロボットの経路計画は、新しいロボットが追加されるたびに探索空間の組み合わせ爆発のために困難です。結合された状態空間を完全に探索することは、すぐに困難になります。本論文では、より効率的な計画を可能にする新しい抽象化形式を提示します。この抽象化の鍵となるのは、マップを、入口と出口の制約を持つ既知の構造を持つサブグラフに分割することです。これらの制約は、コンパクトに表現できます。これにより、計画は、はるかに小さなサブグラフ構成空間における探索になります。抽象的な計画が見つかると、それ以上の探索を必要とせずに、正しい（ただし、おそらく最適ではない）具体的な計画に迅速に解決できます。この手法が健全かつ完全であることを証明し、実際のマップ上での実用的な有効性を実証します。競合する解決策である優先順位付け計画も評価し、完全性を犠牲にするものの、同様の性能を示すことが示されています。2つのアプローチは必ずしも矛盾するものではありません。これらを単一のアルゴリズムに組み合わせることで、どちらか一方のアプローチのみよりも優れた性能を発揮する方法を示します。
Axiomatic Foundations for Ranking Systems
ランキングシステムの公理的基盤
Reasoning about agent preferences on a set of alternatives, and the aggregation of such preferences into some social ranking is a fundamental issue in reasoning about multi-agent systems. When the set of agents and the set of alternatives coincide, we get the ranking systems setting. A famous type of ranking systems are page ranking systems in the context of search engines. In this paper we present an extensive axiomatic study of ranking systems. In particular, we consider two fundamental axioms: Transitivity, and Ranked Independence of Irrelevant Alternatives. Surprisingly, we find that there is no general social ranking rule that satisfies both requirements. Furthermore, we show that our impossibility result holds under various restrictions on the class of ranking problems considered. However, when transitivity is weakened, an interesting possibility result is obtained. In addition, we show a complete axiomatization of approval voting using ranked IIA.
選択肢の集合に対するエージェントの選好についての推論、そしてそのような選好を何らかの社会的ランキングに集約することは、マルチエージェントシステムの推論における基本的な問題です。エージェントの集合と選択肢の集合が一致するとき、ランキングシステムの設定が得られます。ランキングシステムの有名なタイプとしては、検索エンジンのコンテキストにおけるページランキングシステムがあります。本稿では、ランキングシステムに関する広範な公理的研究を提示します。特に、推移性と無関係な選択肢のランク付けされた独立性という2つの基本公理を考察します。驚くべきことに、両方の要件を満たす一般的な社会的ランキングルールは存在しないことがわかった。さらに、検討対象のランキング問題のクラスに対する様々な制約の下で、我々の不可能性の結果が成り立つことを示す。しかし、推移性を弱めると、興味深い可能性の結果が得られた。さらに、ランク付けされたIIAを用いた承認投票の完全な公理化を示す。
First Order Decision Diagrams for Relational MDPs
関係MDPのための一次決定図
Markov decision processes capture sequential decision making under uncertainty, where an agent must choose actions so as to optimize long term reward. The paper studies efficient reasoning mechanisms for Relational Markov Decision Processes (RMDP) where world states have an internal relational structure that can be naturally described in terms of objects and relations among them. Two contributions are presented. First, the paper develops First Order Decision Diagrams (FODD), a new compact representation for functions over relational structures, together with a set of operators to combine FODDs, and novel reduction techniques to keep the representation small. Second, the paper shows how FODDs can be used to develop solutions for RMDPs, where reasoning is performed at the abstract level and the resulting optimal policy is independent of domain size (number of objects) or instantiation. In particular, a variant of the value iteration algorithm is developed by using special operations over FODDs, and the algorithm is shown to converge to the optimal policy.
マルコフ決定過程は、不確実性下での逐次的な意思決定を捉えるものであり、エージェントは長期的な報酬を最適化するように行動を選択しなければならない。本論文では、世界状態がオブジェクトとそれらの関係の観点から自然に記述できる内部関係構造を持つ関係マルコフ決定プロセス(RMDP)の効率的な推論メカニズムについて検討します。2つの貢献が示されています。まず、関係構造上の関数の新しいコンパクトな表現であるFODD (First Order Decision Diagrams)を、FODDを組み合わせる演算子のセットと、表現を小さく保つための新しい削減手法とともに開発します。次に、推論が抽象レベルで実行され、結果として得られる最適なポリシーがドメイン サイズ(オブジェクト数)やインスタンス化に依存しないRMDPのソリューションを開発するためにFODDを使用する方法を示します。特に、FODD上の特別な演算を使用して値反復アルゴリズムのバリアントが開発され、アルゴリズムが最適なポリシーに収束することが示されています。
Global Inference for Sentence Compression: An Integer Linear Programming Approach
文圧縮のための大域的推論：整数線形計画法によるアプローチ
Sentence compression holds promise for many applications ranging from summarization to subtitle generation. Our work views sentence compression as an optimization problem and uses integer linear programming (ILP) to infer globally optimal compressions in the presence of linguistically motivated constraints. We show how previous formulations of sentence compression can be recast as ILPs and extend these models with novel global constraints. Experimental results on written and spoken texts demonstrate improvements over state-of-the-art models.
文の圧縮は、要約から字幕生成に至るまで、多くの応用に期待が寄せられています。本研究では、文の圧縮を最適化問題と捉え、整数線形計画法（ILP）を用いて、言語的制約が存在する状況下で、大域的に最適な圧縮を推論します。従来の文の圧縮の定式化をILPとして再構成し、これらのモデルを新たな大域的制約で拡張する方法を示す。書き言葉と話し言葉のテキストを用いた実験結果は、最先端のモデルを上回る改善を示しています。
Gesture Salience as a Hidden Variable for Coreference Resolution and Keyframe Extraction
共参照解決とキーフレーム抽出のための隠れ変数としてのジェスチャーの顕著性
Gesture is a non-verbal modality that can contribute crucial information to the understanding of natural language. But not all gestures are informative, and non-communicative hand motions may confuse natural language processing (NLP) and impede learning. People have little diffculty ignoring irrelevant hand movements and focusing on meaningful gestures, suggesting that an automatic system could also be trained to perform this task. However, the informativeness of a gesture is context-dependent and labeling enough data to cover all cases would be expensive. We present conditional modality fusion, a conditional hidden-variable model that learns to predict which gestures are salient for coreference resolution, the task of determining whether two noun phrases refer to the same semantic entity. Moreover, our approach uses only coreference annotations, and not annotations of gesture salience itself. We show that gesture features improve performance on coreference resolution, and that by attending only to gestures that are salient, our method achieves further significant gains. In addition, we show that the model of gesture salience learned in the context of coreference accords with human intuition, by demonstrating that gestures judged to be salient by our model can be used successfully to create multimedia keyframe summaries of video. These summaries are similar to those created by human raters, and significantly outperform summaries produced by baselines from the literature.
ジェスチャーは、自然言語理解に重要な情報を提供できる非言語的モダリティです。しかし、すべてのジェスチャーが有益な情報を提供するわけではなく、非コミュニケーション的な手振りは自然言語処理（NLP）を混乱させ、学習を妨げる可能性があります。人間は、無関係な手振りを無視し、意味のあるジェスチャーに集中することにほとんど困難を感じないため、自動システムもこのタスクを実行できるように訓練できる可能性があります。しかし、ジェスチャーの情報価値は状況依存であり、すべてのケースをカバーするのに十分なデータをラベル付けするにはコストがかかります。本研究では、条件付きモダリティ融合を提案します。これは、2つの名詞句が同じ意味的実体を参照しているかどうかを判断するタスクである共参照解決において、どのジェスチャーが顕著であるかを予測する学習を行う条件付き隠れ変数モデルです。さらに、本手法では、共参照アノテーションのみを使用し、ジェスチャーの顕著性自体のアノテーションは使用しません。ジェスチャーの特徴が共参照解決のパフォーマンスを向上させること、そして顕著なジェスチャーのみに注意を払うことで、本手法がさらに大きな効果を発揮することを示します。さらに、共参照の文脈で学習したジェスチャーの顕著性モデルが人間の直感と一致することを示す。具体的には、本モデルによって顕著と判断されたジェスチャーを用いて、動画のマルチメディアキーフレーム要約を作成できることを実証します。これらの要約は、人間の評価者が作成した要約と類似しており、文献のベースラインによって生成された要約を大幅に上回る性能を示した。
Planning with Durative Actions in Stochastic Domains
確率的領域における持続的アクションを伴うプランニング
Probabilistic planning problems are typically modeled as a Markov Decision Process (MDP). MDPs, while an otherwise expressive model, allow only for sequential, non-durative actions. This poses severe restrictions in modeling and solving a real world planning problem. We extend the MDP model to incorporate 1) simultaneous action execution, 2) durative actions, and 3) stochastic durations. We develop several algorithms to combat the computational explosion introduced by these features. The key theoretical ideas used in building these algorithms are — modeling a complex problem as an MDP in extended state/action space, pruning of irrelevant actions, sampling of relevant actions, using informed heuristics to guide the search, hybridizing different planners to achieve benefits of both, approximating the problem and replanning. Our empirical evaluation illuminates the different merits in using various algorithms, viz., optimality, empirical closeness to optimality, theoretical error bounds, and speed.
確率的計画問題は、通常、マルコフ決定過程（MDP）としてモデル化されます。MDPは、表現力豊かなモデルである一方、連続的で非持続的なアクションしか許容しない。これは、現実世界の計画問題のモデル化と解決に厳しい制約を課す。MDPモデルを拡張し、1)同時アクション実行、2)持続アクション、3)確率的持続を組み込む。これらの特徴によって生じる計算量爆発に対処するため、複数のアルゴリズムを開発します。これらのアルゴリズム構築に用いられる主要な理論的アイデアは、複雑な問題を拡張状態/アクション空間におけるMDPとしてモデル化すること、無関係なアクションの枝刈り、関連アクションのサンプリング、情報に基づくヒューリスティックを用いた探索の誘導、異なるプランナーをハイブリッド化して両方の利点を実現すること、問題の近似化と再計画です。我々の実証的評価は、様々なアルゴリズムを用いることの異なるメリット、すなわち、最適性、最適性への経験的近似度、理論的な誤差範囲、そして速度を明らかにします。
The Complexity of Planning Problems With Simple Causal Graphs
単純な因果グラフを用いたプランニング問題の複雑性
We present three new complexity results for classes of planning problems with simple causal graphs. First, we describe a polynomial-time algorithm that uses macros to generate plans for the class 3S of planning problems with binary state variables and acyclic causal graphs. This implies that plan generation may be tractable even when a planning problem has an exponentially long minimal solution. We also prove that the problem of plan existence for planning problems with multi-valued variables and chain causal graphs is NP-hard. Finally, we show that plan existence for planning problems with binary state variables and polytree causal graphs is NP-complete.
我々は、単純な因果グラフを持つ計画問題のクラスについて、3つの新しい計算量結果を提示します。まず、マクロを用いて、バイナリ状態変数と非巡回因果グラフを持つクラス3Sの計画問題に対する計画を生成する多項式時間アルゴリズムについて説明します。これは、計画問題が指数的に長い最小解を持つ場合でも、計画生成が扱いやすい可能性があることを意味しています。また、多値変数と連鎖因果グラフを持つ計画問題における計画存在の問題がNP困難であることを証明した。最後に、バイナリ状態変数とポリツリー因果グラフを持つ計画問題における計画存在の問題がNP完全であることを示す。
Modular Reuse of Ontologies: Theory and Practice
オントロジーのモジュール再利用：理論と実践
In this paper, we propose a set of tasks that are relevant for the modular reuse of ontologies. In order to formalize these tasks as reasoning problems, we introduce the notions of conservative extension, safety and module for a very general class of logic-based ontology languages. We investigate the general properties of and relationships between these notions and study the relationships between the relevant reasoning problems we have previously identified. To study the computability of these problems, we consider, in particular, Description Logics (DLs), which provide the formal underpinning of the W3C Web Ontology Language (OWL), and show that all the problems we consider are undecidable or algorithmically unsolvable for the description logic underlying OWL DL. In order to achieve a practical solution, we identify conditions sufficient for an ontology to reuse a set of symbols “safely”—that is, without changing their meaning. We provide the notion of a safety class, which characterizes any sufficient condition for safety, and identify a family of safety classes–called locality—which enjoys a collection of desirable properties. We use the notion of a safety class to extract modules from ontologies, and we provide various modularization algorithms that are appropriate to the properties of the particular safety class in use. Finally, we show practical benefits of our safety checking and module extraction algorithms.
本稿では、オントロジーのモジュール再利用に関連する一連のタスクを提案します。これらのタスクを推論問題として形式化するために、非常に一般的なクラスの論理ベースオントロジー言語に対して、保守的拡張、安全性、モジュールの概念を導入します。これらの概念の一般的な特性とそれらの関係性を調査し、これまでに特定した関連する推論問題間の関係性を考察します。これらの問題の計算可能性を考察するため、特にW3Cウェブオントロジー言語（OWL）の形式的な基盤となる記述論理（DL）を考察し、考察するすべての問題がOWL DLの基盤となる記述論理では決定不能、すなわちアルゴリズム的に解決不可能であることを示す。実用的な解決策を実現するために、オントロジーが記号集合を「安全に」（つまり、意味を変えずに）再利用するための十分な条件を特定します。安全性の十分な条件を特徴付ける「安全性クラス」の概念を提示し、望ましい特性を持つ「局所性」と呼ばれる安全性クラスのファミリーを特定します。安全性クラスの概念を用いてオントロジーからモジュールを抽出し、使用する特定の安全性クラスの特性に適した様々なモジュール化アルゴリズムを提供します。最後に、安全性チェックおよびモジュール抽出アルゴリズムの実用的な利点を示す。
On the Expressiveness of Levesque’s Normal Form
Levesque正規形の表現力について
Levesque proposed a generalization of a database called a proper knowledge base (KB), which is equivalent to a possibly infinite consistent set of ground literals. In contrast to databases, proper KBs do not make the closed-world assumption and hence the entailment problem becomes undecidable. Levesque then proposed a limited but efficient inference method V for proper KBs, which is sound and, when the query is in a certain normal form, also logically complete. He conjectured that for every first-order query there is an equivalent one in normal form. In this note, we show that this conjecture is false. In fact, we show that any class of formulas for which V is complete must be strictly less expressive than full first-order logic. Moreover, in the propositional case it is very unlikely that a formula always has a polynomial-size normal form.
Levesqueは、固有知識ベース（KB）と呼ばれるデータベースの一般化を提案した。これは、おそらく無限の一貫性のあるグラウンドリテラルの集合に相当します。データベースとは対照的に、適切なKBは閉世界仮定を行わないため、含意問題は決定不能となります。そこでLevesqueは、適切なKBに対して限定的だが効率的な推論法Vを提案した。これは健全であり、クエリが特定の正規形である場合は論理的に完全でもあります。彼は、すべての一階述語クエリに対して、それと同等の正規形のクエリが存在すると予想した。本稿では、この予想が誤りであることを示す。実際、Vが完全であるような式のクラスはどれも、完全な一階述語論理よりも厳密に表現力が劣ることを示す。さらに、命題論理の場合、式が常に多項式サイズの正規形を持つことは非常にまれです。
Loosely Coupled Formulations for Automated Planning: An Integer Programming Perspective
自動プランニングのための疎結合定式化：整数計画論的観点
We represent planning as a set of loosely coupled network flow problems, where each network corresponds to one of the state variables in the planning domain. The network nodes correspond to the state variable values and the network arcs correspond to the value transitions. The planning problem is to find a path (a sequence of actions) in each network such that, when merged, they constitute a feasible plan. In this paper we present a number of integer programming formulations that model these loosely coupled networks with varying degrees of flexibility. Since merging may introduce exponentially many ordering constraints we implement a so-called branch-and-cut algorithm, in which these constraints are dynamically generated and added to the formulation when needed. Our results are very promising, they improve upon previous planning as integer programming approaches and lay the foundation for integer programming approaches for cost optimal planning.
我々は、計画を疎結合ネットワークフロー問題の集合として表現します。各ネットワークは、計画ドメイン内の状態変数の1つに対応します。ネットワークノードは状態変数の値に対応し、ネットワークアークは値の遷移に対応します。計画問題は、各ネットワークにおいて、それらをマージしたときに実行可能な計画を構成するパス（一連のアクション）を見つけることです。本稿では、これらの疎結合ネットワークを様々な柔軟性でモデル化する整数計画定式化をいくつか提示します。マージによって指数関数的に多くの順序制約が導入される可能性があるため、いわゆる分岐切断アルゴリズムを実装します。このアルゴリズムでは、これらの制約は必要に応じて動的に生成され、定式化に追加されます。我々の結果は非常に有望であり、整数計画アプローチとしての従来の計画を改善し、コスト最適計画のための整数計画アプローチの基礎を築くものです。
Sound and Complete Inference Rules for SE-Consequence
SE-Consequenceのための健全かつ完全な推論規則
The notion of strong equivalence on logic programs with answer set semantics gives rise to a consequence relation on logic program rules, called SE-consequence. We present a sound and complete set of inference rules for SE-consequence on disjunctive logic programs.
解答集合意味論を持つ論理プログラムにおける強同値性の概念は、論理プログラム規則における帰結関係、いわゆるSE帰結を導きます。選言的論理プログラムにおけるSE帰結に関する、健全かつ完全な推論規則の集合を提示します。
Conjunctive Query Answering for the Description Logic SHIQ
記述論理SHIQのための連言クエリ応答
Conjunctive queries play an important role as an expressive query language for Description Logics (DLs). Although modern DLs usually provide for transitive roles, conjunctive query answering over DL knowledge bases is only poorly understood if transitive roles are admitted in the query. In this paper, we consider unions of conjunctive queries over knowledge bases formulated in the prominent DL SHIQ and allow transitive roles in both the query and the knowledge base. We show decidability of query answering in this setting and establish two tight complexity bounds: regarding combined complexity, we prove that there is a deterministic algorithm for query answering that needs time single exponential in the size of the KB and double exponential in the size of the query, which is optimal. Regarding data complexity, we prove containment in co-NP.
結合クエリは、記述論理（DL）の表現力豊かなクエリ言語として重要な役割を果たしています。現代のDLは通常、推移的役割を提供するが、DL知識ベース上の結合クエリ回答は、クエリに推移的役割が認められる場合にのみ十分に理解されています。本稿では、著名なDL SHIQで定式化された知識ベース上の結合クエリの和集合を考察し、クエリと知識ベースの両方で推移的役割を許容します。この設定において、クエリ応答の決定可能性を示し、2つの厳密な計算量限界を確立します。複合計算量に関しては、KBサイズの1指数関数、クエリサイズの2指数関数の時間を要する、最適なクエリ応答決定論的アルゴリズムが存在することを証明します。データ計算量に関しては、co-NPにおける包含性を証明します。
CTL Model Update for System Modifications
システム変更のためのCTLモデル更新
Model checking is a promising technology, which has been applied for verification of many hardware and software systems. In this paper, we introduce the concept of model update towards the development of an automatic system modification tool that extends model checking functions. We define primitive update operations on the models of Computation Tree Logic (CTL) and formalize the principle of minimal change for CTL model update. These primitive update operations, together with the underlying minimal change principle, serve as the foundation for CTL model update. Essential semantic and computational characterizations are provided for our CTL model update approach. We then describe a formal algorithm that implements this approach. We also illustrate two case studies of CTL model updates for the well-known microwave oven example and the Andrew File System 1, from which we further propose a method to optimize the update results in complex system modifications.
モデル検査は有望な技術であり、多くのハードウェアおよびソフトウェアシステムの検証に適用されています。本稿では、モデル検査機能を拡張する自動システム修正ツールの開発に向けて、モデル更新の概念を紹介します。我々は計算木論理（CTL）モデル上で基本的な更新操作を定義し、CTLモデル更新における最小変更原理を形式化します。これらの基本的な更新操作は、基礎となる最小変更原理と共に、CTLモデル更新の基礎となります。我々のCTLモデル更新アプローチについて、本質的な意味的および計算的特性を提供します。次に、このアプローチを実装する形式アルゴリズムについて説明します。また、よく知られている電子レンジの例とAndrew File System 1の2つのCTLモデル更新のケーススタディを示し、そこから複雑なシステム変更における更新結果を最適化する手法を提案します。
MiniMaxSAT: An Efficient Weighted Max-SAT solver
MiniMaxSAT：効率的な重み付きMax-SATソルバー
In this paper we introduce MiniMaxSat, a new Max-SAT solver that is built on top of MiniSat+. It incorporates the best current SAT and Max-SAT techniques. It can handle hard clauses(clauses of mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost as in Max-SAT) as well as pseudo-boolean objective functions and constraints. Its main features are: learning and backjumping on hard clauses; resolution-based and substraction-based lower bounding; and lazy propagation with the two-watched literal scheme. Our empirical evaluation comparing a wide set of solving alternatives on a broad set of optimization benchmarks indicates that the performance of MiniMaxSat is usually close to the best specialized alternative and, in some cases, even better.
本稿では、MiniSat+をベースに構築された新しいMax-SATソルバーであるMiniMaxSatを紹介します。このソルバーは、最新のSATおよびMax-SAT技術を組み込んでいます。ハード節（SATのように必須の充足節）、ソフト節（Max-SATのように偽造にコストがかかる節）、擬似ブール型の目的関数と制約を処理できます。主な機能は、ハード節の学習とバックジャンプ、解決ベースおよび減算ベースの下限設定、2つのウォッチド・リテラル・スキームによる遅延伝播です。幅広い最適化ベンチマークで多様な解決方法を比較した経験的評価では、MiniMaxSatのパフォーマンスは通常、最も優れた特化方法に近いことが示されており、場合によってはさらに優れていることもあります。