Importance of Variables Semantic in CNF Encoding of Cardinality Constraints

In the satisfiability domain, it is well-known that a SAT algorithm may solve a problem instance easily and another instance hardly, whilst these two instances are equivalent CNF encodings of the original problem. Moreover, different algorithms may disagree on which encoding makes the problem easier to solve. In this paper, we focus on the CNF encoding of cardinality constraints, which states that exactly k propositional variables in a given set are assigned to true. We demonstrate the importance of the semantics of the SAT variables in the encoding of this constraint. We implement several variants of the CNF encoding in which the close semantic variables are grouped. We then examine these new encodings on problems generated from diagnosis of discrete-event system. Our results demonstrate that both stochastic and systematic SAT algorithms can now solve most of the problem instances, which were unreachable before. These results also indicate that, on average cases, there is an encoding that suits well both SLS and DPLL algorithms.