Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem

Decision and optimization problems can be tackled with dif-ferent techniques, such as Mixed Integer Programming, Constraint Pro-gramming or SAT solving. An important ingredient in the success of eachof these approaches is the exploitation of common constraint structureswith specialized (re-)formulations, encodings or other techniques. In thispaper we present a new linear SAT encoding using binary decision dia-grams over multiple variable orders as intermediate representation of aspecial form of constraints denoted as staircase at-most-one-constraints.The use of these constraints is motivated by recent work on the antiband-width problem, where an iterative solution procedure using feasibility-mixed integer programs based on such constraints was most effective. Ina computational study we compare the effectiveness of our new encodingagainst traditional SAT-encodings for staircase at-most-one-constraints.Additionally we compare against previous exact solution methods for theantibandwidth problem, such as a constraint programming approach andthe one based on feasibility-mixed integer programs.