Compiling Pseudo-Boolean Constraints to SAT with Order Encoding

This paper presents a SAT-based pseudo-Boolean (PB for short) solver named PBSugar. PBSugar translates a PB instance to a SAT instance by using the order encoding, andsearches its solution by using an external SAT solver, such as Glucose. We first introduce an optimized version of the order encoding, and it is appliedto encode each PB constraint a₁ x₁ +...a_n x_n # k. The encoding isreformulated as a sparse Boolean matrix, named Counter Matrix, of size n × (k+1) constructed for each PB constraint. The same Counter Matrix can be usedfor any relations ≥, ≤, =, and ≠, and can be reused for other PBconstraints having common sub-terms. The experimental results for 669 instances of DEC-SMALLINT-LIN category(decision problems, small integers, linear constraints) demonstrates thesuperior performance of PBSugar compared to other state-of-the-art PB solvers interms of the number of solved instances within the given time limit.