Importance of Variables Semantic in CNF Encoding of Cardinality Constraints
Anbu Anbulagan, Alban Grastien · ANU Open Research (Australian National University) · 2009
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 disagr