Satisfiability Problem

Quantum Algorithms

Boolean Satisfiability Problems

Satisfiability problems are an extension of Grover's algorithm. The Boolean satisfiability problem focuses on determining if there exists an interpretation that satisfies a given Boolean formula.  Said differently, the Boolean satisfiability problem determines whether the variables of a given Boolean formula can be consistently replaced by the values 'True' or 'False' so that the Boolean formula evaluates to 'True'.  Thus, the formula is labeled satisfiable.  Otherwise, if no such assignment exists, the function expressed by the Boolean formula is 'False' for all possible variable assignments and is unsatisfiable. 

For example, the formula "a AND NOT b" is satisfiable because one can find the values a = True and b = False, which make (a AND NOT b) = True.  In contrast, "a AND NOT a" is unsatisfiable.  

A naïve way to find such an assignment is by trying every possible combinations of input values of f. Below is the table obtained from trying all possible combinations of v1,v2,v3v1,v2,v3. 

Note: SAT problems can be always written in conjunctive normal form (CNF), that is, a conjunction of one or more clauses, where a clause is a disjunction of three literals.  Said differently, it is an AND of k ORs.

Changes / Migration Guide:

• Instead of using the LogicalExpressionOracle now use the PhaseOracle circuit from the circuit library.
  • Import ...
    • from qiskit.circuit.library import PhaseOracle
    • from qiskit.algorithms import Grover, AmplificationProblem