To Be or Not To Be: Adding Integrity Constraints to stableKanren to Make a Decision

TL;DR

This paper introduces a novel method to incorporate integrity constraints into stableKanren, enhancing its ability to solve combinatorial search problems by leveraging contradiction reasoning and control over goal outcomes.

Contribution

The paper presents a new approach to integrate integrity constraints into stableKanren, enabling more effective combinatorial problem solving with contradiction reasoning.

Findings

Unified framework for integrity constraints in stableKanren

Improved control over predicate outcomes during resolution

Enhanced capability to solve combinatorial search problems

Abstract

We integrate integrity constraints to stableKanren to enable a new problem-solving paradigm in combinatorial search problems. stableKanren extends miniKanren to reasoning about contradictions under stable model semantics. However, writing programs to solve combinatorial search problems in stableKanren did not fully utilize the contradiction reasoning. This is mainly due to the lack of control over the predicate (goal function) outcome during resolution. Integrity constraints defined by answer set programming (ASP) provide the ability to constrain the predicate outcome. However, integrity constraints are headless normal clauses, and stableKanren cannot create a goal function without a valid head. There are two approaches to handling integrity constraints, but they do not fit stableKanren. Therefore, we design a new approach to integrate integrity constraints into stableKanren. We show a uniform framework to solve combinatorial search problems using integrity constraints in extended stableKanren.