TY - GEN

T1 - Importance of variables semantic in CNF encoding of cardinality constraints

AU - Anbulagan,

AU - Grastien, Alban

PY - 2009

Y1 - 2009

N2 - 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 prepositional 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 (Grastien et al. 2007). These results also indicate that, on average cases, there is an encoding that suits well both SLS and DPLL algorithms.

AB - 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 prepositional 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 (Grastien et al. 2007). These results also indicate that, on average cases, there is an encoding that suits well both SLS and DPLL algorithms.

UR - http://www.scopus.com/inward/record.url?scp=84890261698&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9781577354338

T3 - SARA 2009 - Proceedings, 8th Symposium on Abstraction, Reformulation and Approximation

SP - 10

EP - 17

BT - SARA 2009 - Proceedings, 8th Symposium on Abstraction, Reformulation and Approximation

T2 - 8th Symposium on Abstraction, Reformulation and Approximation, SARA 2009

Y2 - 7 July 2009 through 10 July 2009

ER -