The programming language Mercury which is a functional, predicate based, moded language uses something like a precursor to a sat solver to "run" the program. As

The programming language Mercury which is a functional, predicate based, moded language uses something like a precursor to a sat solver to "run" the program. As in you can ask for the input of a function to make your program true. I imagine all sorts of things can be done like this, and the sat solver is useful for verifying correctness.