Boolean Satisfiability Encoding and Solving
flowchart TD
CNF["$$(\textcolor{red}{\neg a}\lor b)\land(\textcolor{red}{\neg a}\lor\neg b)\land(b\lor c)\land(a\lor\neg c)$$"]
A(( )) --> |"$$a$$"| B(( ))
A --> |"$$\neg a$$"| C(( ))
B --> |"$$b$$"| D(( ))
B --> |"$$\neg b$$"| E(( ))
C --> |"$$b$$"| F(( ))
C --> |"$$\neg b$$"| G(( ))
D --> |"$$c$$"| H(( ))
D --> |"$$\neg c$$"| I(( ))
E --> |"$$c$$"| J(( ))
E --> |"$$\neg c$$"| K(( ))
F --> |"$$c$$"| L(( ))
F --> |"$$\neg c$$"| M(( ))
G --> |"$$c$$"| N(( ))
G --> |"$$\neg c$$"| O(( ))
style CNF fill:none,stroke:#333,stroke-width:0px
linkStyle 0,2,3 stroke:red,stroke-width:4px
linkStyle 1,4,11 stroke:green,stroke-width:4px
「充足可能性問題」、通称「SAT問題」は、与えられた命題論理式を満たす変数割当てが存在するかどうかを判定する問題である。上の図に示すように、論理変数 $a$ を真とすると、$b$ の割当てが矛盾に陥す。SAT問題の効率的な解法は、理論計算機科学における最も重要な課題の一つである。
“N-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT”. Aolong Zha, Miyuki Koshimura, Hiroshi Fujita. Constraints, Vol. 24(2), 2019, pp. 133–161.
Coalition Structure Generation for Partition Function Games
kanban
CS1[Coalition Structure 1]
c1[Alice = Expert]@{ assigned: '3', priority: 'Very High' }
c2[Ben = Intermediate]@{ assigned: '1', priority: 'Low' }
c3[Carl = Beginner]@{ assigned: '-1', priority: 'High' }
CS2[Coalition Structure 2]
c4[Alice]@{ assigned: '2', priority: 'Very High' }
c5[Ben + Carl]@{ assigned: '2' }
CS3[Coalition Structure 3]
c6[Alice + Carl]@{ assigned: '3' }
c7[Ben]@{ assigned: '0', priority: 'Low' }
CS4[Coalition Structure 4]
c8[Alice + Ben]@{ assigned: '4' }
c9[Carl]@{ assigned: '-1', priority: 'High' }
CS5[Coalition Structure 5]
c10[Alice + Ben + Carl]@{ assigned: '2' }
「提携構造形成問題」は、協力ゲーム理論の問題の一つであり、エージェント集合を社会的利得が最大となるよう分割する問題である。上の図に示すように、上級者・中級者・初心者を含む3人の集合があって、彼らそれぞれの貢献度は、どのようにチームを組むかによって多少変動する。いかにして彼らを組合せ、最大の社会的価値を生み出すか、それがこの問題の本質である。
“Coalition structure generation for partition function games utilizing a concise graphical representation”. Aolong Zha, Kazuki Nomoto, Suguru Ueda, Miyuki Koshimura, Yuko Sakurai, Makoto Yokoo. In Proc. of 20th International Conference on Principles and Practice of Multi-Agent Systems, 2017, pp. 143–159.
Real-Time Taxi-Sharing Assignment
利用者は乗車希望時刻と場所、及び降車希望時刻と場所を配車システムに送信する。システムはその条件に基づき最適化を行い、タクシーをリアルタイムで割り当てる。従来のタクシーサービスと異なり、このシステムは異なる利用者のリクエストを考慮し、相乗りを可能にすることで運賃の削減を図る。
“An incremental SAT-based approach for solving the real-time taxi-sharing service problem”. Aolong Zha, Qiong Chang, Ituski Noda. Discrete Applied Mathematics, Vol. 335, 2023, pp. 131–145.
Pedestrian Evacuation Simulation and Optimization
歩行者道路網は大規模群集による混雑で事故が発生しやすい。本研究は、ハイブリッド群集モデルとモデル予測制御を組み合わせ、ネットワーク全体の動態を離散・連続の両面から同時に監視・制御する枠組みを考案し、群集分布の均衡維持と飽和リスク低減を求める。
“Hybrid modeling and predictive control of large-scale crowd movement in road network”. Rongxuan Gao, Aolong Zha, Shusuke Shigenaka, Masaki Onishi. In Proc. of 24th International Conference on Hybrid Systems: Computation and Control, 2021, pp. 26:1–26:7.
Optimization for Logistics and Transportation
近年、「物流2024年問題」対策や「カーボンニュートラル実現」に向け、道路輸送から鉄道貨物への転換が進められている。これら二つの輸送モードの組合せによる輸送コストとCO2排出量のパレート解を求め、そのトレードオフ関係を明らかにする。
“Optimization of transport costs and CO2 emissions through modal shift to railways using actual shipment amount” (in Japaneses). Hitoshi Hara, Aolong Zha, Naoto Imura. Journal of Japan Logistics Society, Vol. 32, 2024, pp. 52–62.
Stereo Matching on Embedded GPUs
計算資源が限られた組み込みGPU向けに最適化されたステレオマッチングフレームワークを考案し、効率的かつ高精度な深度推定を実現する。これにより、リアルタイムでの距離計測や障害物検知など、車載システム・ドローン向け応用場面でも実用的な性能を発揮できる。
“Efficient stereo matching on embedded GPUs with zero-means cross correlation”. Qiong Chang, Aolong Zha, Weimin Wang, Xin Liu, Masaki Onishi, Lei Lei, Tsutomu Maruyama. Journal of Systems Architecture, Vol. 123, 2022, p. 102366.