Cardinality encodings for graph optimization problems

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

5 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationProceedings of the 26th International Joint Conference on Artificial Intelligence
EditorsCarles Sierra
Place of PublicationMarina del Rey CA USA
PublisherAssociation for the Advancement of Artificial Intelligence (AAAI)
Number of pages7
ISBN (Electronic)9780999241103
ISBN (Print)9780999241110
Publication statusPublished - 2017
Externally publishedYes
EventInternational Joint Conference on Artificial Intelligence 2017 - Melbourne, Australia
Duration: 19 Aug 201725 Aug 2017
Conference number: 26th (Proceedings)


ConferenceInternational Joint Conference on Artificial Intelligence 2017
Abbreviated titleIJCAI 2017
Internet address


  • Constraints and Satisfiability
  • Applications
  • Modeling/Formulation
  • Combinatorial & Heuristic Search
  • Combinatorial search/optimisation

Cite this