2:50 PM - 3:10 PM
[2N4-OS-17a-03] Reducing SAT Clauses for Transitive Relation
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.
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.
Authentication for paper PDF access
A password is required to view paper PDFs. If you are a registered participant, please log on the site from Participant Log In.
You could view the PDF with entering the PDF viewing password bellow.