Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4949683 | Discrete Applied Mathematics | 2017 | 7 Pages |
Abstract
Using a SAT-solver on top of a partial previously-known solution we improve the upper bound of the packing chromatic number of the infinite square lattice from 17 to 15. We discuss the merits of SAT-solving for this kind of problem as well as compare the performance of different encodings. Further, we improve the lower bound from 12 to 13 again using a SAT-solver, demonstrating the versatility of this technology for our approach.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Barnaby Martin, Franco Raimondi, Taolue Chen, Jos Martin,