Automated Construction and Verification of Unextendible Product Bases

Technical Summary: Automated Construction and Verification of Unextendible Product Bases

Problem Statement
Unextendible Product Bases (UPBs) are finite sets of mutually orthogonal product states whose orthogonal complement contains no nonzero product state. They are fundamental to quantum information theory, serving as the source for completely entangled subspaces (CES) and bound entangled states. A central challenge in the field is determining the existence of UPBs with prescribed cardinalities in specific multipartite Hilbert spaces. While theoretical bounds exist (e.g., the Alon-Lovász bound), the systematic construction of UPBs with diverse sizes, particularly in multipartite systems with local dimensions greater than two, remains difficult. Existing methods often rely on manual design of "seed" decompositions or are restricted to bipartite or qubit systems.

Methodology
The authors propose a unified framework that automates the construction and verification of UPBs through three integrated components:

1. $O_N$-Tile Decompositions and the Tile-to-UPB Theorem:
   The authors generalize the concept of "tiles" from 2-cube decompositions to $N$-dimensional hypercubes ($C = \mathbb{Z}_{d_1} \times \dots \times \mathbb{Z}_{d_N}$). They define an $O_N$-tile decomposition as a partition of the hypercube into tiles such that the union of any proper subset of tiles (with size between 2 and $s-1$) does not form a single tile.
   They prove a Tile-to-UPB Theorem: Every $O_N$-tile decomposition induces a UPB. The construction involves:

   • Generating a tile-wise Fourier product basis for each tile.
   • Removing the "all-zero" Fourier state from each tile's basis.
   • Adding a single global "stopper" state (the tensor product of uniform superpositions over all local dimensions).
     The resulting set is proven to be a UPB with cardinality $|U| = (\prod d_i) - s + 1$, where $s$ is the number of tiles.

2. SAT-Assisted Search:
   To find valid $O_N$-tile decompositions with a specific number of tiles $s$, the authors encode the problem as a Boolean Satisfiability (SAT) problem. The encoding includes constraints for:

   • Admissibility: Tiles must be proper subsets in at least two coordinates.
   • Covering: Every point in the hypercube must be covered by at least one tile.
   • Non-overlap: Selected tiles must be disjoint.
   • Non-combinability: No union of a proper subset of selected tiles (size $>1$) can form a Cartesian product (ensuring the $O_N$ condition).
   • Cardinality: The total number of selected tiles must equal $s$.
     Modern SAT solvers are used to generate explicit decompositions for specific systems.

3. Verification Algorithm:
   To certify the generated sets, the authors implement a verification algorithm based on local orthogonality graphs and unsaturated subspaces.

   • Orthogonality Check: Verifies that the union of local orthogonality graphs (one for each subsystem) forms a complete graph.
   • Unextendibility Check: Verifies that the set of product states cannot be covered by a collection of "unsaturated" sets (subsets of states whose local components do not span the local Hilbert space).
     The algorithm efficiently enumerates Maximal Unsaturated Sets (MUS) using a subspace-closure method. The authors report that this method scales significantly better than existing tools like QETLAB's IsUPB function for larger instances.

Key Contributions

• Theoretical Bridge: Established a rigorous $N$-partite Tile-to-UPB theorem, generalizing previous bipartite results and providing a structural link between hypercube decompositions and UPBs.
• Automated Construction: Developed a SAT-based pipeline that removes the need for manual seed design, enabling the discovery of UPBs with diverse cardinalities in high-dimensional multipartite systems.
• Efficient Verification: Introduced an exact verification algorithm based on orthogonality graphs that outperforms existing benchmarks in speed and scalability.
• New Instances: Successfully constructed UPBs in tripartite and quadripartite systems that were previously unknown.

Results
Using the SAT-assisted framework, the authors generated explicit UPB instances for several systems. A primary result is the construction of UPBs in the tripartite system $\mathbb{C}^3 \otimes \mathbb{C}^3 \otimes \mathbb{C}^3$.

• Cardinality Range: They found UPBs of sizes 13, 14, ..., 23 in $\mathbb{C}^3 \otimes \mathbb{C}^3 \otimes \mathbb{C}^3$.
• Comparison: Prior to this work, only sizes 7 and 19 were known for this specific system.
• Recursive Potential: The small-dimensional instances obtained serve as "seed" UPBs. By combining these with existing recursive construction lemmas (e.g., Lemma 2 from [24]), the authors demonstrate how to generate infinite families of UPBs in larger multipartite systems (e.g., $\mathbb{C}^3 \otimes \mathbb{C}^3 \otimes \mathbb{C}^d$).
• Performance: The verification algorithm was benchmarked against QETLAB, showing order-of-magnitude improvements in verification time for UPBs of size 9 and above.

Significance
The paper claims that this work provides a systematic, automated pipeline for generating UPBs, moving beyond the reliance on manually designed constructions. By solving the combinatorial problem of $O_N$-tile decompositions via SAT, the authors expand the known landscape of UPB cardinalities in multipartite systems. The resulting UPBs provide explicit examples of completely entangled subspaces and bound entangled states. Furthermore, the ability to generate diverse seed UPBs facilitates the recursive construction of UPBs in systems with larger local dimensions, offering new resources for the study of quantum nonlocality without entanglement and bound entanglement. The authors note that the data, including symbolic product bases and verification certificates, are made available for further study.