Cardinality Encodings for Graph Optimization Problems

Cardinality Encodings for Graph Optimization Problems

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 652-658. https://doi.org/10.24963/ijcai.2017/91

Different optimization problems defined on graphs find application in complex network analysis. Existing propositional encodings render impractical the use of propositional satisfiability (SAT) and maximum satisfiability (MaxSAT) solvers for solving a variety of these problems on large graphs. This paper has two main contributions. First, the paper identifies sources of inefficiency in existing encodings for different optimization problems in graphs. Second, for the concrete case of the maximum clique problem, the paper develops a novel encoding which is shown to be far more compact than existing encodings for large sparse graphs. More importantly, the experimental results show that the proposed encoding enables existing SAT solvers to compute a maximum clique for large sparse networks, often more efficiently than the state of the art.
Keywords:
Constraints and Satisfiability: Applications
Constraints and Satisfiability: Modeling/Formulation
Constraints and Satisfiability: Constraints and Satisfiability
Combinatorial & Heuristic Search: Combinatorial search/optimisation