Wayne Joubert wrote a great post about SAT solvers, software that finds how, if possible, to set Boolean variables to satisfy a collection of logical expressions. This problem is NP-complete, and yet in practice it is possible to solve enormous SAT problems.
Wayne discusses applications, recommends some references, and gives some Z3 code to illustrate using SAT solver.
Health care providers in the US — physicians, pharmacists, midwives, etc. — are required to apply for a 10-digit unique identifier called an NPI (National Provider Identifier).
The last digit of a NPI number is a checksum. NPIs use the same checksum algorithm as credit cards, the Luhn algorithm, with a small difference: a magic number is prepended before computing the checksum.
Love this stuff! Thanks for this post....
Amazon Science has a strong team here. This post (below) offers context, pretty pictures, competition members and results, and some future prognostications.
https://www.amazon.science/blog/automated-reasonings-scientific-frontiers
Why SAT/SMT tools & techniques are not every bit as 'popular' as Large Hallucination and Crowdspeak algorithms is mildly mystifying to me...