Logic Programming with Graph Automorphism: Integratingnautywith Prolog (Tool Description)

DOI10.1017/S1471068416000223MaRDI QIDQ4593050zbMATH OpenOpenAlexFDO

Authors M. Frank, Michael Codish

Publication date 9 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1607.04829

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to combinatorics (05-04) Logic programming (68N17) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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 auty'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.

Recommendations

• scientific article; zbMATH DE number 638303
• scientific article; zbMATH DE number 177436
• scientific article; zbMATH DE number 1638651
• Automated theorem proving and logic programming: a natural symbiosis
• scientific article; zbMATH DE number 3936497
• scientific article; zbMATH DE number 7453192
• Automated verification of Prolog programs
• Automatic inductive theorem proving using Prolog

Cites work

• Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems
• Compiling finite domain constraints to SAT with BEE
• Engineering an efficient canonical labeling tool for large and sparse graphs
• scientific article; zbMATH DE number 3823850 (Why is no real title available?)
• scientific article; zbMATH DE number 1974110 (Why is no real title available?)
• McKay's canonical graph labeling algorithm
• Practical graph isomorphism. II.
• Random models and analyses for chemical graphs
• Sorting nine inputs requires twenty-five comparisons
• SWI-Prolog

Cited in

(2)

• pl-nauty
• Resolution with symmetry rule applied to linear equations

Describes a project that uses

Uses Software

• nauty
• BEE
• SWI-Prolog
• bliss
• Traces

This page was built for publication: Logic Programming with Graph Automorphism: Integratingnautywith Prolog (Tool Description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4593050)