This work generalizes a state-of-the-art SAT solver into a “cardinality solve” we call MiniCARD. Using a watched-literal scheme for native cardinality constraints, MiniCARD greatly outperforms CNF encodings of cardinality constraints on all purecardinality instances tested. The modifications to the solver are minimal, and it retains its performance on pure CNF instances. With easy implementation and no cost, any CDCL SAT solver can be extended to be a cardinality solver “for free.”

MiniCARD Solver

CNFP Generators

Published Poster