I hadn't really thought about it in those terms, but the implementation of bounded model checking is very similar to the proof of the Cook-Levin theorem. You encode the nondeterministic transition relation of your model of computation as a formula in propositional logic, unroll it to some fixed depth (given by the polynomial-time bound in the case of Cook-Levin), and check for satisfiability of the unrolled transition relation formulas and an auxiliary formula.
=> More informations about this toot | View the thread | More toots from pervognsen@mastodon.social
text/geminiThis content has been proxied by September (3851b).