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

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

Research output: Chapter in Book/Report/Conference proceedingPaper in conference proceedingpeer-review

Abstract

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
Pages338-357
Number of pages20
ISBN (Print)9783030584740
DOIs
Publication statusPublished - 2020
Event26th International Conference on Principles and Practice of Constraint Programming, CP 2020 - Louvain-la-Neuve, Belgium
Duration: 2020 Sept 72020 Sept 11

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12333
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Conference on Principles and Practice of Constraint Programming, CP 2020
Country/TerritoryBelgium
CityLouvain-la-Neuve
Period2020/09/072020/09/11

Subject classification (UKÄ)

  • Computer Science

Fingerprint

Dive into the research topics of 'Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems'. Together they form a unique fingerprint.

Cite this