Answer Set Programming for PCG: the Good, the Bad, and the Ugly Ian Horswill 1 Northwestern University, Evanston IL ian@northwestern.edu Abstract This paper is an attempt to work through the sources of its Declarative languages allow designers to build procedural difficulty and power in the hopes of teasing them apart. content generation systems without having to design and de- The four claims of the paper are that (1) ASP’s difficulty bug specialized generation algorithms. Instead, the designer comes in part from its nonmonotonicity: the ability to draw describes the desired properties of the objects to be generated, inferences based on the absence of information. Nonmono- and a general-purpose constraint-solver constructs the de- sired artifact. Answer-Set Prolog (Gebser et al., 2012; tonicity is important for domains such as legal reasoning. Lifschitz, 2008b) is a popular family of languages and solvers But to the extent that procedural content generation is gen- used in procedural content generation research. Answer set erally a perfect-information problem, default reasoning is of programming is very powerful, with mature implementations lesser value. I would argue that (2) being simpler, classical and a significant user base outside the PCG community. monotonic logic is preferable when applicable. That said, However, ASP uses stable-model semantics (Gelfond & Lifschitz, 1992), which is subtle and difficult. In this paper, ASP is more powerful than classical first-order logic insofar I will present some of the history and motivation underlying as it can express concepts such as transitive closure. I would stable model semantics in as non-technical manner as I can argue that (3) the source of that power is ASP’s use of min- manage, and discuss its advantages and disadvantages. I will imization in its semantics. Since minimization does not re- argue that while it is appropriate for some very difficult PCG quire nonmonotonicity, (4) I suggest we explore logics that tasks, the simpler semantics of classical monotonic logic may be preferable for tasks not requiring ASP’s non-monotonic- support minimization while retaining monotonicity, such as ity. FO(TC), first-order logic with the addition of a transitive closure operator. In my experience, the difficulty of ASP is not especially Executive Summary controversial. For the skeptical, I submit as evidence that This is basically a one-paragraph position paper intended to my one-paragraph position statement is packaged with eight spark conversation, followed by several pages of tutorial on pages of tutorial. One can also compare the standard text- to explain this paragraph to those not steeped in stable model books on ASP (Gebser et al., 2012; Lifschitz, 2019) to text- semantics. Readers who are steeped in ASP may wish to books for other languages. It’s not quite as bad as if How to read just the first three paragraphs of the paper, while those Design Programs (Felleisen et al., 2018) or Structure and unfamiliar with logic programming, may wish to skip to the Interpretation of Computer Programs (Abelson et al., 1996) next section (Declarative PCG Example), and those unfa- began with the Church-Rosser theorem, but they require miliar with formal logic may wish to skip to the section after dramatically more mathematical sophistication than those that (Introduction). texts or Clocksin and Mellish (Clocksin & Mellish, 2003), Answer-Set Programming (Gebser et al., 2012; Lifschitz, the canonical Prolog text. While I do teach classes in which 2019, 2008b) is an extremely useful tool for procedural con- students without programming experience make PCG sys- tent generation (A. M. Smith, 2017; A. M. Smith & Mateas, tems using constraint programming (Horswill, 2018b) and 2011, 2010; Summerville et al., 2018). It can express and logic programming (Horswill, 2020), in my experience stu- solve problems that are beyond the capability of other de- dents find ASP much more challenging. clarative languages. However, it is also notoriously tricky. One of the appeals of constraint programming for PCG is that constraints operate relatively independently of one 1 Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). another. Something is a model of a program if and only if it Under classical logic, the models are the ones that don’t con- satisfies each constraint in the program. If your generator tradict any constraints. That gives us four different models generates a problematic model, you can add a constraint to (the ones in green), and so four possible characters that can rule it out. If it fails to generate what you believe to be a be generated. valid model, that model must violate at least one constraint. A naïve, line-by-line translation of the constraints above You can find it and fix it. These properties do not hold in into ASP would read: ASP: adding a rule can add models, remove them, or both. I once spent 20 minutes with a Ph.D. student working on an :- ebullient, depressive. ASP thesis, one doing an SMT thesis, and one doing a PL depressive :- tanner. semantics thesis, puzzling over why a 12-line ASP program was unsatisfiable. We were able to write ASP programs that The first line says ebullient and depressive together form a did the job, but we were never able to determine why that contradiction. The second says that tanner implies depres- particular one didn’t. sive. However, this program only has one solution under ASP (one stable model): the model in which all propositions are false. The technical description in terms of stable-model Declarative PCG Example semantics is complicated, but in this case it boils down to our not having provided any rules for concluding ebullient The core idea of declarative PCG is to describe the objects or tanner are true. In the absence of such rules, ASP requires to generate in terms of a set of choices or degrees of freedom them be false. And indeed ASP solvers such as clingo for the objects, together with constraints on how those (Gebser et al., 2010) issue warnings when reading such a choices interact. It’s difficult to generate an example that is program. Depressive can’t be true either because it can only compact, gets at the issues, is fair to both classical logic and be true when tanner is true, and tanner is never true. Thus, ASP, and doesn’t require having first read the rest of the pa- all three propositions are false. per. But here’s my attempt. This is unfair to ASP because an ASP programmer would Let suppose we’re generating personalities for characters, know not to write it this way. They would more likely write by selecting traits, as is common in commercial games such it as: as Dwarf Fortress (Adams & Adams, 2006), The Sims (Evans, 2009; Maxis, 2009), and City of Gangsters (Zubek 0 { ebullient; depressive } 1. et al., 2021; Zubek & Viglione, 2021), which does use a ran- { tanner }. domized SAT solver (Horswill, 2018a). To keep things sim- depressive :- tanner. ple, we’ll assume there are two personality traits, ebullient and depressive. A character can be either of these but not The first line here says that both ebullient and depressive both at once. And in homage to One Night Ultimate Were- can be freely chosen, but at most one can be true. The sec- wolf (Alspach, 2009), all tanners are depressive. This gives ond says that tanner can be freely chosen. These lines are us two constraints: syntactic sugar for more complicated systems of rules, which are outside the scope of this paper, see (Gebser et al., 𝐶𝐶1: ¬(ebulluent ∧ depressive) 2012). For this desugared ASP program, all four classical C2: tanner → depressive models are stable. Again, this is an unfair comparison for ASP, both because This has three different propositions for eight different truth it makes ASP look more verbose, and also because experi- assignments, and two different constraints that may be sat- enced ASP programmers wouldn’t make this specific mis- isfied or contradicted by any given truth assignment: take. But it is indicative of the kind of mistake that it’s easy to make as one develops a program, such as forgetting to Ebullient Depressive Tanner Contradicts explicitly include a choice rule, or being misled by different F F F None ways of saying something that one might naively assume to F F T C2 be equivalent, or simply forgetting they are different. F T F None In the remainder of the paper, I’ll explain the background underlying the position statement. I want to emphasize that F T T None ASP is unquestionably useful. I am questioning only T F F None whether it makes sense to adopt the restriction to stable T T F C1 models when working on problems like the one above that T T T C1 don’t require it. Introduction programs (which are different), and the semantic difficulties encountered by traditional logic programming languages Declarative programming languages (e.g. constraint pro- that motivated the development of stable-model semantics. gramming, Prolog, ASP) are very attractive for PCG. They Section headings are provided to help the reader to skip over allow a designer to describe the choices involved in gener- material they’re already familiar with. I will then present ating an artifact, along with constraints on the relationships stable-model semantics and discuss the kinds of situations between those choices, leaving it to the system to find ex- in which it is invaluable. I will also discuss why it is so amples (models) that satisfy those constraints. They have difficult to understand and some possible alternatives. been used successfully both by commercial game develop- ers (Zubek & Viglione, 2021) and non-programmers (Horswill, 2018b) for generation of characters, in-game Semantics of logic items, character relationship maps, and prompts for table- A formal logic is a compositional language for formulating top role-playing games. truth statements. It is a set of symbol strings, referred to as Answer-Set Prolog (Lifschitz, 2008b) is an extremely sentences or well-formed formulae (WFFs), defined by powerful family of declarative languages and solvers. It has some recursive grammar, together with some set of semantic been used for a number of procedural content generation rules that relate the meaning of a sentence to the meaning of tasks (A. M. Smith & Mateas, 2011), ranging from level its constituents so that, for example, the meaning of 𝐴𝐴 ∧ 𝐵𝐵 generation (A. Smith, 2011) to generation of complete is derived from the meanings of 𝐴𝐴 and 𝐵𝐵. games and their critiques (Summerville et al., 2018). A theory in a logic is simply a set of sentences, all of ASP provides a number of clear advantages: which are asserted to be true. In most logics, this will be equivalent to the conjunction of those sentences. Thus, we • It provides an expressive and concise first-order will treat the theory {𝐴𝐴, 𝐵𝐵} and the sentence 𝐴𝐴 ∧ 𝐵𝐵 as inter- language for describing problems. changeable. • It supports pseudo-Boolean constraints, which al- Formal logics largely divide into classical and intuition- low natural expression of taxonomic constraints, istic logics, 2 with the distinction being roughly that classical build-point systems, and “pick 𝑁𝑁 from a menu” logics commit to every sentence having a simple truth value, constraints. while intuitionistic logics do not. Semantic systems for in- • It works in part by transforming programs to SAT tuitionistic logics often identify the meaning of a sentence problems, allowing users to leverage the consider- with the possible proofs of the sentence, while those for clas- able progress in high performance SAT solving. sical logics identify it with the possible mathematical ob- • It offers mature, highly optimized implementations jects for which it is true (its models). 3 Although intuition- with a sizable user base (Gebser et al., 2010, 2012) istic logics are more relevant for much of CS, logic program- • It is a non-monotonic logic, which makes it natural ming semantics is somewhat surprisingly grounded in clas- for planning and default reasoning tasks. sical logic. The first four of these, I think are non-problematic. How- ever, the last of these, its non-monotonic semantics based on Important syntactic categories “stable” models (Gelfond & Lifschitz, 1992), while power- In most logics, an atom is a either a proposition symbol such ful, is both subtle and difficult. Here I will try to unpack as 𝐴𝐴 or 𝐵𝐵, or the application of a predicate to some argu- those semantics in a way that is more accessible those that ments, such as 𝑃𝑃(𝑎𝑎, 𝑏𝑏) or 𝑄𝑄(𝑓𝑓(𝑎𝑎), 𝑏𝑏)). A literal is either an those that are often given (Gebser et al., 2012; Lifschitz, atom (a positive literal) or its negation (a negative literal). 2008a). 𝐴𝐴 is a positive literal, ¬𝐵𝐵 is a negative literal. An atom/lit- I will assume here that the reader has a basic undergradu- eral containing no variables is said to be a ground atom/lit- ate familiarity with set theory, (classical) propositional eral. logic, and first-order logic, but will not assume the reader In classical propositional logic, a (disjunctive) clause is a knows or remembers any of the details of Tarskian model disjunction of literals, e.g. 𝐴𝐴 ∨ ¬𝐵𝐵. Any theory has an theory. I will begin by briefly reviewing the model-theoretic equivalent form as a set of clauses. Any clause is equivalent semantics of classical logic, the semantics of positive logic to one or more implications, in which one disjunct is 2 There are a number of more exotic logics, particularly substructural logics, 3 Various non-Tarskian model theories exist for intuitionistic logics, such that don’t fit cleanly into these distinctions. For example, linear logic seeks as those based on Heyting algebras. In particular, Heyting showed that to combine properties of both. However, these come more naturally as ex- particular kinds of subsets of the real line can be used as a kind of model plorations of proof theory, and their model theories are their semantic the- for intuitionistic logic. However, these are more technical devices for stud- ories are well outside the scope of this paper. ying proof systems than useful systems for relating a theory in the logic to some outside system it’s trying to describe. implied by the conjunction of the negations of the others. and complete (i.e. good) iff syntactic entailment and seman- Thus 𝐴𝐴 ∨ ¬𝐵𝐵 ∨ 𝐶𝐶 is equivalent to ¬𝐴𝐴 ∧ 𝐵𝐵 → 𝐶𝐶, 𝐵𝐵 ∧ ¬𝐶𝐶 → tic entailment are the same. 𝐴𝐴, and ¬𝐴𝐴 ∧ ¬𝐶𝐶 → ¬𝐵𝐵. A Horn clause is a clause with at most one positive literal. It is therefore equivalent to an im- Minimal Herbrand models plication with no negative literals. For example, ¬𝐴𝐴 ∨ ¬𝐵𝐵 ∨ We will focus primarily on one particular domain of models, 𝐶𝐶 is a horn clause equivalent to 𝐴𝐴 ∧ 𝐵𝐵 → 𝐶𝐶. the Herbrand base, which consists of all of the ground atoms Clauses in first-order logic are more complicated because constructible from the symbols appearing in the theory. of quantifiers. Automated reasoning systems typically focus Many logic programming systems take 𝐷𝐷, the domain of on theories composed of universally quantified clauses, that possible models, to be the set of possible subsets of the Her- is, clauses of the form ∀𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 . 𝐿𝐿1 ∨ … ∨ 𝐿𝐿𝑚𝑚 where the 𝐿𝐿𝑖𝑖 brand base. These Herbrand models are thus just sets of are literals over the variables 𝑥𝑥𝑗𝑗 . ground atoms. In particular, they are the set of ground atoms taken to be true within the model. Satisfaction If a theory has a model at all, it has a Herbrand model, so In abstract model theory (Chang & Keisler, 2012), the se- it’s sufficient for a logic programming system to restrict its mantics of a logic is defined in terms of a satisfaction rela- attention to Herbrand models. tion: As we shall see, logic programming semantics are defined in terms of minimal Herbrand models: models of which 𝑀𝑀 ⊨ 𝑆𝑆 no subset is also a model: stating that the mathematical object 4 𝑀𝑀 satisfies, or is a minimal(𝑇𝑇) = {𝑀𝑀 ⊨ 𝑇𝑇 | ∄𝑀𝑀′ ⊂ 𝑀𝑀 . 𝑀𝑀′ ⊨ 𝑇𝑇 } model of, 𝑆𝑆. To be a valid satisfaction relation, ⊨ must obey some obvious compositionality requirements, such as 𝑀𝑀 be- Minimal Herbrand models are a kind of approximation to ing a model of 𝐴𝐴 ∧ 𝐵𝐵 iff it’s a model of both 𝐴𝐴 and 𝐵𝐵, as well entailment. If a theory only has one minimal Herbrand as the requirements that it is closed on the left under isomor- model, then that model’s atoms must be true in all models. phism (an object isomorphic to a model of 𝑆𝑆 is itself a model That model is then exactly the set of atoms entailed by the of 𝑆𝑆) and on the right by variable renaming (the models of 𝑆𝑆 theory. don’t depend on our choice of variable names). If a theory has multiple minimal models, then the set of If we fix a particular domain 𝐷𝐷 of objects we want to de- atoms entailed by the theory (if any), don’t form a model by scribe, then we can define an extensional meaning for 𝑺𝑺 as themselves. Moreover, at least one atom in each minimal the set of its models: model isn’t an entailment. However, those models do still represent the atoms common to different clusters of models. modelsD (𝑆𝑆) = { 𝑀𝑀 ∈ 𝐷𝐷 | 𝑀𝑀 ⊨ 𝑆𝑆 } So there’s a sense in which they loosely characterize the set of models. The models of a theory are simply the intersection of the models of its sentences. Minimality, transitive closure, and FOL A sentence or theory is satisfiable if it has a model, i.e. if Minimality comes up repeatedly in logic and computation. at least one object satisfies it. In the logics we’re concerned The difference between the primitive recursive functions with, a contradiction can be proven from a theory iff it is and the general recursive functions is the addition of a min- unsatisfiable. imization operator. The 𝑌𝑌 combinator of the 𝜆𝜆-calculus doesn’t compute an arbitrary fixed-point of the function, it Entailment, inference, and proof computes the least fixed-point: the one that assigns output Model theory was originally developed as a way of validat- values to as few inputs values as possible. Inductively de- ing different proof systems for a given logic. A sentence is fined sets are the least fixed-points of whatever process is (semantically) entailed by a theory iff it is true in all models being iterated to generate them. of the theory, i.e. the models of the theory are a subset of the One place where minimality frequently comes up is with models of the entailed sentence. A sentence is syntactically transitive closure. If 𝑅𝑅 is a relation (a set of pairs), then its entailed from a theory within a proof system iff it is provable transitive closure 𝑅𝑅 ∗ is the smallest relation that contains 𝑅𝑅 from the theory in that system. The proof system is sound and is transitive. If we adopt the standard recursive formal- ization of transitive closure: 4 Specifically, a kind of object called a structure, which is a set equipped whether a specific theory does or does not include the natural numbers as a with some operations and relations that can be performed on it. For exam- model, and what other kinds of systems might also be models of it. ple, the natural numbers under arithmetic is a structure and one can ask Semantics of Prolog-like languages ∀𝑥𝑥, 𝑦𝑦. 𝑅𝑅(𝑥𝑥, 𝑦𝑦) → 𝑅𝑅 ∗ (𝑥𝑥, 𝑦𝑦) ∀𝑥𝑥, 𝑦𝑦, 𝑧𝑧. 𝑅𝑅∗ (𝑥𝑥, 𝑦𝑦) ∧ 𝑅𝑅 ∗ (𝑦𝑦, 𝑧𝑧) → 𝑅𝑅∗ (𝑥𝑥, 𝑧𝑧) Although logic programming languages aren’t logics per se, their semantics are typically defined by pretending that the Then this says only that 𝑅𝑅 ∗ must be transitive and contain 𝑅𝑅, statements of a logic program 𝑃𝑃 are really a theory 𝒯𝒯(𝑃𝑃) in not that 𝑅𝑅 ∗ must be minimal. The model in which 𝑅𝑅 is empty some underlying logic, most commonly FOL or classical but 𝑅𝑅 ∗ is all possible pairs, is a valid model of these axioms. propositional logic, and then defining the meaning of the It’s only in the minimal Herbrand model that 𝑅𝑅 ∗ is the true program in terms of the minimal Herbrand models of 𝒯𝒯(𝑃𝑃). transitive closure of 𝑅𝑅. This brings up the deeply inconvenient fact that first-or- Positive logic programs der logic is not strong enough to formalize transitive closure, A propositional positive logic program is a set of rules of despite the latter’s apparent simplicity. While the formali- the form: zation includes the desired model, it also includes a number of unintended models, even though its entailments are only 𝐶𝐶 ← 𝑃𝑃1 , … , 𝑃𝑃𝑛𝑛 the true statements about the transitive closure. FOL is not expressive enough to rule out the unintended models. Where the conclusion, 𝐶𝐶, and the premises, 𝑃𝑃𝑖𝑖 , are proposi- As a result, there has been a great deal of work in finite- tions. 5 Note that we are not allowing negation on either side model theory on the expressiveness of so-called intermedi- of the arrow. ate logics that add to FOL some operation, such as transitive Consider the following two inference algorithms: closure or a fixed-point operator (Libkin, 2004). The result- ing logic is more expressive than FOL without making it full Backward chaining: second-order logic, which doesn’t even have a proof system. 𝐶𝐶 is true if there is some rule 𝐶𝐶 ← 𝑃𝑃1 , … 𝑃𝑃𝑛𝑛 for which all 𝑃𝑃𝑖𝑖 are true. (Note: 𝑛𝑛 may be zero in which case 𝐶𝐶 is trivi- Monotonicity ally true). First-order logic is monotonic: since the models of a theory are the intersection of the models of its sentences, adding a Forward chaining: sentence to the theory can never add models, only remove 𝑆𝑆 = {} them. And since the entailments of a theory are the sen- repeat to convergence: tences true of all its models, adding sentences to the theory 𝑆𝑆 = 𝑆𝑆 ∪ {𝐶𝐶 | 𝐶𝐶 ← 𝑃𝑃1 , … 𝑃𝑃𝑛𝑛 is a rule and all 𝑃𝑃𝑖𝑖 ∈ 𝑆𝑆} can never remove entailments. Monotonicity is a useful property. If you are trying to The former takes one proposition and recursively applies debug your formalization of a domain and something that rules to attempt to prove it. The latter finds all provable should be a model isn’t, there will be guaranteed to be at propositions by starting with the empty set and iteratively least one sentence in the theory of which your desired model adding all propositions provable from the rules and the pre- isn’t a model. That gives you a place to start debugging. viously proven propositions, until there is no change. Unfortunately, monotonicity doesn’t match certain kinds Both these algorithms find propositions that can be con- of real-world human reasoning, such as reasoning about de- cluded from premises. That said, a rule in this style of logic faults. If I tell you Bill is sitting down to dinner, you will program has a directionality to it and so is not a clause in the draw one set of conclusions and imagine one set of situa- logical sense. In classical logic, 𝐴𝐴 → 𝐵𝐵 not only allows you tions. But if I add that Bill is a vampire, you will suddenly to infer 𝐵𝐵 from 𝐴𝐴, but also to infer ¬𝐴𝐴 from ¬𝐵𝐵. In Prolog imagine a very different set of circumstances. (Warren et al., 1977) and Planner (Hewitt, 1969), 𝐵𝐵 ← 𝐴𝐴 While the set of models of a theory is monotonic as one only allows you to infer 𝐵𝐵 from 𝐴𝐴. adds sentences to the theory, the set of minimal models is Minimal model semantics not. The theory 𝐴𝐴 → 𝐵𝐵 has the models {}, {𝐵𝐵}, and {𝐴𝐴, 𝐵𝐵}, Nonetheless, if we pretend the rules of a program 𝑃𝑃 are Horn which have the single minimal model {}. However, if we clauses, then we can compare 𝑃𝑃’s behavior to the models of add the sentence 𝐴𝐴 to the theory, then the models narrow to 𝒯𝒯(𝑃𝑃). Here, 𝒯𝒯(𝑃𝑃) is simply the theory we get when we re- just {𝐴𝐴, 𝐵𝐵} and that is now minimal. write all the rules 𝐶𝐶 ← 𝑃𝑃1 , … , 𝑃𝑃𝑛𝑛 into Horn clauses 𝑃𝑃1 ∧ … ∧ 𝑃𝑃𝑛𝑛 → 𝐶𝐶. One could imagine the directionality of logic program- ming rules leading the system to miss propositions that are 5 The exposition is simpler in the propositional case. For the first-order case, we think of each rule with variables as being universally quantified and as standing in for the set of all its possible ground instantiations. entailed by 𝒯𝒯(𝑃𝑃). However, Van Emden and Kowalski certainly an improvement over disallowing negation en- (1976) showed that for positive logic programs, 𝒯𝒯(𝑃𝑃) has a tirely. But it departs at unexpected times from classical unique, minimal model. This model: logic, leading to erroneous results. Some of these issues have to do with cases where the al- • consists of exactly the set of atoms entailed by the gorithm recurses infinitely. In these cases, it fails to give the theory right answer, but it at least also fails to give a wrong answer. • is identical to the set 𝑆𝑆 computed by the forward- However, negation as failure also leads to a class of bugs chaining algorithm, and in which one forgets that not provably true is different from • is also identical to the set of propositions provable provably false. A more subtle set of issues come up when by the backward-chaining algorithm the implementation of negation interacts unpredictably with the incremental variable binding performed in classical This minimal model was then taken by logic programming logic programming. For example, if we consider the single- researchers to define the semantics of positive logic pro- line Prolog program that asserts the truth of 𝑝𝑝(𝑎𝑎) without grams. From that point on, semantics for logic program- asserting anything else: ming languages have been based on some notion of canoni- cal or preferred models (Lifschitz, 2008a). p(a). General logic programs Then the results we get the following results for positive A general logic program is simply a logic program that al- queries match their naïve glosses in first-order logic: lows negations in the premises of rules, e.g.: Query Naïve FOL FOL Prolog 𝐶𝐶 ← 𝑃𝑃1 , … 𝑃𝑃𝑛𝑛 , ¬𝑄𝑄1 , … , ¬𝑄𝑄𝑚𝑚 p(a) 𝑃𝑃(𝑎𝑎) T T p(b) 𝑃𝑃(𝑏𝑏) F F where 𝑛𝑛 and/or 𝑚𝑚 might be zero, i.e. the 𝑃𝑃s or 𝑄𝑄s might be p(X) ∃𝑥𝑥. 𝑃𝑃(𝑥𝑥) T T absent. Unfortunately, the clausal form of such a rule is no longer a Horn clause when 𝑚𝑚 > 0. When interpreted as a However, negation can diverge from FOL: theory in classical logic, it no longer has a single minimal Herbrand model. For example, the general logic program: Query Naïve FOL FOL Prlg not p(a) ¬𝑃𝑃(𝑎𝑎) F F 𝐴𝐴 ← ¬𝐵𝐵 not p(b) ¬𝑃𝑃(𝑏𝑏) T T 𝐵𝐵 ← ¬𝐴𝐴 X=b, not p(X) ∃𝑥𝑥. 𝑥𝑥 = 𝑏𝑏 ∧ ¬𝑃𝑃(𝑥𝑥) T T not p(X), X=b ∃𝒙𝒙. ¬𝑷𝑷(𝒙𝒙) ∧ 𝒙𝒙 = 𝒃𝒃 T F when interpreted as a theory in classical logic, has the mod- p(X), X=b ∃𝑥𝑥. 𝑃𝑃(𝑥𝑥) ∧ 𝑥𝑥 = 𝑏𝑏 F F els {𝐴𝐴} and {𝐵𝐵}. However, their intersection, {}, is not a not not p(X), ∃𝒙𝒙. ¬¬𝑷𝑷(𝒙𝒙) ∧ 𝒙𝒙 F T model. Both models are minimal, and there is no single min- X=b = 𝒃𝒃 imal model to take as the meaning of the program. Indeed, while the theory entails the sentence 𝐴𝐴 ∨ 𝐵𝐵, it entails no in- Hence, in Prolog, conjunction is not commutative, nor is ne- dividual literals. gation is its own inverse. Worse, the only way to predict If one were interested in satisfaction, that is, just asking when Prolog code will diverge from the naïve logical inter- what all the different models of the program might be, then pretation is to mentally simulate it. Writing Prolog code this wouldn’t be a problem; we would simply take the mean- thus requires not only comfort with logic, but an understand- ing of the program to be the same as the meaning of the the- ing of the detailed behavior of Prolog interpreters. ory: all the models. Indeed, this is the view I will suggest These problems led to the search for a version of logic below is more appropriate for PCG. However, logic pro- programming in which negation by failure was better be- gramming has generally focused on trying to model infer- haved, eventually resulting in stable-model semantics, an- ence/entailment, and so throwing one’s hands up and ac- swer-set programming and answer-set Prolog. These sys- cepting all the models is less attractive. tems involve transforming a logic program into a SAT prob- Negation as failure lem under classical propositional logic, solving for its mod- Negation is very useful. It’s difficult to express many do- els, and filtering them to find the stable models. They have mains without it. Classical logic programming systems, the advantage that there is a natural definition of stable mod- which were implemented using backward chaining, imple- els, and hence their semantics, independent of the inference mented negations of the form ¬𝑋𝑋 by exhaustively trying to algorithm used to solve for them. However, stable model prove 𝑋𝑋, taking ¬𝑋𝑋 to be proven if the attempt fails. This is semantics is subtle and difficult. Like SLDNF, it’s close to classical FOL, but different enough for bugs to come up AnsProlog includes a number of syntactic extensions to when the programmer fails to anticipate ASP’s divergence general logic programs (Gebser et al., 2012) that are espe- from their logical intuitions. So even though it does not re- cially well suited to PCG applications. In particular, choice quire an understanding of the solver algorithm, it’s still dif- rules and pseudo-Boolean constraints (e.g. cardinality con- ficult to master. straints) come up frequently in PCG applications. Since ASP reduces programs to SAT problems plus some post-processing, 6 it can leverage the considerable algorith- Stable model semantics mic improvements and performance engineering that has The semantics of ASP are defined in terms of a particular gone into the development of SAT solvers in the last 30 kind of minimal Herbrand model called a stable model. years. This allows ASP solvers to be surprisingly fast and Lifschitz (2008a) discusses 12 different definitions of stable effective in many cases. models that all turn out to be equivalent. However, most of Because it looks for minimal models (stable ones, in par- them require enough background in other non-monotonic ticular), it’s expressive enough to represent transitive clo- logics that they can’t be fully defined within the paper. sure. More generally, it can reason about reachability, The definition that is presented in its entirety in that paper, which traditional SMT solvers cannot easily do. You can and the one that appears most often in the literature, uses the think of stable models as representing the results of a kind notion of the “reduct” of a general logic program. The re- of reasoning process in which atoms only appear in the duct ℛ(𝑃𝑃, 𝑀𝑀) of a program 𝑃𝑃 with respect to a Herbrand model if there is some chain of reasoning that would derive model 𝑀𝑀, is the positive logic program one obtains by par- that model from the rules, starting with the assumption of tially evaluating all negations in 𝑃𝑃 with their valuations in everything being false, and then incrementally adding new 𝑀𝑀. That is, we replace ¬𝑃𝑃 with false if 𝑃𝑃 ∈ 𝑀𝑀, and true if atoms as rules allow them to be inferred. 𝑃𝑃 ∉ 𝑀𝑀. For those cases where ¬𝑃𝑃 is true, this effectively Moreover, the reasoning rules in ASP programs are not as removes ¬𝑃𝑃 from the rule. In those cases where it’s false, “one-way” as they are in Prolog. If you say 𝐴𝐴 ← 𝐵𝐵 and ¬𝐴𝐴, it effectively removes the rule entirely since it contains a the system will know that 𝐵𝐵 must also be false. ASP pro- false premise. The reduct has no negations, and so is a pos- grams do constraint satisfaction, albeit a particular kind. itive logic program, and so has a unique minimal Herbrand Finally, the non-monotonicity of ASP programs makes model. them natural for certain kinds of default reasoning problems. A model 𝑀𝑀 is a stable model of a program 𝑃𝑃 is if it’s a Since the system always defaults the value of an atom to model of 𝑃𝑃 and also the minimal model of its reduct of P: false unless it has a rule to justify it, other kinds of default rules can be naturally encoded into ASP rules. stable𝑃𝑃 (𝑃𝑃) = �𝑀𝑀 ⊨ 𝒯𝒯(𝑀𝑀) | 𝑀𝑀 ∈ minimal(𝒯𝒯�ℛ(𝑃𝑃, 𝑀𝑀)�) � The availability of a high-level modeling language that is automatically expanded into a grounded form is also a very Note that since a positive logic program is its own reduct, valuable aspect of ASP, although not unique to ASP, see for the unique minimal model of a positive program is also its example, (Torlak & Bodik, 2013). In what follows, I as- unique stable model. Thus stable model semantics is “back- sume the use of a high-level modeling language and critique ward compatible” with the Van Emden and Kowalski se- merely the use of stable-model semantics. mantics, but extends it to general logic programs with nega- tion as failure. The bad Like Prolog, negation in ASP has strange, unanticipated The good properties. In classical logic, the statements: Stable model semantics gives ASP most of the attractive properties of Prolog, while avoiding the worst excesses of 𝑝𝑝 negation as failure. Although limited to finite-domain prob- ¬¬𝑝𝑝 lems where the system can enumerate the possible values of false ← ¬𝑝𝑝 a variable in advance, it gives a very convenient language for expressing SAT-like problems. It can be thought of as a Are all equivalent. In ASP, the first states that 𝑝𝑝 must be general mechanism for eager reduction of NBSAT problems true, and moreover, that that fact can be used to prove other to SAT problems. atoms. The second is not valid ASP code. And the last of these effectively means only that 𝑝𝑝 must not be provably 6 A SAT solver by itself, will find models, but not necessarily stable ones. the problem and backtracks. It can’t add all possible loop-formulae in ad- ASP solvers work reducing the program to a particular SAT problem, but vance because they can be large and there can be an exponential number of then also test whether the generated model would require circular reasoning them. In practice, this process works surprisingly well. to prove (Lin & Zhao, 2002). If so, it adds a so-called “loop formula” to false. It’s effectively true, but you can’t use its truth to make the programmer is unaware. Those atoms are absent from further inferences; you simply filter out any otherwise stable the source code, present in the stable models, but may also models in which it’s false. Both the first and last of these be absent from the output, making it difficult for novice pro- forms get used in practice. grammers to understand the behavior of the system. Finally, the nonmonotonicity of ASP is a two-edged sword. If you are trying to understand why it is that some- thing isn’t a model of your formalization in a monotonic Why do people find ASP so confusing? logic, 7 then at least one statement in your formalization must Stable-model semantics is a brilliant way of selectively in- contradict that model. You can find that statement and use corporating minimization into model finding in SAT-like that to understand what’s wrong with your formalization. systems. It makes it possible to capture entailment-like in- You can’t do that when reasoning about stable models, be- ference processes within a satisfaction-based framework, cause the statements interact with one another in non-local and selectively loosen some of those requirements using ways. Divide and conquer does not automatically work for choice rules. debugging. That said, ASP terminology and tutorials mix satisfaction terminology (models, satisfiability, unsatisfiability) with en- The ugly tailment/inference terminology (defaults, rules, proof). This definition given above for stable models is concise, Since it looks kind of like FOL, it behaves kind of like FOL precise, and almost entirely useless for the practicing pro- satisfiability, and also behaves kind of like FOL inference, grammer. For one thing, it’s difficult for a programmer to it’s easy to slip into thinking of it as actually being one or read that definition and envision what models will be stable the other. But it’s actually neither; it’s something in be- for a given set of clauses. tween. That leads to confusion and bugs. Perhaps more importantly, it defines stable models only for programs written in the form of implications of conjunc- tions. Virtually no ASP programs written in the game AI ASP for Procedural Content Generation world look like that. Rather, they frequently use constructs SAT-based logic programming provides a convenient and such as choice rules and pseudo-Boolean constraints: 8 highly expressive language for expressing finite-domain constraint satisfaction problems. It allows the kind of first- 1 { 𝑎𝑎; 𝑏𝑏; 𝑐𝑐 } 1 ← 0 {𝑐𝑐 ; 𝑑𝑑 ; 𝑒𝑒} 1 order declarative programming familiar from Prolog, with- out some of its misfeatures. ASP is one particular approach that are macro-expanded by the system into sets of rules in that uses stable model semantics, which permits the expres- the canonical form. The expansion of the rule above is too sion of concepts such as reachability and transitive closure complex to include here, but for a simpler example, the at the cost of a steeper learning curve and a more complex choice rule: 9 debugging task. There are a number of PCG problems for which ASP is { 𝑎𝑎; 𝑏𝑏; 𝑐𝑐 } not only appropriate, but for which it’s hard to imagine and alternative. Problems that require sophisticated reasoning expands into the rules: about reachability and provability, such as game generation (Summerville et al., 2018) or generation of levels that force 𝑎𝑎 ← ¬𝑎𝑎� particular solution methods (Polozov et al., 2015) simply 𝑎𝑎� ← ¬𝑎𝑎 cannot be solved by standard SAT techniques. 𝑏𝑏 ← ¬𝑏𝑏� Nevertheless, there are many PCG applications, such as 𝑏𝑏� ← ¬𝑏𝑏 the one discussed at the beginning of this paper, where some 𝑐𝑐 ← ¬𝑐𝑐̅ kind of constraint formalism is valuable, but ASP’s minimi- 𝑐𝑐̅ ← ¬𝑐𝑐 zation features are unnecessary. In those cases, I would ar- gue that ASP’s nonmonotonic semantics lead to unneces- It is the stable models of this program that form the seman- sary confusion, and a more conventional SAT or SMT tics of the original. Note that these rules expand not only solver 10 would be more appropriate. CatSAT (Horswill, into multiple new rules, but also into new atoms of which 7 For example, when one uses a higher-level modeling language such as 9 This says that the truth values of 𝑎𝑎, 𝑏𝑏, and 𝑐𝑐 may be chosen freely, modulo Rosette (Torlak & Bodik, 2013) to generate a SAT or SMT problem. any constraints put on them by other rules. 8 For those unfamiliar with ASP, this says that if no more than one of the 10 Satisfaction Modulo Theories. An SMT solver is essentially a SAT propositions 𝑐𝑐, 𝑑𝑑, and 𝑒𝑒 are true, then exactly one of 𝑎𝑎, 𝑏𝑏, and 𝑐𝑐 should be solver that coroutines with a domain-specific constraint solver for some true. specialized data type, such as integers, arrays, or bit vectors. 2018a) is an example of such a system that has been de- capabilities might be better served by more conventional ployed in a commercial game (SomaSim, 2021). satisfiability solvers with more predictable semantics. Nevertheless, ASP clearly demonstrates the power of in- corporating some form of minimization into a satisfiability Alternatives and future work solver. This suggests future work on incorporating such For many problems, what I wish I had was neither traditional minimization in a more targeted and predictable manner into SAT nor ASP, but rather something that provided the kinds conventional satisfiability solvers. of minimization supported by ASP in a more selective and controlled manner. There are at least two possible strategies Acknowledgements for doing this. One would be to implement a satisfiability solver for one I would like to thank Rob Zubek and the reviewers for their of the intermediate logics studied in finite model theory comments on the original draft of this paper. I would par- (Libkin, 2004). FO(TC), a version of first-order logic in ticularly like to thank Reviewer 3 for their reference to Bay- which specific predicates can be declared to be the transitive less’ work, which is very much in line with what I was hop- closure of other predicates, would be an obvious choice. ing someone would do. I would also like to thank Adam This could potentially be implemented in the same style as Smith and Adam Summerville for their discussions with me traditional ASP solvers: the system could find a model, then over the years about the pleasures and perils of ASP. test just the transitive closures for minimality, and add addi- tional clauses at runtime to defeat the particular violations of minimality that came up in that particular model. These References would be the equivalents of the loop formulae generated by Abelson, H., Sussman, G. J., & Sussman, J. (1996). Structure and traditional ASP solvers. I could easily imagine that failing interpretation of computer programs (2nd ed.). MIT Press. miserably, that the system would need to generate too many Adams, T., & Adams, Z. (2006). Slaves to Armok: God of Blood such clauses to be practical. But I would have predicted that Chapter II: Dwarf Fortress. Bay 12 Games. to be true of loop formulae in ASP, and that works well. Alspach, T. (2009). One Night Ultimate Werewolf. Bézier Games. Another possibility would be to use an SMT solver that Bayless, S. (2017). SAT Modulo Monotonic Theories. University incorporated a theory solver for connectivity reasoning in of British Columbia. directed graphs (Bayless, 2017; Rossi et al., 2006, chapter Chang, C. C., & Keisler, J. (2012). Model Theory (Third edit). 17). While connectivity of a graph isn’t expressible in first- Dover. order logic, 11 it can be tested in linear time and random con- Clocksin, W. F., & Mellish, C. S. (2003). Programming in Prolog: nected graphs can be constructed in near-linear time. Bay- Using the ISO Standard (5th ed.). Springer. less (2017) used SAT module monotonic theories 12 with Cormen, T. H., Leiserson, C. E., & L., R. R. (1990). Introduction to Algorithms. MIT Press. graph intervals to efficiently acyclicity constraints as well as pairwise reachability, shortest path, and maximum flow Evans, R. (2009). AI Challenges in Sims 3. Artificial Intelligence and Interactive Digital Entertainment. constraints. These could certainly be used in principle to Felleisen, M., Findler, R. B., Flatt, M., & Krishnamurthi, S. (2018). implement transitive closure. How to Design Programs (2nd ed.). MIT Press. Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, Conclusion T., & Thiele, S. (2010). A User ’ s Guide to gringo , clasp , clingo , and iclingo ∗. Answer-set programming is a powerful and versatile tool for Gebser, M., Kaminski, R., Kaufmann, B., & Schaub, T. (2012). constraint-based procedural content generation. However, Answer Set Solving in Practice. In Synthesis Lectures on Artificial its semantics are subtle and difficult to learn. Moreover, it Intelligence and Machine Learning. https://doi.org/10.2200/S00457ED1V01Y201211AIM019 was developed for problems very different from PCG. Gelfond, M., & Lifschitz, V. (1992). The stable model semantics While there are PCG problems for which ASP seems to be for logic programming. The Journal of Symbolic Logic, 57(1), the only viable method, PCG tasks that don’t specifically 274–277. need its minimization or non-monotonic reasoning 11 This is ultimately because first-order logic has a “compactness” property 12 Note that this is a different sense of monotonic than used above. Here that the logic of graphs does not. However, it should be said that it is pos- monotonic means that the predicate obeys some partial order such that if it sible to formalize connectivity of a graph with any fixed, finite number of is true (false) for a particular set of arguments, it is also true (false) when nodes using what amounts to an FOL encoding of the Floyd-Warshall al- those arguments are less under the partial order. gorithm (Cormen et al., 1990). However, this involves adding a cubic num- ber of clauses to the SAT problem, which is not appealing. Hewitt, C. (1969). PLANNER: A Language for Proving Theorems Van Emden, M. H., & Kowalski, R. a. (1976). The Semantics of in Robots. International Joint Conference on Artificial Intelligence Predicate Logic as a Programming Language. Journal of the ACM, (IJCAI). 23(4), 733–742. https://doi.org/10.1145/321978.321991 Horswill, I. (2018a). CatSAT: A Practical, Embedded, SAT Warren, D. H. D., Pereira, L. M., & Pereira, F. (1977). PROLOG - Language for Runtime PCG. AIIDE-18. The Language and its implementation compared with LISP. Horswill, I. (2018b). Imaginarium: A Tool for Casual Constraint- Symposium on AI and Programming Languages, 12(8), 109–115. Based PCG. Workshop on Experimental AI in Games, AIIDE 2018. https://doi.org/10.1145/800228.806939 Horswill, I. (2020). Generative Text using Classical Zubek, R., Horswill, I., Robison, E., & Viglione, M. (2021). Social Nondeterminism. Workshop on Experimental AI in Games (EXAG- Modeling via Logic Programming in City of Gangsters. Artificial 20). Intelligence and Interactive Digital Entertainment (AIIDE-21). Libkin, L. (2004). Elements of Finite Model Theory. Springer. Zubek, R., & Viglione, M. (2021). City of Gangsters. Kasedo Games. Lifschitz, V. (2019). Answer Set Programming (1st ed.). Springer. Lifschitz, V. (2008a). Twelve Definitions of a Stable Model. Proceedings of the International Conference on Logic Programming (ICLP), 37–51. Lifschitz, V. (2008b). What Is Answer Set Programming? Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI), 1594–1597. Lin, F., & Zhao, Y. (2002). ASSAT: computing answer sets of a logic program by SAT solvers. Artificial Intelligence, 112–117. Maxis. (2009). The Sims 3. Polozov, O., O’rourke, E., Smith, A. M., Zettlemoyer, L., GulWani, S., & Popović, Z. (2015). Personalized Mathematical Word Problem Generation. International Joint Conference on Artificial Intelligence (IJCAI). Rossi, F., Van Beek, P., & Walsh, T. (2006). Handbook of Constraint Programming. In F. Rossi, P. Van Beek, & T. Walsh (Eds.), Change (Vol. 35, Issue 9). Elsevier. http://books.google.com/books?hl=en&lr=&id=Kjap9Z WcKOoC&oi=fnd&pg=PR5&dq=Handbook+of+ Constraint+Programming&ots=QADjFO6ROd&sig=4 KRZ7V0HgUWTO4wS4_zEw0yaxhY Smith, A. (2011). A Map Generation Speedrun with Answer Set Programming. Expressive Intelligence Studio Blog. http://eis- blog.ucsc.edu/2011/10/map-generation-speedrun/ Smith, A. M. (2017). Answer Set Programming in Proofdoku. Proceedings of the Fourth Workshop on Experimental AI in Games (EXAG 4). Smith, A. M., & Mateas, M. (2011). Answer Set Programming for Procedural Content Generation : A Design Space Approach. IEEE Transactions on Computational Intelligence and AI in Games, 3(3), 187–200. https://doi.org/10.1109/TCIAIG.2011.2158545 Smith, A. M., & Mateas, M. (2010). Variations Forever : Flexibly Generating Rulesets from a Sculptable Design Space of Mini- Games. IEEE Conference on Computational Intelligence and Games, 273–280. https://doi.org/10.1109/ITW.2010.5593343 SomaSim. (2021). City of Gangsters. Summerville, A., Martens, C., Samuel, B., Osborn, J., & Mateas, N. W. M. (2018). Gemini : Bidirectional Generation and Analysis of Games via ASP. Proceedings of the Fourteenth Artificial Intelligence and Interactive Digital Entertainment Conference (AIIDE 2018), 1, 123–129. Torlak, E., & Bodik, R. (2013). A lightweight symbolic virtual machine for solver-aided host languages. Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’14. https://doi.org/10.1145/2594291.2594340