[2N4-OS-17a] OS-17 (1)

[2N4-OS-17a-03] Reducing SAT Clauses for Transitive Relation

〇Miyuki Koshimura¹, Xiaojuan Liao², Emi Watanabe¹, Yuko Sakurai³, Makoto Yokoo¹ (1. Kyushu University, 2. Chengdu University of Technology, China, 3. National Institute of Advanced Industrial Science and Technology)

Keywords:Coalition Structure Generation, MaxSAT

Transitivity is a property satisfied by many practical relations. When we solve problems containing some transitive relations with SAT, we need to encode them into SAT clauses. Though a well-known encoding is quite simple, the number of generated SAT clauses becomes huge as the size of problem grows.

This paper considers transitivity of reachable relation in undirected graph and proposes an idea for reducing SAT clauses for transitivity. We experimentally evaluate the amount of reduction and the performance of our proposed idea using several instances of CSG (Coalition Structure Generation) with MC-nets.