Home · Installation · Usage · Reference

Usage

Synthesis is run with the milq script in the repository root. It can be started from any directory, also through a symlink on your PATH (Installation): paths are relative to the current directory, which is also where the output files go.

$ ./milq [options] <input.qasm>

All options are listed in the command-line reference. This page walks through the choices you usually make.

Input circuits

The input is an OpenQASM 2.0 or 3.0 file with a single quantum register. Examples are in benchmarks/.

Registers: qreg q[n]; / creg c[n]; (2.0), or qubit[n] q; / bit[n] c; (3.0). A second quantum register is rejected.
Gates without parameters, one per statement, applied to distinct qubits q[i] of the register: h, x, y, z, s, sdg, t, tdg, sx, sxdg, id, cx, cy, cz, ch, cs, csdg, csx, swap, iswap, sqrtswap, dcx, xcx (a CX controlled on |0⟩), ccx, cswap and ccz. A single-qubit gate on the whole register (h q;) applies to each qubit.
Measurements at the end: measure q[i] -> c[i]; (2.0) or c[i] = measure q[i]; (3.0). A gate on a qubit that was already measured is rejected. See Measurements.
Comments and barrier statements are skipped.
gate definitions of the gates above are accepted when they are MILQ’s own or have the same unitary up to global phase (as Qiskit writes them); the gate is simulated natively. Their bodies can use the gates above, p, u1 and rz with a multiple of π/4, and gates defined before them that take no parameters or don’t use them. Other definitions are skipped, and using their gate is an error.

1. Pick what must be preserved (`-v`)

MILQ simulates the input circuit on a set of input states and requires the synthesized circuit to produce the same output states.

`-v`	Input states	Meaning
`all` (default)	all 2ⁿ computational basis states	the two circuits implement the same unitary
`zero`	only \|0…0⟩	state preparation: the same state is produced from \|0…0⟩
`jamiolkowski`	one maximally entangled state on 2n qubits	the same unitary, checked with a single vector
`rus`	\|0⟩, \|1⟩ and \|+⟩ on the targets, ancillas in \|0⟩	repeat-until-success circuits, see below

-v zero is usually much faster than -v all, but it only guarantees the state prepared from |0…0⟩:

$ ./milq -s smt -a cvc5 -v zero benchmarks/ghz/3.qasm
...
h q[2];
cx q[2], q[1];
cx q[2], q[0];

2. Pick a backend (`-s`, `-a`, `-c`)

`-s`	`-a`	What runs
`smt`	a solver name	The formula is sent to an external SMT solver. In incremental mode a single solver keeps running, and new layers are added with `push`/`pop`.
`smt`	`portfolio`	All compatible SMT solvers run in parallel on each formula, and the first answer wins. Solvers that fail are skipped.
`gurobi` (default)	`gurobi`	The problem is built directly in Gurobi’s Python API.
`milp`	`gurobi` or `cbc`	The problem is built as a PuLP model and solved by Gurobi or by CBC. CBC ships with PuLP, so it needs no license.

The complex-number representation (-c) decides which SMT solvers can be used:

`-c`	Arithmetic	SMT solvers
`FiveTuple` (default)	exact, linear integer (QF_LIA)	yices2, cvc5, OpenSMT, SMTInterpol, z3
`Classic`	floating point a + bi, nonlinear real (QF_NRA)	yices2, cvc5, z3, dReal

FiveTuple is exact and usually the fastest choice for Clifford+T circuits. Classic is needed for end-of-circuit measurements and is the practical choice for approximate synthesis.

$ ./milq -s smt -a opensmt benchmarks/ghz/2.qasm      # FiveTuple, OpenSMT
$ ./milq -s gurobi -c Classic -v zero benchmarks/ghz/2.qasm

3. Pick a search mode (`-m`)

`-m`	What it does
`incremental` (default)	Tries 0, 1, 2, … layers until a circuit is found, so the result has the minimum number of gates. With `--max-depth N` it gives up once no circuit with at most N gates exists.
`basic`	Encodes a fixed number of layers d (the input’s gate count, or `-d`) and solves once. Gurobi minimizes the gate count within d layers. SMT solvers return some circuit with at most d gates.
`bottomup`, `topdown`, `binary`	Encode d layers like `basic`, then search over a bound on the gate count: upwards from 0, downwards from d + 1, or by bisection.
`pareto-incremental`	Enumerates all circuits depth by depth and keeps a Pareto front: gate count vs. cost by the gate weights (e.g. T-count), or for `-v rus` T-count vs. probability of success. Every point is written to `pareto_front/` and the front is plotted to `pareto_front.pdf`. It runs until the `-pt` time limit or `--max-depth`.

The gate set is the set of gates in the input circuit plus Clifford+T (x, z, h, s, sdg, t, tdg, cx). Every gate costs 1. An empty layer (id) costs 0, so circuits shorter than d are allowed in the fixed-depth modes.

$ ./milq -s smt -a yices2 -m bottomup benchmarks/ghz/2.qasm

Measurements

If the input circuit measures qubits at the end, the synthesized circuit must produce the same post-measurement state, and that requires -c Classic. To ignore the final measurements instead, pass -nm. Circuits from MQT Bench end with measurements, for example:

$ ./milq -s smt -a yices2 -nm benchmarks/mqt-bench/ghz_nativegates_clifford+t_opt2_2.qasm

Equivalence up to global phase

With -u, the synthesized circuit may differ from the input by a global phase. For FiveTuple, the phase is a multiple of π/4.

$ ./milq -s smt -a yices2 -u benchmarks/ghz/2.qasm

Approximate synthesis

With -ap, the circuits only need an average fidelity of at least -f (default 1.0). The fidelity constraint is nonlinear. Gurobi handles small instances quickly, while SMT solvers can take very long.

$ ./milq -ap -f 0.9 -c Classic -s gurobi -v zero benchmarks/ghz/2.qasm

Repeat-until-success circuits

With -v rus, the input circuit is treated as a repeat-until-success (RUS) circuit with -T target qubits (the lowest indices) and -A ancilla qubits (the highest indices). The input states are |0⟩, |1⟩ and |+⟩ on the targets, with the ancillas in |0⟩. The cost counts only t/tdg gates (T-count). Examples are in benchmarks/rus/.

$ ./milq -v rus -T 1 -A 1 -c Classic -s gurobi benchmarks/rus/2/spec.qasm

Note: RUS instances need a full Gurobi license; they exceed the size-limited one.

Output

On success, milq prints the timing of each phase and the synthesized circuit (the exit statuses are listed in the reference):

synthesis successful
Full time: 0.27 seconds
Parsing time: 0.002 seconds
Encoding time: 0.11 seconds
Solving time: 0.15 seconds
Updating time: 0 seconds
OPENQASM 3.0;
...

The circuit is written to a file only with -o. The following files are written:

File	Content
with `-o`: that path	the synthesized circuit in OpenQASM 3.0
with `-o`: the same name with `.smt2` or `.lp`	the last formula given to the solver
with `-o` and `-v rus -m pareto-incremental`: the same name with `_recovery.qasm`	the recovery circuit of the returned circuit (without `-o`, it is only in `pareto_front/`)
with `--log`: `synth.log` in the current directory (`--log PATH` for another file)	a detailed log of the run, including Gurobi’s output (`--verbose` adds debug messages)

Without --log, --verbose prints that log, with the debug messages, to stdout before the result.

Warnings, e.g. that Gurobi stopped early and the cost is not proven minimal, are also printed to stderr.

Note: The directory of the -o path must already exist.

The circuit file uses include "stdgates.inc";. If it uses gates that are not in the standard library (e.g. sxdg, dcx, ccz), their definitions are added at the top. End-of-circuit measurements are written at the end, into the same classical bits as in the input (e.g. measure q[0] -> c[1]; becomes c[1] = measure q[0];), with the classical declarations of the input (creg c[2]; is declared as bit[2] c;). The file can be loaded by other tools, for example with qiskit.qasm3.loads.

Known limitations

Known limitations and planned features are tracked as issues on GitHub.