#CCF/A/AAAI

[!tldr]文章链接 The Impact of Literal Sorting on Cardinality Constraint Encodings [!summary]The effectiveness of satisfiability solvers strongly depends on the quality of the encoding of a given problem into conjunctive normal form.