Towards "Propagation = Logic + Control"

TL;DR

This paper introduces a high-level framework for controlling constraint propagation algorithms, distinguishing between control information and logical semantics, and demonstrates its practicality through implementation and benchmarking.

Contribution

It presents a novel controlled propagation framework that captures principles of manual algorithms and improves efficiency in logical inference tasks.

Findings

Framework effectively differentiates control and semantics

Implementation shows practical efficiency

Captures principles of existing propagation algorithms

Abstract

Constraint propagation algorithms implement logical inference. For efficiency, it is essential to control whether and in what order basic inference steps are taken. We provide a high-level framework that clearly differentiates between information needed for controlling propagation versus that needed for the logical semantics of complex constraints composed from primitive ones. We argue for the appropriateness of our controlled propagation framework by showing that it captures the underlying principles of manually designed propagation algorithms, such as literal watching for unit clause propagation and the lexicographic ordering constraint. We provide an implementation and benchmark results that demonstrate the practicality and efficiency of our framework.