Unextendible product bases (UPBs) are important structures in quantum information theory, with applications to completely entangled subspaces, bound entanglement, and local indistinguishability. Since many properties and applications of UPBs are closely related to their cardinalities, one of the central problems in the study of UPBs is to determine whether UPBs of prescribed sizes exist in a given multipartite system. In this paper, we introduce a SAT-assisted framework based on decompositions of the
N-dimensional hypercube. We define
ON-tile decompositions and prove a tile-to-UPB theorem: every
ON-tile decomposition induces a UPB through a construction based on tile-wise Fourier product bases and a global stopper state. We then encode the search for such decompositions as a Boolean satisfiability (SAT) problem and use SAT solvers to generate explicit instances. In terms of verification, we also implement a UPB verification algorithm based on local orthogonality graphs and unsaturated subspaces. The algorithm can be used to determine whether an arbitrary finite set of product states forms a UPB. Using this framework, we obtain UPBs of several sizes in some tripartite and quadripartite systems, including sizes
13,14,…,23 in
C3⊗C3⊗C3. Moreover, the small-dimensional instances obtained here can serve as seed UPBs for recursive constructions, leading to further examples in larger multipartite systems.
Unextendible product bases (UPBs) play a key role in the study of quantum entanglement and nonlocality. A famous open question is whether there exist genuinely unextendible product bases (GUPBs), namely multipartite product bases that are unextendible with respect to every possible bipartition. Here we shed light on this question by providing a characterization of UPBs and GUPBs in terms of orthogonality graphs. Building on this connection, we develop a method for constructing UPBs in low dimensions, and we derive a lower bound on the size of any GUPB, significantly improving over the state of the art. Moreover, we show that every minimal GUPB saturating our bound must be associated to regular graphs. Finally, we discuss a possible path towards the construction of a minimal GUPB in a tripartite system of minimal local dimension.