Optimization as theorem proving?

Question

There is sometimes need to find optimal rules, optimal policies, e.g. optimal Markov policy in symbolic form. E.g.see article about symbolic planning and hierarchical reinforcement learning. My question is: are there ideas about symbolic optimization or planning as theorem proving, .I.e. formulate the optimization task as some theorem in some logic/logic theory and then see the proof of this theorem as solution? Or maybe there are other ways how to logically formulate the search for some optimal rule set, some optimal policy rules, some optimal grammar as some logical task and solve it using available theorem provers or SAT solvers?