It seems that today’s network dwellers are capable of discovering a whole new world with a single keyword, and here are a few keywords and concepts for you if you want to find out more by yourself.
SAT and SMT are two problem families that can model most problems in real world, who lay in the heart of our discussion.
make the highlight stylish
The complexity class NP-Complete shows how and why a problem is hard. It has many peers, like P, PSPACE, BQP, and so on.
Gödel discovered the deep-rooted flaw of our logical system, defining a boundary where our computation can reach, while the complexity defines how hard to reach it.
DPLL and CDCL are two stages of the same mainstream SAT solver algorithm, and DPLL(T) is a SMT solver algorithm as a extension of CDCL.
Z3, CVC5 and their peers are the cutting edge SAT/SMT solvers.