Armin Biere,
"Two Pigeons per Hole Problem"
, in A. Balint, A. Belov, M. Heule, M. Järvisalo: In Proceedings of SAT Competition 2013, Vol. B-2013-1, Department of Computer Science, University of Helsinki, Seite(n) 103, 2013
Original Titel:
Two Pigeons per Hole Problem
Sprache des Titels:
Englisch
Original Buchtitel:
In Proceedings of SAT Competition 2013
Original Kurzfassung:
In the newest version of our SAT solver Lingeling we
included a simple algorithm for solving large trivially encoded
pigeon hole problems. The algorithm is based on cardinality
reasoning. More information about the algorithm can be found
in our solver description.
One phase of the algorithm consists of extracting at-mostone
constraints, which we extended to extract at-most-two constraints
too. This extension allowed us to solve the following
simple extension of the pigeon hole problem.