Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Documents

  • Fulltext

    Submitted manuscript, 339 KB, PDF document

  • Stephan Gocht
  • Ross McBride
  • Ciaran McCreesh
  • Nordström, Jakob
  • Patrick Prosser
  • James Trimble

An algorithm is said to be certifying if it outputs, together with a solution to the problem it solves, a proof that this solution is correct. We explain how state of the art maximum clique, maximum weighted clique, maximal clique enumeration and maximum common (connected) induced subgraph algorithms can be turned into certifying solvers by using pseudo-Boolean models and cutting planes proofs, and demonstrate that this approach can also handle reductions between problems. The generality of our results suggests that this method is ready for widespread adoption in solvers for combinatorial graph problems.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming : 26th International Conference, CP 2020, Proceedings
EditorsHelmut Simonis
PublisherSpringer
Publication date2020
Pages338-357
ISBN (Print)9783030584740
DOIs
Publication statusPublished - 2020
Event26th International Conference on Principles and Practice of Constraint Programming, CP 2020 - Louvain-la-Neuve, Belgium
Duration: 7 Sep 202011 Sep 2020

Conference

Conference26th International Conference on Principles and Practice of Constraint Programming, CP 2020
LandBelgium
ByLouvain-la-Neuve
Periode07/09/202011/09/2020
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12333 LNCS
ISSN0302-9743

ID: 251866968