A separate procedure to encode the circuits

[JingyiMei98]

Now we use quokka-sharp as

    import quokka-sharp as qk
    # the input circuit should be in QASM format
    # compute probability of measurement outcome 0 on the first qubit
    res = qk.Measure("circ1.qasm", "firstzero")
    print(res.prob)
    # compute probability of measurement outcome 0 on the all qubits
    res = qk.Measure("circ1.qasm", "allzero")
    print(res.prob)

To avoid encoding the circuits twice, we can rewrite the function as

    import quokka-sharp as qk
    # the input circuit should be in QASM format
    # compute probability of measurement outcome 0 on the first qubit
    cnf1 = qc2cnf1("circ1.qasm")
    res = qk.Measure(cnf1, "firstzero")
    # compute probability of measurement outcome 0 on the all qubits
    res = qk.Measure(cnf1, "allzero")

[alaarman]

Yes I think that would be much better. Users would also want to be able to export the Weighted DIMACS file. Can they do that from cnf1?

Ideally we also generalize measurement a bit. Can we make it a map with qubit indices to outcomes? Or two arrays? Low priority.

[JingyiMei98]

    from quokka_sharp.encoding import QASMparser, QASM2CNF
    from quokka_sharp import EQ2CNF, EQ_check
    from quokka_sharp import Sim2CNF, Sim
    # the path of the WMC tool
    tool_path = "/Users/meij/GPMC/bin/gpmc"
    # cnf_file_root = " "
    '''
    Simulation
    '''
    # Parse the circuit
    circuit1 = QASMparser(qasmfile1, True)
    # Encode the circuit
    cnf_circ1 = QASM2CNF(circuit1)
    
    # Add constraints of measurement outcome 0 on the first qubit and initial state
    cnf_firstzero = Sim2CNF(cnf_circ1, "firstzero")
    # Write to weighted cnf file 
    cnf_firstzero.write_to_file("circ1_firstzero.cnf")
    # Solving cnf file by a given tool
    res = Sim(tool_path, cnf_firstzero, "circ1_firstzero.cnf", "firstzero")
    print(res.prob)

    # Add constraints of measurement outcome 0 on the all qubits and initial state
    cnf_allzero = Sim2CNF(cnf_circ1, "allzero")
    # Write to weighted cnf file 
    cnf_allzero.write_to_file("circ1_allzero.cnf")
    # Solving cnf file by a given tool
    res = Sim(tool_path, cnf_allzero, "circ1_allzero.cnf", "allzero")
    print(res.prob)    
    
    '''
    Equivalence checking
    '''

    # Parse another circuit
    circuit2 = QASMparser(qasmfile2, True)
    # Get (circuit1)^dagger(circuit2)
    circuit1.dagger()
    circuit1.merge(circuit2)
    # Get CNF for the merged circuit
    cnf = QASM2CNF(circuit1)

    # write to the cnf_file_list containing 2N cnf files under given root (tempfile.gettempdir() by default)
    # N is the number of qubits
    cnf_file_list = EQ2CNF(cnf, cnf_file_root="./")
    res = EQ_check(tool_path, cnf_file_list)
    print(res.result)

Now users can obtain the cnf file for a circuit, the cnf file for a circuit with single measure, the cnf file for a circuit with multi-measure.

[alaarman]

What is the "True" parameter for the parser?
Where is the DIMACS written to disk?

[JingyiMei98]

What is the "True" parameter for the parser?

the parameter is translate_ccx. If it is True, then we translate CCX to clifford+T

Where is the DIMACS written to disk?

Here we write DIMACS to circ1_firstzero.cnf in the current folder

    # Write to weighted cnf file 
    cnf_firstzero.write_to_file("circ1_firstzero.cnf")

[alaarman]

Ok. Will this code go in the text? It is a bit longish.

The translate CCX thing might raise questions, we may want to avoid. We should hide or know how to explain (short).

In the documentation we should make clear that the "weighted CNF" is in "weighted DIMACS" format of WMC competition or whereever this is from (link to specs)

[JingyiMei98]

Maybe we can add DIMACS as an argument

    import quokka-sharp as qk
    # the input circuit should be in QASM format
    # compute probability of measurement outcome 0 on the first qubit
    res = qk.Measure("circ1.qasm", "circ1.qasm.cnf", "firstzero")
    print(res.prob)

for users to written in some DIMACS files directly.

Put the detailed version in the appendix or in the repo.

[alaarman]

Some things, crucial to users, should be explained:

• Do we assume the circuit has no measurements?
• Why are measurements added to the encoding and not to the (parsed) circuit?
• why supply both cnf file and cnf object to the simulator?
• What is the res object? Can we turn this into a probability / boolean (for equivalence checking?
• cnf_file_root wouldn't be needed with proper file handling. A user simply supplies an absolute or a relative path...

For example, an alternative could be:

    import quokka-sharp as qk

    # Simulation with Quokka#:
    circuit = qk.QASMparser("circuit1.qasm")                # Parse a circuit without measurements
    circuit1 = circuit.copy()                                               #Create backup copy
    circuit.add_measurement(cnf_circ1, {0: 0, 1:0} )    # add measurement for |01> on first two quibits
    cnf = qk.QASM2CNF(circuit1)                                   # Encode the circuit
    cnf.write_to_file("circuit1_measure01.cnf")            # Optional: Write as weighted DIMACS file 
    res = qk.Simulate(cnf)                                                # Perform simulation with default GPMC
    print(res.prob)

    # Equivalence checking with Quokka#:
    circuit2 = qk.QASMparser("circuit2.qasm")
    circuit1.dagger()
    circuit1.append(circuit2)
    cnf = QASM2CNF(circuit1)
    res = qk.CheckEquivalence(cnf)
    print(res.result)    

[alaarman]

Ok I think I can see why we need to add measurements to the CNF and not to the QASM file: It is because we check for a certain outcome and maybe QASM doesn't support this.
We should then make clear that we only take circuits without measurements. Does the tool give an error? In my opinion, we cannot just drop measurements (or any other gates) as this would result in unexpected behavior for unsuspecting users. The cases should be handled explicitly.

[alaarman]

Aha, I also see now why you use the file path for equivalence checking: we generate a sequence of CNF files.

What about?:

    # Equivalence checking with Quokka#:
    circuit2 = qk.QASMparser("circuit2.qasm")
    circuit1.dagger()
    circuit1.append(circuit2)
    cnf = QASM2CNF(circuit1)
    for i in range(circuit1.nr_quibits):
        for P in ["X", "Z"]:
           res = qk.CheckEquivalence(cnf)
           cnf.add_constraint(P, i)
           # cnf. write_to_file("circuit1-circuit2-check"+ P +str(i) +".cnf")
           if !res:     print("Non-Equivalent")    
    print("Equivalent")    

To be clear, I like non of the approaches. We should figure out what is easy to present in the paper and in the tool library interface (documentation).

We could also choose omit the description of how to store equivalence check CNF files in the paper?

[alaarman]

Note also that we assume the initial state is |000000>. We could make this explicit in the interface or we hardcode this assumption. In either case the paper should mention it.

[JingyiMei98]

Ok I think I can see why we need to add measurements to the CNF and not to the QASM file: It is because we check for a certain outcome and maybe QASM doesn't support this. We should then make clear that we only take circuits without measurements. Does the tool give an error? In my opinion, we cannot just drop measurements (or any other gates) as this would result in unexpected behavior for unsuspecting users. The cases should be handled explicitly.

Our tool throw an error for undefined gates and throw syntax error for measurement and barrier.

[JingyiMei98]

To sum up, we should

• make initial constraint for |0...0> explicit in the interface and mention this in the paper.
• make this clear in the paper: we take circuits without measurement
• turn res object into a probability / boolean (for equivalence checking)
• extend "single-", "multi-" to a general measurement
• have a better interface

[JingyiMei98]

I will make simulation look like:

    import quokka-sharp as qk

    # Simulation with Quokka#:
    circuit = qk.QASMparser("circuit1.qasm")                # Parse a circuit without measurements
    circuit.add_measurement(cnf_circ1, {0: 0, 1:0} )    # add measurement for |01> on first two quibits
    cnf = qk.QASM2CNF(circuit1)                                   # Encode the circuit
    cnf.write_to_file("circuit1_measure01.cnf")            # Optional: Write as weighted DIMACS file 
    prob = qk.Simulate(cnf)                                                # Perform simulation with default GPMC

and equivalence checking:

    circuit1 = qk.QASMparser("circuit1.qasm")
    circuit2 = qk.QASMparser("circuit2.qasm")
    circuit1.dagger()
    circuit1.append(circuit2)
    cnf = QASM2CNF(circuit1)
    are_equivalent = qk.CheckEquivalence(cnf)
    print(are_equivalent)   
    # True or False

We omit the list of cnf files writing process and store them in the tempfile. Maybe we just tell the users where to find those files?

[alaarman]

Sounds good, May. Yes, let's refer to the included CNF files (and maybe a README where we can add more details on equivalence checking later).

@timcp Do you agree?