Are there quantum algorithms for Prolog (SLD resolution - unification and depth-first-search) or for automated theorem proving in general (negation, resolution, and SAT)?

Usually automated theorem proving involves SAT problem for the negation of the initial statement and there is some better (but no exceptionally better) algorithms for that, e.g. Do any quantum algorithms improve on classical SAT?. But maybe there are some new ideas, some holistic approaches that involve the parallel search available on quantum computers? Google is of no help ("automated theorem proving quantum algorithm" no any result).

  • $\begingroup$ I'm interested in answer to this as well. $\endgroup$ Feb 5, 2021 at 19:17

1 Answer 1


One "dumb" way to speed-up a generic SAT problem would be to use Grover's Algorithm, but that would only give a quadratic speed-up over brute-force. It may the best one can do for some (or many) situations, but this is the most straight-forward thing that comes to mind.

Grover's algorithm is an algorithm that finds the input that makes an oracle function return true in $\sqrt{N}$ time where $N$ is the size of the search-space. It's often called a "database-search" problem but this is a big misnomer. It is NOT useful for searching databases because it's expensive to express databases as oracle functions. However, at least in theory, Boolean-SAT is naturally amenable to being expressed as a Grover algorithm oracle because you just need to make a circuit that computes the boolean expression and inverts the phase of the output qubit if the SAT problem is satisfied.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.