Semi-declarative Language for Combinatorial Search

Full abstract

Read the full abstract

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.