Квантовый оракул формулы SAT

Входы — N кубитов в произвольном состоянии $|x\rangle$ и целевой кубит в произвольном состоянии $|y\rangle$.

Литерал — переменная x_j или её отрицание. Пара (j,true) означает x_j, (j,false) — отрицание x_j. Дизъюнкт — логическое ИЛИ литералов, формула — логическое И дизъюнктов.

Третий вход — двумерный массив formula из пар (Int,Bool). Элемент i — массив литералов i-го дизъюнкта в указанном формате.

Пример XOR двух переменных:

$$f(x)=(x_0\vee x_1)\wedge(\neg x_0\vee\neg x_1).$$

Его описание: [[(0,true),(1,true)],[(0,false),(1,false)]].

Реализуйте на языке Q# оракул формулы f(x), инвертирующий y при f(x)=1. Полные вспомогательные операции из предыдущих упражнений даны в заготовке.

Восстановите исходные значения входного регистра. Решение должно работать на суперпозициях; измерения запрещены.

Заготовка Q#:

namespace Kata {
    import Std.Arrays.*;

    operation Oracle_SATFormula(x : Qubit[], y : Qubit, formula : (Int, Bool)[][]) : Unit is Adj + Ctl {
        // Implement your solution here...

    }

    // You might find these helper operations from earlier tasks useful.
    operation Oracle_SATClause(x : Qubit[], y : Qubit, clause : (Int, Bool)[]) : Unit is Adj + Ctl {
        let clauseQubits = Mapped((ind, _) -> x[ind], clause);
        within {
            for (ind, positive) in clause {
                if not positive {
                    X(x[ind]);
                }
            }
        } apply {
            Oracle_Or(clauseQubits, y);
        }
    }

    operation Oracle_Or(x : Qubit[], y : Qubit) : Unit is Adj + Ctl {
        ApplyControlledOnInt(0, X, x, y);
        X(y);
    }

    operation Oracle_And(x : Qubit[], y : Qubit) : Unit is Adj + Ctl {
        Controlled X(x, y);
    }
}