发表机构
Reykjavik University（雷克雅未克大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出精确算法，在多项式时间内计数避免递增模式与231直和的排列（如1342、12453），通过识别受保护状态简化递推，并给出至长度150的计数及随机生成方法。
AI 中文摘要
我们给出一个精确算法，用于计数避免以下固定模式的排列：递增模式与模式231的直和。该家族的首两个成员是1342和12453。对于每个成员，该算法使用多项式次算术运算和多项式个存储整数，计算直到给定界限的所有长度的避免排列数，其度数随模式长度线性增长。我们首先通过从左到右读取排列，并在每一步记录已读字母对未读字母施加的约束，得到一个精确递推。其状态空间呈指数增长，因此直接求值需要指数时间。然后我们证明状态的一部分是受保护的：后续步骤原样携带它且不依赖它。将受保护部分分解出来，可将递推转化为一个动态规划，具有多项式个存储的转移条目，这为家族的每个成员提供了多项式界限。对于模式12453，平移对称性将界限改进为操作次数为七次、存储次数为四次。分别编写的实现和精确的中国剩余定理认证确定了长度至150的所有12453避免排列的数量。先前发表的序列达到长度38。相同的表格也以多项式时间生成均匀随机避免排列。我们用浮点表格抽样的一百万个长度为300的12453避免排列的热图来说明这一点。1342和12453的计数递推在Lean 4证明助手中得到验证。
英文摘要
We give an algorithm counting the permutations that avoid a fixed pattern of the following form: the direct sum of an increasing pattern and 231. The first members of the family are 1342 and 12453. For each member the algorithm uses polynomially many operations and stored integers, with degrees that grow linearly in the length of the pattern. It comes from a recurrence that reads a permutation from left to right and records the constraints that the letters read so far impose on those still unread. This recurrence has exponentially many states, but part of each state is protected: later steps carry it along unchanged and do not depend on it, and factoring the protected part out leaves a dynamic program of polynomial size. For 12453 a translation symmetry sharpens the bounds to degree seven for the operations and degree four for the storage. We also compute the number of 12453-avoiding permutations of every length up to 150. The previously published series, due to Biers-Ariel (2019), reached length 38. We also give a sampler of uniformly random avoiders. A floating-point implementation of it, proved to be within total variation distance $3.5\cdot10^{-5}$ of uniform for ideal random bits, draws the one million 12453-avoiding permutations of length 300 shown in a heatmap. The literal and kernel recurrences for 1342 and 12453 are verified in the Lean 4 proof assistant.
Comments36 pages, 4 figures, 1 table. v2: revised and shortened exposition, corrected account of prior work, the first 151 terms tabulated, a proved error bound for the floating-point sampler (Appendix A), the Lean 4 development described (Appendix B), and Conjecture 10.1 with the exponent left unspecified. Code, data and Lean 4 development: https://github.com/ulfarsson/public-12453
