Z3 import and usage in C++

[ritu-thombre99]

Context:

Z3 is a powerful SMT-solver for wide range of applications. It has been mainly proposed as an optimal solution to qubit mapping and routing problem (more details on mapping and routing with examples in #1928).

When running a quantum circuit on a hardware with certain connectivity constraints, two-qubit gates like CNOTs can only be executed using physical qubits that are connected by an edge on the hardware.

Hence, necessary SWAPs need to be inserted in order to route the logical qubits so that they are mapped to an edge on the device, while respecting other compiling constraint i.e. order the gate dependencies from the input quantum circuit, and ensuring compiled quantum circuit is equivalent to the input quantum circuit.

Following image shows a simple example:

Following is the list of papers that proposed optimal solution using SAT solvers:

• Optimal Layout Synthesis for Quantum Computers wit Z3 implemented in Python
• Improving OLSQ above with more efficient encodings with support in both Python and C++
• Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits implemented in Python
• Qubit Mapping Routing with MAX-SAT Open-WBO-Inc Incomplete MaxSAT Solver implemented in Python
• Old IBM Paper Full-stack, real-system quantum computer studies: Architectural comparisons and design insights which used heuristics and multiple SMT solvers including Z3 C++
• ...

Description of the Change:

1. A sample routing pass with Z3 installed with CMake

Benefits:

1. Intended for research in hybrid optimal-heuristic qubit mapping routing techniques in the future
2. Template to start using Z3 directly in Catalyst

Possible Drawbacks:

1. Z3's cmake name opt clashed with Catalyst's opt. This was resolved using z3.patch but there are still some issues. Patch applies when running a clean build but it will fail with the name conflict error. The 2nd build runs fine since patch was already applied in the last build.
2. Warnings as errors in the top level CMAKE mlir/CMakeLists.txt are disabled for Z3 to compile. If they are enables, the build will always fail.

Related GitHub Issues:

Example Usage:

catalyst % quantum-opt --route-circuit="hardware-graph=(0,1);(1,2);(2,3);(3,4);" input.mlir

Output will show the following Z3 instance information followed by input mlir as is since routing-pass currently doesn't do anything.

        context c;
        expr x = c.bool_const("x");
        expr y = c.bool_const("y");
        expr conjecture = (!(x && y)) == (!x || !y);
        
        solver s(c);
        s.add(!conjecture);
        llvm::outs() <<  "Z3 result " << s.to_smt2() << "\n";
        llvm::outs() <<  "Z3 check " << s.check() << "\n";
        llvm::outs() <<  "sat " << z3::sat << "\n";
        llvm::outs() <<  "unsat " << z3::unsat << "\n";
        llvm::outs() <<  "unknown " << z3::unknown << "\n";

Output:

Z3 result ; 
(set-info :status unknown)
(declare-fun y () Bool)
(declare-fun x () Bool)
(assert
 (let (($x11 (or (not x) (not y))))
(let (($x12 (= (not (and x y)) $x11)))
(not $x12))))
(check-sat)

Z3 check 0
sat 1
unsat 0
unknown 2

[ritu-thombre99]

@mlxd