Logic Programming with Graph Automorphism: Integrating naut with Prolog (Tool Description)

TL;DR

This paper introduces plnauty, a Prolog interface to the nauty graph-automorphism tool, enabling symmetry reduction in logic programming and integration with existing tool-chains like SAT solvers.

Contribution

It presents a novel Prolog library that integrates nauty's graph automorphism capabilities, enhancing symmetry handling in logic programming environments.

Findings

Enables symmetry reduction in Prolog graph reasoning

Integrates nauty with Prolog tool-chains

Demonstrates applications in generating Ramsey graphs

Abstract

This paper presents the plnauty~library, a Prolog interface to the nauty graph-automorphism tool. Adding the capabilities of nauty to Prolog combines the strength of the "generate and prune" approach that is commonly used in logic programming and constraint solving, with the ability to reduce symmetries while reasoning over graph objects. Moreover, it enables the integration of nauty in existing tool-chains, such as SAT-solvers or finite domain constraints compilers which exist for Prolog. The implementation consists of two components: plnauty, an interface connecting \nauty's C library with Prolog, and plgtools, a Prolog framework integrating the software component of nauty, called gtools, with Prolog. The complete tool is available as a SWI-Prolog module. We provide a series of usage examples including two that apply to generate Ramsey graphs. This paper is under consideration for publication in TPLP.