論理と推論の理論, 実装, 応用に関する合同セミナー

ERATO湊離散構造処理系プロジェクトは2010年4月より本格的な研究活動を開始して、今年で4年目に入った。本プロジェクトは開放的な組織運営により、多様な研究者・技術者が集う場を形成しており、これまでに、学術的成果のみでなく、小中高生や一般市民の注目を集める成果や、社会的に重要な応用事例など、当初予想していなかったような多様な研究成果が得られている。本講演では、本プロジェクトの近況と今後の展望について述べる。

共同研究者: 番原睦則，宋剛秀 (神戸大学)

制約充足問題をSATに符号化する手法には，直接符号化，支持符号化，対数符号化，順序符号化，コンパクト順序符号化などがある．本講演では，いくつかの制約充足問題を例題として各種SAT符号化の概要を解説し，特に順序符号化の特徴について述べる．また，制約モデリングによる違いについても言及する．

SAT問題を制約を利用して効率的に解くというポリシーの下、九州大学大学院システム情報科学研究院長谷川・藤田研究室で行った研究の主な成果を三部構成で紹介する．

[Part1] モデル生成型SATソルバー
1階の極小モデル生成器MM-MGTPを命題に特化したMiniMGを開発した．MiniMGでは，違反節に基づく多分岐や分岐仮定による極小モデル生成を特長とするMGTPと，学習節やリスタート等の最新のSAT技術を備えたDPLL型ソルバーMiniSatの融合を図っている．SATベンチマークに対する極小モデルの全解探索実験では，MiniMGはMGTPを凌駕したが，入力節の正選言でしか分岐しないため，うまい変数順序が選べず性能が低下する問題があった．これを解決するため，学習節をある基準の下で分岐に利用し，削除する方式を考案した．SAT Competition, SATRACEの問題から抽出した303問を用いた評価実験の結果，上記に基づく改良版MiniMGは，従来のMiniMGよりも13問，また，MiniSat2.0よりも4問多く解くことができ，通常のSATソルバーとしても十分通用することが分かった．

[Part2] MaxSATソルバー
多くの制約充足問題はSAT問題に変換して解くことができるが，とりわけ基数制約は重要である。基数制約の代表的CNF符号化方式として，BailleuxらによるTotalizer (TO) とAsinらによるHalf Sorting Network (HS) がある．TOは1進数表現の整数を用いており，生成される節数は \(O(n^{2})\) ，変数数は \(O(n ~ \log ~ n)\) である．HSは odd-even merge に基づいており，生成される節数および変数数はともに \(O(n ~ \log^{2} ~ n)\) である．我々はこれまで，TO をベースとした部分MaxSATソルバーQMaxSATを開発してきた．このK-基数版はMaxSAT2012の部分MaxSAT部門Industrial，Crafted分野で優勝した．TOは変数数の点でHSより優れているが，節数の点では著しく劣る．これを克服するため，modulo計算に基づくModulo Totalizer (MTO) を考案した．法 \(p=n^{1/2}\) のとき，MTOの節数は \(O(n^{3/2})\) ，変数数は \(O(n ~ \log ~ n)\) である．
[速報] MTO版QMaxSatはMaxSAT2013の部分MaxSAT部門Industrial分野で２位に入賞．

[Part3] 未解決問題に挑戦
我々は，ICOTプロジェクトの頃から自動定理証明技術の応用として組合せ最適化問題等の未解決問題に取組んでいる．制約を扱うCMGTPを用い，1993年に準群に関する未解決問題 (QG5-16) を解くことに成功した．その後，MiniSaT及び並列計算環境を利用することにより，2009年にはさらに高次のQG5-18の解決に成功した．この結果を受け，より困難な未解決問題としてラムゼー数に関する挑戦を開始した．ソルバー技術，制約技法等について試行錯誤の結果，2012年にラムゼー数R(4,8)の下界更新に成功した．成功の要因は，問題に固有の対称性等，適切な補助制約の推察・発見とその利用である．ここで採られた，制約緩和技術をSCSatとしてツール化し，さらなる未解決問題探求に向け，改良を進めている．

A grand challenge in computing is to establish a substrate computational model that encompasses diverse forms of non-sequential computation. This talk demonstrates how a hypergraph rewriting framework nicely integrates various forms and ingredients of concurrent computation. Specifically, we show how fine-grained strong reduction of the lambda calculus can be concisely encoded into hypergraph rewriting with a small set of primitive operations.

The whole framework has been embodied as our publicly available HyperLMNtal language and system that evolved into a parallel LTL model checker. The strengths of our HyperLMNtal model checker are its powerful data structures with a symmetry reduction mechanism, highly nondeterministic computation it can express, and little discrepancy between programming and modeling languages. The implementation achieved high scalability and can handle models with half billion states.

Unlike black-box approaches to model checking, the visualizer of LaViT turned out to be extremely useful in analyzing and understanding models by state space browsing. The talk will be given with live demos of examples taken from various fields of computing.

ある環境に存在する人間の集団に対して，集団としての意思決定のメカニズム／制度を導入すると，何らかの社会的な結果が得られる．望ましい結果を得るためのメカニズムの設計方法に関する研究は，メカニズムデザイン／制度設計と呼ばれ，ゲーム理論／ミクロ経済学の一分野として活発な研究が行われている．メカニズムデザインに関する著名な研究成果として，1996 年にノーベル経済学賞を受賞したW. Vickrey による第二価格入札に関する研究がある．従来，第二価格入札は理論的に優れた性質を持つにも関わらず，広く用いられるには至らなかった．ところが，近年，検索エンジンでのキーワード広告において，第二価格入札が用いられるようになり，今や第二価格入札は世界中でもっとも頻繁に実行されている入札方式となっている．
従来，このような望ましい結果を得るためのメカニズムは人手により開発されてきたが，メカニズム設計をある種の最適化問題として表現し，望ましい性質を持つメカニズムを自動的に生成しようとする研究が行われている (自動メカニズムデザイン). 本講演では，メカニズムデザイン，および自動メカニズムデザインに関して概説し，機械学習や法則発見等の研究との関連について議論する．

マルチエージェントシステム（MAS: Multi-Agent Systems）における多くの問題は、あるまとまりをもった構成要素が互いに疎に結合された制約問題として記述することができる。本発表では、そのような制約問題を、緩和（Relax）して分解（Decompose）した後に調整（Coordinate）して解くという解法の枠組みを紹介し、MASの問題への主な適用例を述べる。

共同研究者: 山本泰生

本講演では，まず，データストリーム中の頻出な系列やアイテム集合のオンライン型マイニングのアルゴリズムについて簡単に紹介し，次に我々が開発した「データバーストを伴うストリームを固定容量のメモリでマイニングする近似アルゴリズム」を紹介する。更に時間が許せば，負の相関ルールマイニングの現状と我々のアプローチについても紹介させて頂く。

ブーリアンネットワーク (BN) やセルオートマトン (CA) を含む動的な系の論理モデルに関する推論と学習について講演する．これらの系は標準論理プログラム (NLP) を用いて表現でき，プログラムの各ルールは状態遷移規則を表している．また，NLP の T_P オペレーターは状態の同期更新に相当しており，系のアトラクターは NLP の支持クラス意味論を用いて表される．さらに，状態遷移の観測列を入力とし，NLP で表される系を学習するアルゴリズムを開発し，BN や CA の学習に応用している．

Katsumi Inoue (National Institute of Informatics)

We study inference and learning of logic-based dynamic systems including Boolean networks (BNs) and cellular automata (CAs). We first show that these systems can be expressed as normal logic programs (NLPs), which are regarded as sets of state transition rules.
On the inference side, the supported model semantics of NLPs can characterize point attractors of BNs, and supported classes of NLPs represent periodic oscillation induced by the T_P operator, which can characterize cycle attractors of BNs.
On the leaning side, given a set of pairs of interpretations (I,J) such that J=T_P(I), we infer the program P. This framework can be applied to infer BNs from basins of attraction and to identify CAs by observing transitions of configurations.

共同研究者: 亀谷由隆 (名城大学)

確率モデルにもとづく統計的機械学習では、不変な構造（グラフなど）に確率パラメータを持たせ、データからパラメータを学習することにより、現実に合うモデルを構築する。
本講演では不変な構造として論理を選び、論理に確率を加えたモデリング言語による機械学習について、可能多世界意味論から命題論理による確率計算とパラメータ学習まで概説する。

共同研究者: 田村直之, 番原睦則 (神戸大学), Daniel Le Berre, and Stéphanie Roussel (CRIL)

ScarabはSAT型制約プログラミングシステム開発者を対象に高い表現力，変更容易性，効率性を備えたワークベンチを提供することを目的としたツールである．主に制約プログラミングのためのドメイン特化言語, SAT符号化モジュール, SATソルバーへのインターフェースから構成されており，特にSATソルバーSat4jに対する API を使用することにより，インクリメンタル SAT解法などのSAT解法技術を実現可能である．
本発表では，いくつかの例を用いて Scarab の特長について説明を行う．

共同研究者: 岩沼宏治 (山梨大学), 井上克巳 (国立情報学研究所)

SAT 2013 Competition に参加した GlueMiniSat 2.2.7 の概要と結果について報告する．GlueMiniSat 2.2.7 の特徴は，binary resolvents を利用した軽量な節簡単化手法にある．また，矛盾発生速度の向上を目的としたリスタート戦略や，真偽値割り当てが急速に成長した場合にリスタートを保留する戦略も導入している．本発表では，これらの概要について紹介する．

基数制約のSAT符号化を利用して実装されているQwMaxSATについて報告する．QwMaxSATは，重みなし部分MaxSAT問題に対して高い性能を示すQMaxSATのSAT符号化部分を別の符号化方式に代えたものである．重みつきMaxSAT問題を解くには，巨大な基数を扱う必要があり，arc consistencyを満たさないSAT符号化を採用した．本発表では，これらの概要とQMaxSATとの性能比較について述べる．

共同研究者: 長谷川隆三，越村三幸 (九州大学)

ソフト制約を用いて探索誘導を行うSCSatの概要と成果について報告する．適切なソフト制約が与えられれば，稀少な充足解への効率的な探索誘導が可能となる．ソフト制約が強すぎる場合には，緩和と探索再開が自動的に行われる．これにより，ラムゼーグラフRG(4,8,57)を発見し，ラムゼー数R(4,8)の最良下界を56から58に更新することに成功した．本発表では，これらの概要について紹介する．