Automatic Synthesis of Generalized Winning Strategies of Impartial Combinatorial Games Using SMT Solvers

1 Introduction

Strategy representation and reasoning has recently received much attention in artificial intelligence, particularly, multiagent systems and game theory [Chatterjee et al., 2010; Zhang and Thielscher, 2015; Xiong and Liu, 2016]. In the area of game theory, one class of the elementary and fundamental games is impartial combinatorial games (ICGs) where two players alternate moving with perfect information [Ferguson, 2018]. Various ICGs (e.g., Nim [Bouton, 1901], Wythoff [Wythoff, 1907], Chomp [Schuh, 1952] and Empty-and-Divide [Ferguson, 1998]), and their variants and extensions [Liu and Zhao, 2015; Ahn et al., 2017] have been proposed and analyzed. The following is the 2-rowed Chomp game.

Example 1. Cookies are laid out on 2 rows each of which contains an arbitrary number of cells. The cookie in the leftmost-topmost position (1, 1) is poisoned. At each move, a player has to eat a remaining cookie, together with all cookies to the right and above it. The loser is the player who has no choice but to eat the poisoned cookie.

∗Corresponding author

One of the challenging problems of ICGs is to synthesize the winning strategy for one player. Given an instance, that is, an ICG together with an initial state, one winning strategy can be computed via the backward search algorithm [de Jonge and Zhang, 2016]. However, this strategy holds for only some instances but not (infinitely) many instances. This is illustrated in the 2-rowed Chomp game as follows. Assume that the number v1 and v2 of cookies at the first and second row are both initially 2. In the first round, the first player eats the cookie at (2, 2). If the other player eats the cookie at (1, 2) (resp. (2, 1)), then she chooses to eat the cookie at (2, 1) (resp. (1, 2)) in the next round. Following the above strategy, the first player finally wins no matter how the other player does. But for another instance where the initial state is v1 = 3 ∧ v2 = 1, it is impossible that the first player eats the cookie at (2, 2) since no cookie is at such position. It has been proved that the first player can force to win in all instances where v1 ̸= v2 + 1 initially [Zeilberger, 2001]. Hence, the above strategy does not work for some of these instances.

Synthesizing a generalized winning strategy that works for possibly infinitely many instances is of utmost importance. However, this problem is notoriously difficult even for simple games, and undecidable in general [Luo and Liu, 2019].

In this paper, we concentrate on ICGs, and investigate synthesizing generalized winning strategies. The contributions of this paper are as follows: (1) We propose a logical framework to formalize ICGs via the linear integer arithmetic fragment of Planning Domain Definition Language (PDDL) [Fox and Long, 2003]. (2) We propose an approach to synthesizing the arithmetic formula, called the winning formula, which exactly captures the states in which the player forces to win. To do this, we propose three constraints for the winning formula, then the synthesis of the winning formula is reduced to searching an arithmetic formula that is consistent with these constraints. We implement the searching process via adapting the enumerative approach proposed in [Udupa et al., 2013]. (3) We give a method to synthesize generalized winning strategies for impartial combinatorial games. To this end, we divide the winning formula into several arithmetic formulas through a series of syntactic operations. For each formula, we then choose a suitable action together with its parameters via the enumerative approach. (4) Finally, we evaluate our approach on several games, and experimental results demonstrate the effectiveness of the proposed approach.

2 Impartial Combinatorial Games

In this section, we briefly introduce impartial combinatorial games (ICGs). A game that satisfies the following conditions is called an ICG [Ferguson, 2018]: (1) There are two players and many states such that the player can move from one state to another one. (2) Two players alternate moving and have the same choice of moving. (3) The game ends when it moves to an ending state in which no player has a possible move. (4) The game always ends in a finite number of moves, and the last player to move wins. An instance of an ICG is the ICG together with an initial state. In general, an ICG may contain infinite states, and hence it may have infinite instances.

Each instance of an ICG is a finite two-player game with perfect information and no-chance move where the players take turns moving. In addition, this game does not end in a draw. By Zermelo's Theorem [Zermelo, 1913], there always exists a winning strategy for one player in an ICG.

It can be easily observed that the player cannot guarantee to win in all states. To distinguish states in which the player can forces to win from those in which she cannot, we classify states into two types: winning and losing states.

Definition 1 ([Ferguson, 2018]). In an ICG, winning and losing states are recursively defined as follows:

1. All ending states are losing states.
2. All states such that there is at least one move to a losing state are winning states.
3. All states such that the only possible moves are to winning states are losing states.

We hereafter introduce the concept of strategy. ICGs are a special case of Gale-Stewart games, and so are determined by memoryless strategies [Gale and Stewart, 1953]. In addition, it is impossible to obtain a winning strategy for the player in a losing state, there is no need to consider how to choose a move in this case. We hence define a strategy as a function from winning states to moves.

3 A Logical Framework

In this section, we present a logical framework for describing ICGs. The framework we adopt is a slight modification of the linear integer arithmetic fragment of the PDDL 2.1 language defined in [Fox and Long, 2003].

Traditionally, arithmetic formulas allow the occurrence of multiplication. In this paper, we use the decidable fragment: linear integer arithmetic (LIA). An arithmetic formula is LIA-definable if it is defined by LIA. The syntax of LIA is defined as follows. Let N be the set of integers, V a set of variables and X ⊆ V a finite set of state variables. The sets of arithmetic expressions (Exp), literals (Lit) and formulas (Form) is defined by the following grammar:

where c, c′ ∈ N and v ∈ V.

We remark that formulas defined by the above syntax are negation-free. For the sake of simplification, when we use the negation symbol ¬φ, we refer to the negation-free formula equivalent to ¬φ, obtained in the obvious way. The literal e ≡c′ c denotes that e - c are divisible by c′ , and its negation is e ̸≡c c′ . We use |φ| (resp. |e|) for the size of an arithmetic formula φ (resp. an arithmetic expression e). It is well-known that LIA admits quantifier elimination, i.e., any arithmetic formula can be equivalently transformed into a quantifier-free one [Cooper, 1972; Monniaux, 2010]. We use Form qf for the set of quantifier-free formulas (qf-formulas). We use ExpX for the set of expressions over X, and say e is semi-ground if e ∈ ExpX . We use FormX for the set of formulas of which free variables are state variables, and say φ is semi-ground if φ ∈ FormX . The notation Form qf X is similar. We say an arithmetic formula is an arithmetic term, if it is a conjunction of arithmetic literals.

A state s is a valuation function X → N. Given a state s, we evaluate a semi-ground expression e into an integer e(s) to which the expression simplifies when substituting every state variable v with their respective value s(v). The Boolean value φ(s) of a semi-ground formula φ can be determined in a similar way. We say a state s satisfies a formula φ, denoted by s |= φ, if φ(s) = ⊤. We say a formula φ entails another one φ′ , denoted by φ |= φ′ , if for all states s s.t. s |= φ, we have s |= φ′ . A numeric effect is a triple 〈φ, v, e〉 where φ ∈ Form, v ∈ X, and e ∈ Exp. Intuitively, it means that if φ holds in a state s, then the value of v becomes e(s) after performing the action; otherwise, it remains unchanged.

Definition 2. An ICG is defined as a tuple Π = 〈X , A, C, E〉 where

• X: a finite set of state variables.
• A: a finite set of actions. Each action a(Y) ∈ A can be parameterized by a vector Y of variables. An action a(Y) is defined by a tuple 〈pre, eff〉 where pre ∈ Form denotes the precondition, and eff is the effect represented by a set of numeric effects.
• C: a formula of FormX denoting all legal states.
• E: a formula of FormX denoting all ending states.

Let Σ be a vector of semi-ground expressions. A semiground action a[Y/Σ] is an action whose the i-th parameter yi of Y is replaced by the i-th semi-ground expression ei of Σ. For simplicity, we sometimes use a to denote semi-ground actions. Given a semi-ground action a, we say a is applicable over a state s, if s |= pre(a). The result of applying an applicable action a over s is a state, written do(a, s), which results from s by replacing s(v) with e(s) when s |= φ for all 〈φ, v, e〉 ∈ eff(a).

Example 2. The formalization of the 2-rowed Chomp game is given as follows. Two state variables v1 and v2 denote the number of cookies in the first and second row respectively. Any legal state is such that (1) the first row contains at least as many cookies as the second one, (2) the first row contains at least one cookie, and (3) the number of the cookies in the second row is non-negative (i.e., C = v1 ≥ v2∧v1 ≥ 1∧v2 ≥ 0). The ending condition E is v1 = 1 ∧ v2 = 0. The action eat1(k) (resp. eat2(k)) means eating the cookie at (1, k) (resp. (2, k)) together with all cookies to the right and/or above it. The following are descriptions of actions.

1. pre(eat1(k)) = v1 ≥ k ∧ k > 1; 2. pre(eat2(k)) = v2 ≥ k ∧ k > 0; 3. eff(eat1(k)) = {〈⊤, v1, k -1〉, 〈v2 ≥ k, v2, k -1〉};

1. eff(eat2(k)) = {〈⊤, v2, k -1〉}.

To obtain the finite representation of winning states, we use an arithmetic formula to exactly capture this notion, called the winning formula.

Definition 3. Let Π = 〈X,A, C, E〉 be an ICG and φ ∈ FormX . We call φ a winning formula of Π, if

1. For any ending state s, we have s |= ¬φ;
2. For any winning state s, there is an action a s.t. a is applicable in s and do(a, s) |= ¬φ;
3. For any losing state s and action a where a is applicable in s, we have do(a, s) |= φ.

For an ICG, the winning formula is unique up to equivalence as the set of winning states is unique. Since the sets of winning states and losing states are disjoint, ¬φ is the symbolic representation of losing states. Each condition illustrated in the definition of winning formulas corresponds to each rule given in the definition of winning states (cf. Definition 1). In this paper, we restrict winning formulas to be LIA-definable. The winning formulas for some games are not LIA-definable. For example, the winning formula of the Wythoff game [Wythoff, 1907] is v1 ̸= ⌊g ·n⌋∨v2 ̸= ⌊g2 ·n⌋ for any positive integer n where g is the Golden ratio 1+√5 2 and ⌊r⌋ is the integer part of the real number r. We leave the investigation of synthesizing winning formulas for these games requiring more expressive language to future work.

We hereafter define winning strategies as a set of pairs of semi-ground formulas and actions.

Definition 4. Let Π = 〈X , A, C, E〉 be an ICG, and φ a winning formula of Π. A winning strategy δ is a set of pairs {(ψ1, a1), · · · , (ψn, an)} where each ψi ∈ FormX and ai is a semi-ground action, if

1. ∨ni=1 ψi ≡ φ;
2. ψi ̸|= ψj for i ̸= j.
3. For any winning state s and a ∈ δ(s), we have do(a, s) is a losing state.

Conditions 1 and 2 together guarantee that the formulas ψi's form a cover of the winning formula φ. That is, (1) φ is covered by all of the ψi's; and (2) any formula ψi can not entail another one ψj. Condition 3 requires the successor state, resulting from a winning state by executing the action according to the strategy, be a losing state. Condition 3 together with the fact that E |= ¬φ (Item 1 of Definition 3) implies that the strategy δ defined in Definition 4 is winning.

4 Synthesis of Winning Strategies

In this section, we provide a synthesis approach to winning strategies. Our approach consists of three steps: (1) synthesizing the winning formula (Sec. 4.2), (2) refining the winning formula (Sec. 4.3), and (3) synthesizing the winning strategy (Sec. 4.4). The first and third steps are based on the enumerative algorithm proposed in [Udupa et al., 2013] (Sec. 4.1).

Algorithm 1: Synthesize(Θ) Input: Θ : (θ1, · · · , θm): a set of specifications. Output: Ω : (obj1, · · · , objn): a vector of expression and formula satisfying Θ. 1 Initialize the set E of examples 2 while true do 3 Ω← Enumerate(E) 4 sat ← true 5 (in, sat) ← Verifiy(Ω, Θ) 6 if sat = false then /* The specification is not satisfied */ 7 Compute the output (out1, · · · , outn) according to the input in 8 e ← (in, (out1, · · · , outn)) 9 E ← E ∪ e 10 else /* Ω is correct */ 11 return Ω

4.1 The enumerative algorithm for multiple objects

The task of the original enumerative algorithm is to synthesize a single object satisfying a set of specifications [Udupa et al., 2013]. The object is an expression or a formula, and each specification is expressed by an formula. In this paper, we need to consider identifying a vector of expressions and formulas. We hereafter extend the original algorithm to be suitable for multiple objects.

As Algorithm 1 illustrates, the algorithm aims to synthesize n objects Ω satisfying the specifications Θ. It maintains a set E of examples. An example e consists of an input in(e) and an output out(e). The input is a state while the output is a vector of Boolean values and/or integers with the same length of the vector of objects. The i-th element of the output is a Boolean value (resp. integer) if the i-th object is a formula (resp. expression). The main idea of this algorithm is to iteratively enumerate candidates consistent with the set E of examples, and then return the correct ones via verifying them against the set Θ of specifications.

The enumeration process generates the candidate expressions (or formulas) by induction on size according to the grammar illustrated in Section 3. In the first step, only arithmetic expressions of size 1 (i.e., state variables and integers) are considered. As the set of integers is infinite, the integers considered in the first step are 0, 1 together with the constants explicitly occurring in the formalization of games. Firstly, this restriction does not affect visiting all integers since any positive integer c can be represented by the addition of c 1's, and the negative integer -c equals to 0 - c. Furthermore, we observe that some integers occurring in the winning formula and winning strategy are close to some explicit constants of appearing in the formalization. Hence, supplementing these constants can accelerate the synthesis process. In the k-th step, we generate arithmetic expressions and formulas of size k. The enumeration process terminates when it finds candidates that are consistent with the set of examples. Formally, a vector of objects (obj1, · · · , objn) is consistent with a set E of examples, if for any 1 ≤ i ≤ n and any example e ∈ E, we have obji(in(e)) = outi(e).

To improve the efficiency of the enumeration process, we remove expressions and formulas based on the notion of indistinguishability. Formally, two formulas φ1 and φ2 are indistinguishable w.r.t. a set S of states, if φ1(s) = φ2(s) for every s ∈ S. The definition of indistinguishability between two expressions is similar. For example, suppose that S = {(v1 : 1, v2 : 2), (v1 : 2, v2 : 2)}. It is easily verified that the two formulas v1 ̸= v2 and v1 + 1 = v2 hold in the first state and does not hold in the second one. Therefore, the two formulas are indistinguishable w.r.t. S. Suppose that we are generating expressions and formulas of size k. Let I be the collection of the inputs of the set of examples e ∈ E. If φ1 and φ2 are indistinguishable w.r.t. I, then it is sufficient to carry forward only one of φ1 and φ2 to the next iteration k + 1. Based on the notion of indistinguishability, we can prune the search space of candidates.

When desired candidates are generated by the enumeration process, they will be sent to the verification process for checking against the correctness of given specifications. The verification process can be executed by an SMT solver. If the candidates are correct, then we succeed in finding the correct expressions and formulas. Otherwise, the SMT solver returns a state that distinguishes the correct expressions and formulas and the candidates generated by the enumeration process. For each state s, we construct a new example e with the state and a suitable output, and enlarge the set E of example by e. Then, the enumeration process restarts. The whole enumerative algorithm repeats until it searches correct candidates.

The enumerative algorithm is a general approach to synthesizing multiple objects. To adopt this algorithm, three factors should be designed: (1) what is the type of each object and the constraints for objects, (2) how to initialize the set E of examples (Line 1), and (3) how to compute the output for the state generated by the SMT solver (Line 7). The details will be illustrated in Sections 4.2 and 4.4.

4.2 Synthesizing the winning formula

In this subsection, we introduce the idea of synthesizing the winning formula via adopting the enumerative algorithm.

Firstly, the search object is a semi-ground qf-formula. Each ouput of all examples of E contains a single Boolean value. Secondly, the set E initially contains only examples whose inputs are ending states. The output is ⊥ as each ending state is a losing state. This can be done by finding states satisfying the ending condition E via the SMT solver. Thirdly, the Boolean value of a state s, denoting if s is a winning state is determined by a recursive way according to the definition of winning and losing states (cf. Definition 1).

In the following, we introduce the notion of transition formulas and global transition formulas that are ingredient components of the constraints. The following construction of transition formulas is a numerical generalization of the existing boolean encoding for the planning problem which focuses on transition systems over finite states [Hoffmann and Brafman, 2006; Rintanen, 2012]. For an action a, the transition formula of a reflects the relation between predecessor and successor states. In order to express these two notions, we consider two versions v and v′ for all v ∈ X. The unprimed version v denotes the state variable before performing an action, and the primed one v′ denotes the one after.

Definition 5. Let a be an action. The transition formula T (a) of a is the conjunction of the following formulas:

The first formula is the precondition of action a. The second one is the effect axiom meaning that the value of v becomes e(s) if the condition φ holds in the state s. The third formulas is the frame axiom meaning that if no condition φ s.t. 〈φ, v, e〉 ∈ eff(a) holds, then the value of v remains unchanged.

The global transition formula denotes the state transition system of the whole game. The definition is as follows:

Definition 6. Let A be a set of actions. The global transition formula T (A) of Π is ∨a(Y)∈A ∃Y[T (a(Y))].

The following example illustrates the construction of transition formulas from the definition of actions.

Example 3. Let us continue the 2-rowed Chomp game. We construct the transition formula T (eat1(k)) as follows. The precondition is v1 ≥ k ∧ k > 1. The effects contain two elements: 〈⊤, v1, k -1〉 and 〈v2 ≥ k, v2, k -1〉. Hence, Formula 2 of T (eat1(k)) is (⊤ → v′1 = k - 1) ∧ (v2 ≥ k → v′2 = k-1). We now consider Formula 3 of T (eat1(k)). For the variable v1, the formula is ⊤ ∨ v′1 = v1 as v1 only occurs in the first element of eff(eat1(k)). Similarly, we obtain the formula v2 ≥ k ∨ v′2 = v2 for the variable v2. Conjoining the above formulas and simplifying the conjunction lead to the transition formula T (eat1(k)) ≡ (v1 ≥ k ∧ k > 1) ∧ (v′1 = k-1)∧(v2 ≥ k → v′2 = k-1)∧(v2 ≥ k∨v′2 = v2). Similarly, we get that T (eat2(k)) ≡ v2 ≥ k∧k > 0∧v′2 = k - 1 ∧ v′1 = v1. By Definition 6, the global transition formula T (A) ≡ ∃k[T (eat1(k)) ∨ (T (eat2(k))].

With the global transition formula in hand, we are ready to give the constraints for the winning formula.

Definition 7. Let Π = 〈X,A, C, E〉 be an ICG. The constraints for the winning formula φ of Π are as follows:

where φ[X/X ′ ] is the formula obtained by replacing every occurrence of v ∈ X in φ with v′ .

The three constraints correspond to Items 1 - 3 of Definition 3 respectively. When the enumeration process generates a candidate φ, we check if the constraint is valid via the SMT solver. If it is the case, then φ is the winning formula. Otherwise, the SMT solver returns a state s that can be used to construct a new example e. However, the state s may be not suitable to improve the candidate φ. Suppose that s is a winning state and s |= φ. The example e we construct is (s,⊤). In this case, even if we add this example into E, the new candidate may be equivalent to the previous one. This phenomenon may also happen when s is a losing state and s |= ¬φ. To repair this defect, we enumerate states in an increasing order of the sum of values of all state variables until we find a state s matches the two requirements: (1) the state s is not the input of an existing example (i.e., s ̸= in(e) for all e ∈ E); (2) s is a winning state and s |= ¬φ, or s is a losing state and s |= φ. Finally, we add the example (s, (out)), where out denotes if s is a winning state, into E, and the enumeration process restarts.

We show the working of the process of synthesizing the winning formula on the 2-rowed Chomp game.

Example 4. Table 1 shows the candidates constructed by the enumeration process and the corresponding examples obtained from the verification process. Initially, the set E contains an example ((v1 : 1, v2 : 0), (⊥)). The enumeration process constructs a candidate v1 ̸= v1, and sends it to the verification process. The latter finds that v1 ̸= v1 is not the winning formula, and enlarges the set E by ((v1 : 1, v2 : 1), (⊤)). The enumeration process then submits the formulas v2 ̸= 0 and v1 = v2 to the verification process. The SMT solver returns a losing state (v1 : 2, v2 : 1) and a winning state (v1 : 2, v2 : 2), respectively, as counterexamples to the above two formulas. Since the winning state (v1 : 2, v2 : 2) satisfies the formula v1 = v2, it is a state that is not suitable to construct an example. At this iteration, we generate a winning state (v1 : 3, v2 : 1) that falsifies the candidate v1 = v2. Finally, the enumeration process succeeds in finding the winning formula v1 ̸= v2 +1 which is certified by the verification process, and the whole algorithm terminates.

Next, we state two important properties of the enumerative algorithm to synthesize the winning formula.

Soundness If Algorithm 1 synthesizes the formula φ satisfying the constraints illustrated in Definition 7, then φ is the winning formula of Π.

Relatively Completeness If the winning formula of Π is LIA-definable, then Algorithm 1 terminates with a winning formula.

Proof. Soundness Suppose that φ is the formula that Algorithm 1 returns. It satisfies the constraints illustrated in Definition 7. It follows that φ satisfies the requirements illustrated in the definition of winning formulas.

Completeness Suppose that φ is the winning formula of Π with the smallest size. According to Algorithm 1, the enumeration process generates the formula φ, and the verification process guarantees the correctness of φ according to the constraints illustrated in Definition 7.

Although our synthesis algorithm of winning formulas is sound and relatively complete on LIA, this algorithm is non-terminating and incomplete. This is because some linear ICGs (i.e., ICGs formalized in LIA) have no LIA-definable winning formula, e.g., the Wythoff game.

4.3 Refining the winning formula

Although we obtain the winning formula from the above step, it is not sufficient to synthesize winning strategies. We illustrate this with the following example. The winning formula for the 2-rowed Chomp game is v1 ̸= v2+1. For the first case v1 < v2 + 1, the player should perform the action eat2(v1) so as to reach a losing state. For the other case v1 > v2 + 1, she should execute eat1(v2 + 2). It can be observed that the player chooses two different actions eat1 and eat2 in different cases. Therefore, the winning formula should be divided into a set of formulas satisfying the meticulous condition.

Definition 8. Let Π = 〈X,A, C, E〉 be an ICG. Let φ be the winning formula of Π, and ψ a formula entailing φ. The formula ψ is meticulous, if there is a semi-ground action a[Y/Σ] s.t. the following condition holds

Intuitively, the above formula says that a[Y/Σ] is applicable over every legal state s satisfying ψ, and performing a[Y/Σ] from these states satisfying ψ leads to a losing state.

We say a cover Ψ of the winning formula is meticulous, if every formula ψ ∈ Ψ is meticulous.

We hereafter present a syntactic method to refine the cover of the winning formula φ facilitating synthesis of winning strategies. The method involves two syntactic operations. We first obtain an equivalent formula φ′ by replacing in φ every occurrence of numeric literals of the form e1 ̸= e2, e1 ≤ e2, e1 ≥ e2 and e1 ̸≡e3 e2 by the disjunction of arithmetic literals as follows.

We then transform φ′ into the form ∨ni=1 ψi where ψi is a arithmetic term via the distributive law and removing contradictory arithmetic terms. It can be verified that {ψ1, · · · , ψn} forms a cover of the winning formula.

We remark that this step may cause an exponential blowup in the size of the original winning formula. The experimental results in Section 5 show that the runtime of the refining step can be ignored. Another noteworthy point is that it is not guaranteed that the cover constructed by the method meet the meticulousness condition. Fortunately, our method does work on all benchmarks of games considered in this paper.

4.4 Synthesizing the winning strategy

Finally, we synthesize the winning strategy from the cover of the winning formula as follows.

Algorithm 2 gives the pseudo-code of the synthesis process. For each ψ of the cover, we need to find a semiground action a[Y/Σ] satisfying the constraint illustrated in

Algorithm 2: SynthesizeWinningStrategy(Π, Ψ) Input: Π: an description of impartial combinatorial game; Ψ: a cover of the winning formula φ of the ICG Π. Output: δ: a winning strategy for Π. 1 foreach ψ ∈ Ψ do /* Traverses each formula ψ of the cover Ψ */ 2 f ound ← f alse 3 foreach a(Y) ∈ A do /* Find a vector Σ of semi-ground expressions s.t. a[Y/Σ] is winning for ψi */ 4 θ ← C ∧ ψ → {pre(a[Y/Σ])∧ 5 ∀X ′ [T (a[Y/Σ]) → ¬φ[X /X ′ ]]} 6 (Σ, f ound) ← Synthesize({θ}) 7 if found = true then 8 δ ← δ ∪ (ψ, a[Y/Σ]) 9 break 10 return NULL

Definition 8. To do this, we will identify the vector Σ of semi-ground expressions for each action a(Y) ∈ A via the enumerative algorithm satisfying the constraints illustrated in Definition 8. Suppose that we are considering an action a(Y). If the enumerative algorithm succeeds in finding a desired vector Σ, then a[Y/Σ] is the semi-ground action that is winning for ψ. Initially, the set E of examples is empty. Finally, the output of a state s is constructed as follows. The output is a vector I of integers such that the formula ∀X{Form(s) → [pre(a[Y/I]) ∧ ∀X ′ [T (a[Y/I]) → φ[X/X ′ ]]]} is valid. The subformula Form(s) = ∧v∈X [v = s(v)] is a formula representing the state s. Intuitively, the above formula means that in the state s, the ground action a(Y/I) is applicable and executing it results in a losing state. The vector I can be computed via a SMT solver. To let the enumerative algorithm to be terminating, we restrict the maximal size of expressions to be m. If no such expression satisfies the constraints, then we consider that the action a is not appropriate, and continue to choose another action. If we succeeds in finding the semi-ground action a[Y/Σ] that is winning for ψ, we continue to handle another formula of the cover. If no action is suitable for the formula ψ, then we consider that ψ is not meticulous, and terminate the synthesis process.

Similarly to the step of synthesizing the winning formula, we obtain the soundness and completeness theorem for synthesizing the winning strategy.

Theorem 2. Let Π = 〈X,A, C, E〉 be an ICG. Let φ be the winning formula of Π, Ψ the cover of φ, and m the maximal size of expressions generated in the enumeration process.

Soundness If Algorithm 2 synthesizes the strategy δ, then δ is the winning strategy of Π.

Bounded Completeness Suppose that for each ψi ∈ Ψ, there is a semi-ground action ai[Yi/Σi] s.t. each expression of Σi is of at most size m and {(ψ1, a1[Y1/Σ1]), · · · , (ψn, an[Yn/Σn])} is the winning strategy of Π. Then, Algorithm 2 terminates with a winning strategy δ.

Proof. Soundness Suppose that δ is the strategy that Algorithm 2 returns. For each pair (ψ, a[Y/Σ]) of δ, we get that it satisfies the constraints illustrated in Definition 8. Hence, δ satisfies the requirements illustrated in the definition of winning stratigies.

Bounded Completeness Suppose that δ : {(ψ1, a1[Y1/Σ1 ]), · · · , (ψn, an[Yn/Σn])} is the winning strategy where for each ψi ∈ Ψ, there is a semi-ground action ai[Yi/Σi] s.t. each expression of Σi is of at most size m. According to Algorithm 2, the enumeration process in the Synthesize({θ}) process can generate the vector Σi of expressions of at most size m for each ψi ∈ Ψ. In addition, the verification process guarantees the correctness of Σi according to the constraints illustrated in Definition 8. Hence, Algorithm 2 returns a winning strategy s.t. each expression for the parameter of semiground actions is of at most size m.

Now, we discuss the decidability of the problem of strategy synthesis for ICGs. Given a fixed ICG, we have (1) the problem of strategy synthesis is undecidable [Luo and Liu, 2019] since it requires the entailment of arithmetic theory containing multiplication, which is undecidable; (2) the problem of the existence of a LIA-definable strategy is decidable remains open; (3) although the problem that synthesis LIA-definable strategy is decidable if the given ICG has a LIA-definable strategy, Algorithm 2 only computes a LIA-definable strategy under the condition that the cover generated by refining winning formula satisfies the meticulous condition.

Finally, we end with an example of refining the winning formula and synthesizing the winning strategy.

Example 5. We now synthesize the winning strategy of the 2-rowed Chomp game from the winning formula v1 ̸= v2+1. We first refine the cover of the winning formula as {v1 < v2+ 1, v1 > v2 + 1}. Then, according to Algorithm 2, we choose the action eat2(v1) for the first case, and eat1(v2 +2) for the second case. We combine all results, and obtain the winning strategy {(v1 <v2+1, eat2(v1)), (v1 >v2+1, eat1(v2+2))}.

5 Experimental Evaluation

We have implemented our approach, proposed in the previous section, to a system by using Python and Z3 [de Moura and Bjørner, 2008]. We evaluate our system on the following games: 2-rowed and L-shaped Chomp [Schuh, 1952], Empty-and-Divide [Ferguson, 1998], 2-piled Nim [Bouton, 1901], the monotonic variation of 2-piled Nim [Ahn et al., 2017], Take-away [Ferguson, 2018], and Subtraction [Yaglom, 2001]. All experiments were conducted on a machine with an Intel Core i5 2.50 GHz CPU and 8GB RAM under Windows 10. We let the maximal size m of expressions in the step of synthesizing winning strategies be 9, and use timeout of 300s for each synthesis task.

Although there are some related work about strategy synthesis [Beyene et al., 2014; Farzan and Kincaid, 2018], they cannot solve the above games in a fully-automated way. This will be explained in Section 6. Hence, we do not make a comparison with their work.

2-rowed Chomp: The winning formula is v1 ̸= v2 + 1, meaning that the number of cookies in the first row is not equal to the number of cookies in the second row plus 1. The

(a) The first 5 games and Subtraction game

(b) The Take-away game

Figure 1: Runtimes for impartial combinatoral games.

winning strategy is as follows: the player eats the cookie at (2, v1) (resp. (1, v2 + 2)) if v1 < v2 + 1 (resp. v1 > v2 + 1).

L-shaped Chomp: The L-shaped Chomp game is the Chomp game with an L-shaped board with vertical and horizontal lines. The state variables v1 and v2 denote numbers of chips on the vertical and horizontal lines respectively. The winning formula is v1 ̸= v2, and the winning strategy is that the player eats the cookie at (2, v1 + 1) (resp. (1, v2 + 1)) if v1 < v2 (resp. v1 > v2).

Empty-and-divide: There are two piles containing v1 and v2 chips respectivley. Each player can empty one of the piles, and then divides the chips of the other into two piles such that at least one chip is in each pile. This game ends when both of two piles contains only one chip. The winning state is a state such that the number of chips in any pile is divided by 2 (i.e., v1 ≡2 0 ∨ v2 ≡2 0). The winning strategy for the case v1 ≡2 0 is to empty the second pile, then to move v2 - 1 chips into the first pile, and finally to keep only one chip in this pile if v1 ≡2 0. The winning strategy for the case v2 ≡2 0 is similar.

2-piled Nim: There are two piles of chips containing v1 and v2 chips respectivley. Each player can choose one from these two piles, and then take arbitrary chips from it. Each player cannot remove chips from both piles in one turn. If both piles are empty, then the game ends. The winning formula is v1 ̸= v2. The winning strategy is to take v2 - v1 (resp. v1 - v2) chips from the second (resp. first) pile, if v1 < v2 (resp. v2 > v1).

Monotonic 2-piled Nim: This game is a monotonic variant of 2-piled Nim. The player can take arbitrary number of chips from one pile, given that the resulting sequence is non-decreasing. That is, the second pile always contains at least as many chips as the first pile (v1 ≤ v2). The winning formula is v2 > v1. The winning strategy is to take v2 - v1 chips from the first pile at any winning state.

Take-away: There is a pile that contains v chips. Let n be the parameter of this game, denoting the maximum of chips that the player can take. At least one chip must be taken. This games ends when no chip is in the pile. For any parameter n, the winning formula is v ≡n+1 0, meaning that the number of the remaining chips is not divided by n, and the winning strategy is to take chips such that v ≡n+1 0 holds. We test 28 testcases for this game where 3 ≤ n ≤ 30. As Figure 1(b) shows, the maximal time of computing winning strategy is 238s, and is able to scale up reasonably well.

Subtraction: The Subtraction game is a generalization of the Take-away game. Let S be a finite set of positive integers. In this game, each player can take k chips from the pile where k ∈ S. The ending state is that no player can execute the taking action. The winning formula and winning strategy varies for the games with different sets. Due to space reason, we only present the results our approach obtain for the game with {1, 4, 6}. The winning formula is v ̸≡5 0 ∧ v ̸≡5 2. The winning strategy is to take 1 (resp. 4) chip(s) if v ≡5 1 ∨ v ≡5 3 (resp. v ≡5 4). We test 11 cases for this game. Our approach can solve all cases in 192s, and solves 6 cases in a very short time (< 1.5s).

Finally, we close this section by summarizing experimental results. The runtimes of our approach in the above games are reported in Figure 1. Our approach is able to solve all games in a reasonable amount of time (< 250s). This shows the effectiveness and scalability of our approach on a wide range of games. Hence, our approach provides an effective way to constructing winning formulas and winning strategies.

6 RelatedWork

Strategy Synthesis in LTL Games. A well-known class of games, called Linear Temporal Logic (LTL) Games, is proposed in [Pnueli and Rosner, 1989]. These games are represented by an automaton, and the goals are expressed by an LTL formula. The method proposed in [Pnueli and Rosner, 1989] is an automaton-based approach causing a doubly exponential time complexity. To lower the complexity, Asarin et al. [1998] restrict the goal to be some fragments of LTL formulas so as to obtain polynomial synthesis approaches, e.g., the safety and reachability games whose goal is of the form ✷φ and ✸φ respectively where φ is propositional. The above methods only focus on games over finite states. In general, it is undecidable for the synthesis problem of infinite-state games [de Alfaro et al., 2001]. Some decidable restricted classes of infinite-state games are identified, e.g., games on automatic graphs [Neider and Topcu, 2016], pushdown graphs [Cachat, 2002; Chatterjee and Fijalkow, 2013], and prefix-recognizable graphs [Cachat, 2003].

Besides automatons, arithmetic formulas are an alternative to formalization for games. Compared to the former, the latter are easier to understand, and hence being more suitable for human beings to give a complete description. Recently, arithmetic formulas are used to represent infinite-state games [Beyene et al., 2014; Farzan and Kincaid, 2018]. Our representative framework is also based on arithmetic formulas, and close to their work.

Beyene et al. [2014] devise a sound and relatively complete proof rules for computing winning strategies for safety, reachability and LTL games over infinite states. All impartial combinatorial games considered in this paper are a reachability game over infinite states. The rules for reachability games rely on winning formulas and well-founded relations that are used to guarantee the correctness and termination of the winning strategy respectively. The generation of winning formulas and well-founded relations is solved by the EHSF solver [Beyene et al., 2013]. Our approach finds the winning formula via an enumerative approach, and does not generate the well-founded relation as an impartial combinatorial game always ends in a finite number of moves. One major drawback of Beyene et al.'s approach is that it requires users to provide hints in the form of templates to synthesize winning strategies, and hence it is not a full mechanization. By contrast, our approach succeeds in computing winning strategies for all games considered in this paper in a fully automated way.

Farzan and Kincaid [2018] propose a fully automated method, called SimSynth, for synthesizing winning strategies for reachability games over infinite states. SimSynth firstly unrolls games as a bounded variation. Then it reduces the problem of synthesizing the winning strategy for the bounded variation to the linear arithmetic satisfiability problem [Farzan and Kincaid, 2016]. Finally, it attempts to generalize the strategy so as to hold for all states. The insight of our approach is different from SimSynth. Instead, we first construct the winning formula, and then generate the winning strategy from the cover of the winning formula. SimSynth does not involve the winning formula, which precisely describes the set of winning states. In practice, SimSynth is only able to synthesizes the winning strategy of an ICG instance, and does not scale up well. For example, it fails to solve the 2-piled Nim game for the state v1 = 6∧v2 = 6 within 10 minutes. By contrast, our approach succeeds in computing generalized winning strategies, which works for not only one state but also all winning states, for the 2-piled Nim game in 3.91 seconds.

Another closely related work is the verification of strategies proposed in [Luo and Liu, 2019]. They extend the situation calculus for describing combinatorial games, and use finite state automaton (FSA) to represent generalized winning strategy. The key insight of their approach is to find an invariant for the FSA strategy, which is similar to the notion of winning formulas. Hence, their approach has a few ideas in common with those proposed in this paper and [Beyene et al., 2014]. Their approach only verifies if an FSA is a winning strategy, but cannot generate a winning strategy.

Generalized planning. A related problem is generalized planning that aims to construct a general plan that works for possibly infinitely many planning instances sharing the similar structure [Levesque, 2005; Srivastava et al., 2011]. In this paper, we concentrate on ICGs that is more complex than the planning domain. The former involves two players while the latter only focuses on the single-agent case. Hence it is necessary to consider not only how the current player chooses actions, but also how the other player responds when we synthesize winning strategies. Recently, De Giacomo et al. [2016] study the translation from generalized planning under partial observability to two-player games with perfect information. In the case there are no additional fairness assumptions, the former corresponds to two-player games with imperfect information. By adapting the belief-state construction, De Giacomo et al. remove imperfect information from games, and hence obtain a two-player game with perfect information corresponding to the given generalized planning problem. However, they do not provide an approach to synthesizing winning strategies for the games with perfect information corresponding to the given generalized planning problem.

7 Conclusions and FutureWork

We have devised an effective approach to computing generalized winning strategies that works for possibly infinite many instances of ICGs. The key insight of our approach is to synthesize the winning formula and winning strategy by extending the enumerative algorithm to learn multiple objects. To exploit the extended enumerative algorithm, we have provided constraints that are the specifications of the winning formula and winning strategy. In theory, our algorithm for synthesizing the winning formula (Alg. 1) is proven to be sound and relatively complete on LIA, and our algorithm for synthesizing the winning strategy (Alg. 2) is proven to be sound and bounded complete. We have implemented our approach and experimental results show the effectiveness and scalability of our proposed approach.

Our approach have some limitations, and hence leading to several avenues for future work. Firstly, the ICGs considered in this paper are formalized in LIA. For other ICGs, their formalization involves real numbers, existential quantifiers, multiple operator, rounding operator, exclusive-disjunction operator and so on. We would also like to consider the games whose formalizations require more expressive language. Secondly, the enumerative algorithm is a simple algorithm for the syntax-guided synthesis problem (SyGuS). It would like to design the solution to strategy synthesis based on more efficient algorithms for SyGuS [Alur et al., 2017; Reynolds et al., 2019]. Finally, we focus on ICGs under the normal rule. It is also interesting to apply our approach to other categories of games, e.g., ICGs under the mis`ere rule (i.e., all ending states are losing states), and partizan combinatorial games (i.e., some moves are available to one player and not to the other).

Acknowledgments

We are grateful to Yongmei Liu, Kailun Luo, Naiqi Li and Peiming Mo for their comments on the paper. This paper was supported by the National Natural Science Foundation of China (Nos. 61603152, 61602210, 61703182, 61772232, 61773179, 61877029, 61966009, U1711263, U1811263 and U1811264), the Science and Technology Planning Project of Guangdong (Nos. 2019KTSCX010, 2018KTSCX016 and 2019A050510024), the Science and Technology Project of Guangzhou (No. 201902010041), and the Project of Guangxi Key Laboratory of Trusted Software.