Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints

Felix Ulrich-Oltean, Peter Nightingale, James Alfred Walker

Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simple…