The "Solving SAT problem with Grover's algorithm" quantum kata is a series of exercises designed to get you comfortable with using Grover's algorithm to solve realistic problems using boolean satisfiability problems (SAT) as an example.
Each task is wrapped in one operation preceded by the description of the task.
Your goal is to fill in the blank (marked with the // ...
comments)
with some Q# code that solves the task. To verify your answer, run the cell using Ctrl+Enter (⌘+Enter on macOS).
Within each section, tasks are given in approximate order of increasing difficulty; harder ones are marked with asterisks.
The most interesting part of learning Grover's algorithm is solving realistic problems. This means using oracles which express an actual problem and not simply hard-code a known solution. In this section we'll learn how to express boolean satisfiability problems as quantum oracles.
Inputs:
2 qubits in an arbitrary state $|x\rangle$ (input/query register).
A qubit in an arbitrary state $|y\rangle$ (target qubit).
Goal:
Transform state $|x,y\rangle$ into state $|x, y \oplus f(x)\rangle$ ($\oplus$ is addition modulo 2), i.e., flip the target state if all qubits of the query register are in the $|1\rangle$ state, and leave it unchanged otherwise.
Leave the query register in the same state it started in.
Stretch Goal:
Can you implement the oracle so that it would work
for queryRegister
containing an arbitrary number of qubits?
%kata T11_Oracle_And
operation Oracle_And (queryRegister : Qubit[], target : Qubit) : Unit is Adj {
// ...
}
Can't come up with a solution? See the explained solution in the Solving SAT problem with Grover's algorithm Workbook.
Inputs:
2 qubits in an arbitrary state $|x\rangle$ (input/query register).
A qubit in an arbitrary state $|y\rangle$ (target qubit).
Goal:
Transform state $|x,y\rangle$ into state $|x, y \oplus f(x)\rangle$ ($\oplus$ is addition modulo 2), i.e., flip the target state if at least one qubit of the query register is in the $|1\rangle$ state, and leave it unchanged otherwise.
Leave the query register in the same state it started in.
Stretch Goal:
Can you implement the oracle so that it would work
for queryRegister
containing an arbitrary number of qubits?
%kata T12_Oracle_Or
operation Oracle_Or (queryRegister : Qubit[], target : Qubit) : Unit is Adj {
// ...
}
Can't come up with a solution? See the explained solution in the Solving SAT problem with Grover's algorithm Workbook.
Inputs:
2 qubits in an arbitrary state $|x\rangle$ (input/query register).
A qubit in an arbitrary state $|y\rangle$ (target qubit).
Goal:
Transform state $|x,y\rangle$ into state $|x, y \oplus f(x)\rangle$ ($\oplus$ is addition modulo 2), i.e., flip the target state if the qubits of the query register are in different states, and leave it unchanged otherwise.
Leave the query register in the same state it started in.
Stretch Goal:
Can you implement the oracle so that it would work
for queryRegister
containing an arbitrary number of qubits?
%kata T13_Oracle_Xor
operation Oracle_Xor (queryRegister : Qubit[], target : Qubit) : Unit is Adj {
// ...
}
Can't come up with a solution? See the explained solution in the Solving SAT problem with Grover's algorithm Workbook.
Inputs:
N qubits in an arbitrary state $|x\rangle$ (input/query register).
A qubit in an arbitrary state $|y\rangle$ (target qubit).
Goal:
Transform state $|x,y\rangle$ into state $|x, y \oplus f(x)\rangle$ ($\oplus$ is addition modulo 2).
Leave the query register in the same state it started in.
This oracle marks two states similar to the state explored in task 1.2 of the GroversAlgorithm kata:
$|10101...\rangle$ and $|01010...\rangle$.
It is possible (and quite straightforward) to implement this oracle based on this observation;
however, for the purposes of learning to write oracles to solve SAT problems we recommend using the representation above.
%kata T14_Oracle_AlternatingBits
operation Oracle_AlternatingBits (queryRegister : Qubit[], target : Qubit) : Unit is Adj {
// ...
}
Can't come up with a solution? See the explained solution in the [Solving SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-1.4.-Alternating-bits-oracle:-$f(x)-=-(x_0-\oplus-x_1)-\wedge-(x_1-\oplus-x_2)-\wedge-\dots-\wedge-(x_{N-2}-\oplus-x_{N-1})$).
For SAT problems, $f(x)$ is represented as a conjunction (an AND operation) of several clauses on $N$ variables,
and each clause is a disjunction (an OR operation) of one or several variables or negated variables:
$$clause(x) = \bigvee_k y_{k},\text{ where }y_{k} =\text{ either }x_j\text{ or }\neg x_j\text{ for some }j \in \{0, \dots, N-1\}$$For example, one of the possible clauses on two variables is:
$$clause(x) = x_0 \vee \neg x_1$$
Inputs:
N qubits in an arbitrary state $|x\rangle$ (input/query register).
A qubit in an arbitrary state $|y\rangle$ (target qubit).
A 1-dimensional array of tuples clause
which describes one clause of a SAT problem instance $clause(x)$.
clause
is an array of one or more tuples, each of them describing one component of the clause.
Each tuple is an (Int, Bool)
pair:
true
if the variable is included as itself ($x_j$) and false
if it is included as a negation ($\neg x_j$).Example:
[(0, true), (1, false)]
.Goal:
Transform state $|x,y\rangle$ into state $|x, y \oplus f(x)\rangle$ ($\oplus$ is addition modulo 2).
Leave the query register in the same state it started in.
%kata T15_Oracle_SATClause
operation Oracle_SATClause (queryRegister : Qubit[], target : Qubit, clause : (Int, Bool)[]) : Unit is Adj {
// ...
}
Can't come up with a solution? See the explained solution in the Solving SAT problem with Grover's algorithm Workbook.
For k-SAT problems, $f(x)$ is represented as a conjunction (an AND operation) of $M$ clauses on $N$ variables,
and each clause is a disjunction (an OR operation) of one or several variables or negated variables:
$$f(x) = \bigwedge_i \big(\bigvee_k y_{ik} \big),\text{ where }y_{ik} =\text{ either }x_j\text{ or }\neg x_j\text{ for some }j \in \{0, \dots, N-1\}$$
Inputs:
N qubits in an arbitrary state $|x\rangle$ (input/query register).
A qubit in an arbitrary state $|y\rangle$ (target qubit).
A 2-dimensional array of tuples problem
which describes the k-SAT problem instance $f(x)$.
$i$-th element of problem
describes the $i$-th clause of $f(x)$;
it is an array of one or more tuples, each of them describing one component of the clause.
Each tuple is an (Int, Bool)
pair:
true
if the variable is included as itself ($x_j$) and false
if it is included as a negation ($\neg x_j$).Example:
A more general case of the OR oracle for 3 variables $f(x) = (x_0 \vee x_1 \vee x_2)$ can be represented as [[(0, true), (1, true), (2, true)]]
.
Goal:
Transform state $|x,y\rangle$ into state $|x, y \oplus f(x)\rangle$ ($\oplus$ is addition modulo 2).
Leave the query register in the same state it started in.
%kata T16_Oracle_SAT
operation Oracle_SAT (queryRegister : Qubit[], target : Qubit, problem : (Int, Bool)[][]) : Unit is Adj {
// ...
}
Can't come up with a solution? See the explained solution in the Solving SAT problem with Grover's algorithm Workbook.
Exactly-1 3-SAT problem (also known as "one-in-three 3-SAT") is a variant of a general 3-SAT problem. It has a structure similar to a 3-SAT problem, but each clause must have exactly one true literal, while in a normal 3-SAT problem each clause must have at least one true literal.
Inputs:
3 qubits in an arbitrary state $|x\rangle$ (input/query register).
A qubit in an arbitrary state $|y\rangle$ (target qubit).
Goal:
Transform state $|x,y\rangle$ into state $|x, y \oplus f(x)\rangle$ ($\oplus$ is addition modulo 2), where $f(x) = 1$ if exactly one bit of $x$ is in the $|1\rangle$ state, and $0$ otherwise.
Leave the query register in the same state it started in.
Stretch Goal:
Can you implement the oracle so that it would work
for queryRegister
containing an arbitrary number of qubits?
%kata T21_Oracle_Exactly1One
operation Oracle_Exactly1One (queryRegister : Qubit[], target : Qubit) : Unit is Adj {
// ...
}
Can't come up with a solution? See the explained solution in the Solve SAT problem with Grover's algorithm Workbook.
Inputs:
N qubits in an arbitrary state $|x\rangle$ (input/query register).
A qubit in an arbitrary state $|y\rangle$ (target qubit).
A 2-dimensional array of tuples problem
which describes the 3-SAT problem instance $f(x)$.
problem
describes the problem instance in the same format as in task 1.6;
each clause of the formula is guaranteed to have exactly 3 terms.
Goal:
Transform state $|x,y\rangle$ into state $|x, y \oplus f(x)\rangle$ ($\oplus$ is addition modulo 2).
Leave the query register in the same state it started in.
Example:
An instance of the problem $f(x) = (x_0 \vee x_1 \vee x_2)$ can be represented as [[(0, true), (1, true), (2, true)]]
,
and its solutions will be (true, false, false)
, (false, true, false)
and (false, false, true)
,
but none of the variable assignments in which more than one variable is true, which are solutions for the general SAT problem.
%kata T22_Oracle_Exactly1SAT
operation Oracle_Exactly1_3SAT (queryRegister : Qubit[], target : Qubit, problem : (Int, Bool)[][]) : Unit is Adj {
// ...
}
Can't come up with a solution? See the explained solution in the Solve SAT problem with Grover's algorithm Workbook.
Goal:
Implement Grover's algorithm and use it to find solutions to SAT instances from parts I and II.
If you want to learn the Grover's algorithm itself, try doing GroversAlgorithm kata first.
This is an open-ended task, and is not covered by a unit test. To run the code, execute the cell with the definition of the
Run_GroversSearch_Algorithm
operation first; if it compiled successfully without any errors, you can run the operation by executing the next cell (%simulate Run_GroversSearch_Algorithm
).
Note that this task relies on your implementations of the previous tasks. If you are getting the "No variable with that name exists." error, you might have to execute previous code cells before retrying this task.
For example,
operation Run_GroversSearch_Algorithm () : Unit {
// ...
}
%simulate Run_GroversSearch_Algorithm
Can't come up with a solution? See the explained solution in the Solve SAT problem with Grover's algorithm Workbook.
Inputs:
The number of qubits N.
A marking oracle which implements a boolean expression, similar to the oracles from part I.
Output:
An array of N boolean values which satisfy the expression implemented by the oracle (i.e., any basis state marked by the oracle).
Note that the similar task in the GroversAlgorithm kata required you to implement Grover's algorithm
in a way that would be robust to accidental failures, but you knew the optimal number of iterations (the number that minimized the probability of such failure).
In this task you also need to make your implementation robust to not knowing the optimal number of iterations. You can see an example of doing that in Exploring Grover's Algorithm tutorial.
%kata T32_UniversalGroversAlgorithm
operation UniversalGroversAlgorithm (N : Int, oracle : ((Qubit[], Qubit) => Unit is Adj)) : Bool[] {
// ...
return [false, size = N];
}
Can't come up with a solution? See the explained solution in the Solve SAT problem with Grover's algorithm Workbook.