{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T05:20:11Z","timestamp":1783056011850,"version":"3.54.6"},"reference-count":26,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T00:00:00Z","timestamp":1778716800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Advances in Applied Mathematics"],"published-print":{"date-parts":[[2026,9]]},"DOI":"10.1016\/j.aam.2026.103112","type":"journal-article","created":{"date-parts":[[2026,5,15]],"date-time":"2026-05-15T16:29:37Z","timestamp":1778862577000},"page":"103112","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["North\u2013East lattice paths avoiding k collinear points via satisfiability"],"prefix":"10.1016","volume":"179","author":[{"given":"Aaron","family":"Barnoff","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Curtis","family":"Bright","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.aam.2026.103112_br0010","series-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","first-page":"108","article-title":"Efficient CNF encoding of Boolean cardinality constraints","volume":"vol. 2833","author":"Bailleux","year":"2003"},{"key":"10.1016\/j.aam.2026.103112_br0020","series-title":"Computer Aided Verification \u2013 CAV 2024","first-page":"133","article-title":"CaDiCaL 2.0","volume":"vol. 14681","author":"Biere","year":"2024"},{"key":"10.1016\/j.aam.2026.103112_br0030","first-page":"3669","article-title":"A SAT-based resolution of Lam's problem","volume":"35","author":"Bright","year":"2021","journal-title":"Proc. AAAI Conf. Artif. Intell."},{"key":"10.1016\/j.aam.2026.103112_br0040","series-title":"Maple in Mathematics Education and Research","first-page":"205","article-title":"Effective problem solving using SAT solvers","volume":"vol. 1125","author":"Bright","year":"2020"},{"key":"10.1016\/j.aam.2026.103112_br0050","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1145\/3500921","article-title":"When satisfiability solving meets symbolic computation","volume":"65","author":"Bright","year":"2022","journal-title":"Commun. ACM"},{"key":"10.1016\/j.aam.2026.103112_br0060","first-page":"798","article-title":"Advanced problem 5811","volume":"78","author":"Brown","year":"1971","journal-title":"Am. Math. Mon."},{"key":"10.1016\/j.aam.2026.103112_br0070","series-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","first-page":"71","article-title":"DRAT proofs, propagation redundancy, and extended resolution","volume":"vol. 11628","author":"Buss","year":"2019"},{"key":"10.1016\/j.aam.2026.103112_br0080","series-title":"Proceedings of the Third Annual ACM Symposium on Theory of Computing - STOC '71","first-page":"151","article-title":"The complexity of theorem-proving procedures","author":"Cook","year":"1971"},{"key":"10.1016\/j.aam.2026.103112_br0090","first-page":"294","article-title":"Problem 408","volume":"10","author":"Ecker","year":"1979","journal-title":"Crux Math."},{"key":"10.1016\/j.aam.2026.103112_br0100","doi-asserted-by":"crossref","first-page":"349","DOI":"10.2140\/pjm.1979.83.349","article-title":"Long walks in the plane with few collinear points","volume":"83","author":"Gerver","year":"1979","journal-title":"Pac. J. Math."},{"key":"10.1016\/j.aam.2026.103112_br0110","doi-asserted-by":"crossref","first-page":"357","DOI":"10.2140\/pjm.1979.83.357","article-title":"On certain sequences of lattice points","volume":"83","author":"Gerver","year":"1979","journal-title":"Pac. J. Math."},{"key":"10.1016\/j.aam.2026.103112_br0120","series-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2004","first-page":"345","article-title":"March_eq: implementing additional reasoning into an efficient look-ahead SAT solver","volume":"vol. 3542","author":"Heule","year":"2005"},{"key":"10.1016\/j.aam.2026.103112_br0130","series-title":"Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence Organization","first-page":"4864","article-title":"Solving very hard problems: cube-and-conquer, a hybrid SAT solving method","author":"Heule","year":"2017"},{"key":"10.1016\/j.aam.2026.103112_br0140","series-title":"Hardware and Software: Verification and Testing","first-page":"50","article-title":"Cube and conquer: guiding CDCL SAT solvers by lookaheads","volume":"vol. 7261","author":"Heule","year":"2012"},{"key":"10.1016\/j.aam.2026.103112_br0150","series-title":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"61","article-title":"Happy ending: an empty hexagon in every set of 30 points","volume":"vol. 14570","author":"Heule","year":"2024"},{"key":"10.1016\/j.aam.2026.103112_br0160","series-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","first-page":"428","article-title":"PySAT: a python toolkit for prototyping with SAT oracles","volume":"vol. 10929","author":"Ignatiev","year":"2018"},{"key":"10.1016\/j.aam.2026.103112_br0170","doi-asserted-by":"crossref","DOI":"10.1016\/j.disc.2023.113718","article-title":"Improved bound for the Gerver-Ramsey collinearity problem","volume":"347","author":"Lidbetter","year":"2024","journal-title":"Discrete Math."},{"key":"10.1016\/j.aam.2026.103112_br0180","first-page":"1143","article-title":"Collinear points on a monotonic polygon","volume":"79","author":"Montgomery","year":"1972","journal-title":"Am. Math. Mon."},{"key":"10.1016\/j.aam.2026.103112_br0190","series-title":"Cardinality Constraints in Boolean Satisfiability Solving","author":"Reeves","year":"2025"},{"key":"10.1016\/j.aam.2026.103112_br0200","series-title":"Computer Aided Verification: 36th International Conference, Proceedings, Part I","first-page":"110","article-title":"From clauses to klauses","volume":"vol. 14681","author":"Reeves","year":"2024"},{"key":"10.1016\/j.aam.2026.103112_br0210","author":"Shallit"},{"key":"10.1016\/j.aam.2026.103112_br0220","series-title":"Principles and Practice of Constraint Programming - CP 2005","first-page":"827","article-title":"Towards an optimal CNF encoding of Boolean cardinality constraints","volume":"vol. 3709","author":"Sinz","year":"2005"},{"key":"10.1016\/j.aam.2026.103112_br0230","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"389","article-title":"The packing chromatic number of the infinite square grid is 15","volume":"vol. 13993","author":"Subercaseaux","year":"2023"},{"key":"10.1016\/j.aam.2026.103112_br0240","series-title":"Intelligent Computer Mathematics","first-page":"29","article-title":"Automated symmetric constructions in discrete geometry","volume":"vol. 16136","author":"Subercaseaux","year":"2025"},{"key":"10.1016\/j.aam.2026.103112_br0250","series-title":"Intelligent Computer Mathematics","first-page":"21","article-title":"Automated mathematical discovery and verification: minimizing pentagons in the plane","volume":"vol. 14960","author":"Subercaseaux","year":"2024"},{"key":"10.1016\/j.aam.2026.103112_br0260","series-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","first-page":"422","article-title":"DRAT-trim: efficient checking and trimming using expressive clausal proofs","volume":"vol. 8561","author":"Wetzler","year":"2014"}],"container-title":["Advances in Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0196885826000849?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0196885826000849?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T04:54:37Z","timestamp":1783054477000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0196885826000849"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9]]},"references-count":26,"alternative-id":["S0196885826000849"],"URL":"https:\/\/doi.org\/10.1016\/j.aam.2026.103112","relation":{},"ISSN":["0196-8858"],"issn-type":[{"value":"0196-8858","type":"print"}],"subject":[],"published":{"date-parts":[[2026,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"North\u2013East lattice paths avoiding k collinear points via satisfiability","name":"articletitle","label":"Article Title"},{"value":"Advances in Applied Mathematics","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.aam.2026.103112","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"103112"}}