Exploiting Global Properties in Path-Consistency Applied on SAT

The task of enforcing certain level of consistency in Boolean satisfiability problem (SAT problem) is addressed in this paper. The concept of path-consistency known from the constraint programming paradigm is revisited in this context. Augmentations how to make path-consistency more suitable for SAT are specifically studied. A stronger variant of path-consistency is described and its theoretical properties are investigated. It combines the standard path consistency on the literal encoding of the given SAT instance with global properties calculated from constraints imposed by the instance – namely with the maximum number of visits of a certain set by the path. Unfortunately, the problem of enforcing this variant of path-consistency turned out to be NP hard. Hence, various types of relaxations of this stronger version of path-consistency were proposed. The relaxed version of the proposed consistency represents a trade-off between the inference strength and the complexity of its propagation algorithm. A presented theoretical analysis shows that computational costs of the proposed consistency are kept reasonably low. Performed experiments show that the new consistency outperforms the standard path-consistency in terms of the inference strength as well.