Coupling Different Integer Encodings for SAT

Abstract

Boolean satisfiability (SAT) solvers have dramatically improved their performance in the last twenty years, enabling them to solve large and complex problems. More recently MaxSAT solvers have appeared that efficiently solve optimisation problems based on SAT. This means that SAT solvers have become a competitive technology for tackling discrete optimisation problems.A challenge in using SAT solvers for discrete optimisation is the many choices of encoding a problem into SAT. When encoding integer variables appearing in discrete optimisation problems, SAT must choose an encoding for each variable. Typical approaches fix a common encoding for all variables. However, different constraints are ..