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. Here we provide an equivalent characterization of UPBs in graph-theoretic terms. Different from previous graph-theoretic investigations of UPBs, which focused mostly on the orthogonality relations between different product states, our characterization includes a graph-theoretic reformulation of the unextendibility condition. Building on this characterization, we develop a constructive method for building UPBs in low dimensions and shed light on the open question of whether there exist genuinely unextendible product bases (GUPBs), that is, multipartite product bases that are unextendible with respect to every possible bipartition. We derive a lower bound on the size of any candidate 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 and discuss a possible path towards the construction of a minimal GUPB in a tripartite system of minimal local dimension. Finally, we apply our characterization to the problem of distinguishing UPB states under local operations and classical communication, deriving a necessary condition for reliable discrimination in the asymptotic limit.