Linear Ordering in the SAT Encoding of the All-Different Constraint over Bit-Vectors

Abstract

A novel eager encoding of the ALLDIFFERENT constraint over bit-vectors is presented in this short paper. It is based on 1-to-1 mapping of the input bit-vectors to a linearly ordered set of auxiliary bit-vectors.

Experiments with four SAT solvers showed that the new encoding could be solved order of magnitudes faster than the standard encoding in a hard unsatisfiable case.

Keywords

• Linear Ordering
• SAT Encoding
• All-Different Constraint
• Bit-Vectors