Background

The proof number search (PNS) is reviewed in Subsection 4.1.1, and Connect6 and NCTU6 are described in Subsection 4.1.2.

4.1.1 Proof Number Search

Proof number search (PNS), proposed by Allis et al. [2][4], is a kind of best-first search algorithm that was successfully used to prove or solve theoretical values [21] of game positions for many games [2][3][4][22][44][46][47][58], such as Connect-Four, Gomoku, Renju, Checkers, Lines of Action, Go, and Shogi. Like most best-first searches,

PNS has a well-known disadvantage, the requirement of maintaining the whole search tree in memory. As a result, many variations [8][27][36][38][47][58] have been proposed to avoid this problem, such as PN2, DFPN, PN*, PDS, and parallel PNS [26][44]. For example, PN2 used two-level PNS to reduce the size of the maintained search tree.

As described in [2][4], PNS is based on an AND/OR search tree where each node n is associated with proof/disproof numbers, 𝑝(𝑛) and 𝑑(𝑛), which represent the minimum numbers of nodes to be expanded to prove/disprove 𝑛. Basically, all leaves’ 𝑝(𝑛)/𝑑(𝑛) are initialized to 1/1. The values 𝑝(𝑛)/𝑑(𝑛) are 0/ if the node 𝑛 is proved, and /0 if it is disproved. PNS repeatedly chooses a leaf called the most-proving node (MPN) to expand, until the root is proved or disproved. The details of choosing MPN and maintaining the proof/disproof numbers can be found in [2][4].

An important property related to MPN is: if the selected MPN is proved (disproved), the proof (disproof) number of the search tree decreases by one. The property, called MPN Property in this thesis, can be generalized as follows.

 If the selected MPN is proved (disproved), the proof (disproof) number of the node, whose subtree includes the MPN, decreases by one, and the disproof (proof) number of it remains the same or increases.

4.1.2 Connect6 and NCTU6

Connect6 [61][62] is a kind of six-in-a-row game that was introduced by Wu et al. Two players, named Black and White, alternately play one move by placing two black and white stones respectively on empty intersections of a Go board (a 1919 board) in each turn.

Black plays first and places one stone initially. The winner is the first to get six consecutive stones of his own horizontally, vertically or diagonally.

NCTU6 is a Connect6 program, written by Wu et al. This thesis reviews the results

from [56][65] as follows. NCTU6 included a solver that was able to find Victory by Continuous Four (VCF), a common term for winning strategies in the Renju community.

More specifically, VCF for Connect6, also called VCST, wins by making continuous moves with at least one four (a threat which causes the opponent to defend) and ends with connecting up to six in all subsequent variations.

From the viewpoint of lambda search, VCF or VCST is a winning strategy in the second order of threats according to the definition in [65], that is, a _𝑎²-tree (similar to a

_𝑎²-tree in [56]) with value 1. Lambda search, as defined by Thomsen, is a kind of threat-based search method, formalized to express different orders of threats. Wu and Lin modified the definition to fit Connect6 as well as a family of k-in-a-row games and changed the notation from _𝑎^𝑖 to _𝑎^𝑖.

NCTU6-Verifier (abbr. Verifier) is a verifier modified from NCTU6 by incorporating a lambda-based threat-space search, and used to verify whether the player to move loses in the position, or to list all the defensive moves that may prevent the player from losing in the order _𝑎². If no moves are listed from a position, Verifier is able to prove that the position is a loss. If some moves are listed, Verifier is able to prove that those not listed are losses. In some extreme cases, Verifier may report up to tens of thousands of moves.

One issue for Connect6 is that the game lacks openings for players, since the game is still young when compared with other games such as chess, Chinese chess and Go. Hence, it is important for the Connect6 player community to investigate more openings quickly. For this issue, Wu et al. in [59] designed a desktop grid, like the job-level system, to help human experts build and solve openings.

In the earliest version of the grid, both NCTU6 and Verifier were the two jobs used, and a game record editor environment was utilized to allow users to select and dispatch jobs to free workers. NCTU6 was used to find the best move from the current game position,

while Verifier was used to expand all the nodes (namely for all the defensive moves). This environment helped human experts build and solve openings manually.

In this thesis, the system is modified to support a job-level system where job-level search can be used to create and perform jobs automatically. Both NCTU6 and Verifier are supported as jobs. NCTU6 jobs take tens of seconds on the average (statistics are given in Section 4.4.3), and Verifier jobs take a wide variety of times, from one minute up to one day, depending on the number of defensive moves. As above, in some extreme cases, Verifier may generate a large number of moves in Job-Level Search, which is resource-consuming for both computation and memory resources. Thus, Verifier is less feasible in practice.

In order to solve this problem, NCTU6 is modified to support the following two additional functionalities:

1. Support 𝐽(𝑛, 𝐶(𝑛)). Given a position 𝑛 and a list of prohibited moves 𝐶(𝑛) as input, NCTU6 generates the best move among all the moves outside the list. As described in Section 3.3, this can be used to find the best move of a position, the second best, …, etc.

2. For each job 𝐽(𝑛, 𝐶(𝑛)) , report a sure loss in the job result, if none of the non-prohibited moves can prevent a loss.

Supporting the first functionality, the modified NCTU6 can be used to find the best move of a position, the second best, …, etc., as described in Section 3.3. Supporting the second functionality, all the moves can be expanded like Verifier. Thus, NCTU6 is able to replace Verifier with Job-Level Search.