Квантовый оракул формулы Exactly-1 3-SAT

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

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

Третий вход — двумерный массив formula из пар (Int,Bool). Элемент i задаёт литералы i-го дизъюнкта; каждый дизъюнкт гарантированно содержит ровно три литерала. Здесь он считается выполненным, только если ровно один из трёх литералов истинен. Формула выполнена, если это верно для всех её дизъюнктов.

Пример: формула с одним дизъюнктом $(x_0\vee x_1\vee x_2)$ задана [[(0,true),(1,true),(2,true)]]. Её решения — (true,false,false), (false,true,false), (false,false,true).

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

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

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

namespace Kata {
    import Std.Arrays.*;

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

    }

    // You might want to implement this helper operation that evaluates a single clause and use it in your solution.
    operation Oracle_Exactly13SATClause(x : Qubit[], y : Qubit, clause : (Int, Bool)[]) : Unit is Adj + Ctl {
        // Implement your solution here...

    }

    // You might find these helper operations from earlier tasks useful.
    operation Oracle_Exactly1One(x : Qubit[], y : Qubit) : Unit is Adj + Ctl {
        for i in 0..Length(x) - 1 {
            ApplyControlledOnInt(2^i, X, x, y);
        }
    }

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