Given a constraint satisfaction problem (CSP) predicate $P \subseteq D^r$, the non-redundancy (NRD) of $P$ is maximum-sized instance on $n$ variables such that for every clause of the instance, there is an assignment which satisfies all but that clause. The study of NRD for various CSPs is an active area of research which combines ideas from extremal combinatorics, logic, lattice theory, and other techniques. Complete classifications are known in the cases $r=2$ and $(|D|=2, r=3)$. In this paper, we give a near-complete classification of the case $(|D|=2, r=4)$. Of the 400 distinct non-trivial Boolean predicates of arity 4, we implement an algorithmic procedure which perfectly classifies 397 of them. Of the remaining three, we solve two by reducing to extremal combinatorics problems -- leaving the last one as an open question. Along the way, we identify the first Boolean predicate whose non-redundancy asymptotics are non-polynomial.

翻译：给定约束满足问题（CSP）谓词 $P \subseteq D^r$，$P$ 的非冗余性（NRD）定义为在 $n$ 个变量上规模最大的实例，使得对于该实例的每个子句，存在一个满足所有子句但该子句的赋值。针对不同 CSP 的非冗余性研究是一个活跃领域，它融合了极值组合学、逻辑学、格论及其他技术的思想。在 $r=2$ 以及 $(|D|=2, r=3)$ 的情况下，已有完整分类。本文给出了 $(|D|=2, r=4)$ 情况的近乎完整分类。在 400 个不同的非平凡四元布尔谓词中，我们通过算法程序完美分类了其中 397 个。对于剩余的三个，我们通过将其归约至极值组合学问题解决了两个——最后一个作为开放问题留待后续。在此过程中，我们首次识别出一个非冗余性渐近行为呈非多项式特征的布尔谓词。