一句话：提出半声明式语言 SetLah!，用分层块表达组合搜索并编译到 ASP，兼得模块化与高效求解。
组合搜索需要在指数级候选空间中寻找满足约束的解，常见做法是使用 SAT 求解，但手工把高层需求翻译为布尔子句既繁琐又牺牲清晰性与模块化。ASP 提供了更高层的规则式语言，并可通过有限域推理自动编译到求解器，但其稳定模型语义难以建立直觉，不支持任意一阶逻辑公式作为约束，程序也往往单体化而难以复用。本文提出 SetLah!，一种面向组合搜索的半声明式语言。SetLah! 程序由分层块组成，每块包含定义搜索空间的规则以及用于剪枝的任意一阶逻辑约束，这种结构支持模块化问题分解，并给出逐块生成与过滤候选解的直观语义。作者实现了从 SetLah! 到 ASP 的编译器，以复用高效 ASP 求解器并自动优化生成编码。实验表明，SetLah! 对常见组合搜索问题能给出更简洁直观的规格，其编译得到的 ASP 编码可显著优于基于 SAT 的工具。
Combinatorial search—finding solutions that meet constraints within an exponentially large space of candidates—underpins problems from hardware verification to scheduling and combinatorial design. The most successful approach in practice is Propositional Satisfiability (SAT) solving, but modelling a problem for a SAT solver requires manually translating high-level requirements into conjunctions of boolean clauses, a tedious step that sacrifices clarity and modularity. Answer Set Programming (ASP) offers a higher-level alternative, with a rule-based language whose variables and finite-domain reasoning yield more compact problem descriptions that can be automatically compiled into low-level solver input. Yet, ASP has its own shortcomings: its semantics, defined via a notion of stable models, is hard to build intuition for; it does not allow arbitrary first-order logic formulas as constraints; and its programs tend to be monolithic, making modular design and reuse difficult. We propose SetLah!, a semi-declarative language for combinatorial search that addresses the shortcomings of both SAT and ASP. A SetLah! program is a sequence of stratified blocks, each containing rules that define the search space and arbitrary first-order logic constraints that prune it. This block structure enables modular problem decomposition, allowing for an intuitive semantics: candidate solutions are generated and filtered block by block. We built a compiler from SetLah! programs into ASP, allowing us to take full advantage of the existing efficient ASP solvers, while also automatically optimising the generated encodings. Our empirical evaluation demonstrates that SetLah! offers substantially more concise and intuitive specifications for common combinatorial search problems, and its compiled ASP encodings can significantly outperform SAT-based tools.