REVIEW 1 cited by
Yet Another Comparison of SAT Encodings for the At-Most-K Constraint
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
abstract
The at-most-k constraint is ubiquitous in combinatorial problems, and numerous SAT encodings are available for the constraint. Prior experiments have shown the competitiveness of the sequential-counter encoding for k $>$ 1, and have excluded the parallel-counter encoding, which is more compact that the binary-adder encoding, from consideration due to its incapability of enforcing arc consistency through unit propagation. This paper presents an experiment that shows astounding performance of the binary-adder encoding for the at-most-k constraint.
Forward citations
Cited by 1 Pith paper
-
Asymptotically Smaller Encodings for Graph Problems and Scheduling
Independent set, vertex cover, k-coloring and clique admit CNF encodings with O(n^2/log n) clauses, and the disjoint-intervals encoding needs only O(n^2 log n) clauses.
Discussion (0). Continue with ORCID to comment.