发表机构
Santa Clara University（圣克拉拉大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对热力学晶格搜索中联合不可满足的需求，提出基于属性注册表契约的检索或拒绝方法，利用冲突诊断生成MUS和修复，在可行查询上精确匹配，在空查询上可靠拒绝并保持约束。
AI 中文摘要
早期的热力学晶格需求是知识密集型的，且常常联合不可满足：工程师要求一个轻质、刚硬、横向导热且廉价的晶胞，而库中没有晶胞满足该要求。设计系统应明确说明这一点，并指出应放宽哪个要求及放宽多少，而不是返回最接近的行。即使库中没有候选，生成模型也能返回一个候选。本工作将成熟的冲突诊断应用于均质化属性目录。在1,397个均质化晶胞和19种基础材料（共26,543种组合）上的搜索返回一个目录行，该行可由第二个求解器重建；或者，对于最多包含八个约束的空可行集，返回包含最小不可满足子集（MUS）及修复的松弛量，而非邻近解。一个注册表声明生成提示和评估器，因此未声明的解析键无法到达搜索。在64个冻结的类型化查询套件上，检索或拒绝在每个可行查询（48/48）上匹配最小修复，并在每个空查询（16/16）上以MUS和松弛量拒绝。忽略约束的最近邻和惩罚搜索违反了规定的成本或密度限制。在216个空查询上，以三位有效数字打印并向外舍入的修复在所有情况下（216/216）保持可行。当必须保持密度和成本时，最小基数修复列表在209/211个查询上保持它们；保护优先修复在所有211个查询上保持它们，与完整诊断相同。一个308请求的解析基准是模板文本检查，而非无约束的工程师散文。
英文摘要
Early thermal-mechanical lattice requirements are knowledge-intensive and often jointly unsatisfiable: an engineer asks for a cell that is light, stiff, laterally conducting and cheap, and no cell in the library satisfies it. A design system should say so, and say which requirement to loosen and by how much, rather than return the nearest row. A generative model can return a candidate even when the library holds none. This work applies established conflict diagnosis to a catalogue of homogenised properties. Search over 1,397 homogenised unit cells and 19 base materials (26,543 combinations) returns a catalogue row that a second solver can rebuild, or, for an empty feasible set of at most eight constraints, inclusion-minimal unsatisfiable subsets (MUS) and the slack of a repair, not a neighbour. One registry declaration generates the prompt and the evaluator, so undeclared parsed keys cannot reach search. On a frozen suite of 64 typed queries, retrieve-or-refuse matches min-repair on every feasible query (48/48) and refuses every empty one (16/16) with MUS and slack. Constraint-ignoring nearest-neighbour and penalty search violate stated cost or density limits. On 216 empty queries, repairs printed at three significant figures and rounded outward stay feasible in every case (216/216). When density and cost must be kept, a list of minimum-cardinality repairs keeps them on 209 of 211 queries; a protection-first repair keeps them on all 211, the same as full diagnosis. A 308-request parse benchmark is a template-text check, not unconstrained engineer prose.
Comments30 pages, 7 figures, 22 tables. Appendices A-D give the full property registry, the generated language-model prompt, the frozen 64-query suite, and one worked tool transcript
