A New Method to Encode the At-Most-One Constraint into SAT

摘要: One of the most widely used constraints during process translating a practical problem into propositional satisfiability (SAT) instance is at-most-one (AMO) constraint. This paper proposes new encoding for AMO constraint, so-called bimander which can be easily extended to encode cardinality constraints, are often in constraint programming. Experimental results reveal that very competitive compared with all other state-of-the-art encodings. Furthermore, we will prove allows unit propagation achieve arc consistency - an important technique We also show special case outperforms binary encoding, our experiments.