Single-player games that involve filling rectangular grids with numbers or symbols according to specific rules can be both challenging and captivating. Some of these games are inherently challenging and have a similar interesting property: finding solutions to these puzzles is typically “hard”, but once the solutions are found, checking whether these solutions satisfy the puzzles’ rules is relatively “easy”¹.A famous example of these puzzles Sis Sudoku. Another example is Suguru, a oneplayer game invented by Naoki Inaba, a prominent Japanese logic puzzle designer.

Suguru first emerged in 2001 [1] and gained popularity in the theoretical computer science community in 2022 after Robert et al. proved its NP-completeness [2]. The puzzles are played in rectangular grids; a grid is partitioned into one or more regions. Each region contains one or more orthogonally connected cells. Initially, some cells in the grid might be empty or filled with positive integers. These pre-filled cells are called the hint cells or simply hints. The objective of this puzzle is similar to the famous Sudoku—each empty cell must be filled with exactly one positive integer satisfying particular constraints. Suguru puzzles basically only have two rules: (1) for every region, each cell in that region must be filled with a unique integer between one and the number of cells in such a region, and (2) any two adjacent cells in the grid, either orthogonally or diagonally, must be filled with distinct integers.

Fig. 1 illustrates an example of a Suguru puzzle instance and its solution. Here, we consider a Suguru puzzle of size . The instance in Fig. 1a consists of nine regions: there are six regions of size 5 and one region each of size 1, 2, and 3. The instance has seven hint cells. Notice that the solution to this instance in Fig. 1b preserves these hint cells.

The computational aspects of various one-player puzzles have attracted interest in the theoretical computer science community, especially in their connection to NP-complete problems. In the last six years, many single-player logic puzzles were proven NP-complete, such as Calculation Solitaire [3], Choco Banana [4], Juosan [5], Path Puzzles [6], Suguru [2], Tatamibari [7], Tilepaint [8], Yin-Yang [9], and ZHED [10]. Various techniques have been proposed to solve some of these NP-complete puzzles. Most of them consider imperative approaches, such as the exhaustive search for solving Tatamibari [11], the prune-and-search technique for solving Yin-Yang [12], as well as various backtracking approaches for solving Juosan [13], Path Puzzles [14], Suguru [15], and Tilepaint [16]. Typically, these algorithms involve sophisticated search-based criteria in their computational steps. One of them, namely the backtracking approach for solving Suguru puzzles explained in [15], exhibits a factorial upper bound for its running time complexity—which is not optimal for an NP-complete problem.

The Boolean satisfiability problem (SAT problem) is a fundamental problem in theoretical computer science and mathematical logic. It is the first established NP-complete problem [17], [18], [19], [20]. Theoretically, all NP-complete problems can be transformed into SAT problem instances. This property enables various NPcomplete problems to be solved by SAT solvers—algorithms specifically designed to determine the satisfiability of propositional formulas. Due to its versatility, SAT solvers have been used to assist various problems in computer science, such as automated planning and scheduling [21], automated theorem proving [22], formal software or hardware verification [23], [24], solving complex optimization problem [25], and various aspects of artificial intelligence [26].

Numerous studies have investigated SAT-based approaches for solving singleplayer logic puzzles, such as binary puzzles [27], edge matching puzzles [28], fill-a-pix [29], Juosan [30], Path Puzzles [31], Skyscraper [32], Sudoku [33], [34], [35], and other various single player puzzles [36]. A recent extensive investigation by Bright et al. demonstrates the efectiveness of the SAT-based approach in solving puzzles using the declarative approach [36]. In this approach, one focuses on describing the problems and their constraints as sets of Boolean formulas, rather than providing a sequence of imperative commands. Some empirical performance comparisons of the SAT-based and imperative search-based approaches for solving logic puzzles were recently discussed in [30], [31]. Ammar et al. showed that Juosan puzzles with up to 1350 cells can be solved in less than one second on a standard personal computer, significantly outperforming the backtracking approach, which required four days or more to solve the same puzzles on the same machine [30]. Sakti et al. showed that the SAT-based approach outperforms the backtracking algorithm for solving Path Puzzles if the number of cells is suficiently large [31]. Nevertheless, one should note that, in earlier studies, the imperative paradigms still outperformed the SAT-based ones for small-sized puzzles.

This paper comprehensively discusses the SAT-based approach for solving Suguru puzzles. The analysis of this approach is discussed rigorously from both theoretical and experimental perspectives. The rest of the section in this paper is divided into four main parts. Section 2 discusses the preliminaries and related works, including an outline of the earlier algorithmic investigation of Suguru puzzles and some notational conventions. Section 3 comprehensively explains Suguru puzzles as SAT problem instances, which includes the SAT encoding for Suguru puzzles and its analysis related to the number of variables and clauses of the resulting propositional formulas. Section 4 presents the experimental results and their analyses, including the running time comparison between the previous backtracking technique and our proposed SAT-based approach. Finally, Section 5 concludes the paper with important findings and some open problems.

This section discusses a systematic approach for encoding Suguru puzzle instances and rules into propositional formulas. Suppose we consider an instance represented using an grid divided into regions. For a region , denotes the size of such a region (i.e., the number of cells in such a region). We define if and only if the cell belongs to a region . We can say that is the region label for the cell in a Suguru instance grid.

To represent a Suguru puzzle as a SAT formula, we define a propositional variable that is true if and only if the cell contains an integer . Here, , and where . The definition of this propositional variable is similar to that used in the Sudoku puzzle (see, e.g., [33], [34], and [40, Section 1.3]). We also write to signify that is true and to signify that is false (which is equivalent to is true). In practice, we can also define for a cell with if s _ { k } \end{document} ]]>.

The results in Theorem 3.5 suggest that an instance of Suguru puzzles can be transformed into a SAT problem instance eficiently, thereby allowing one to find the solution to a Suguru instance using the SAT solver efectively. The main purpose of this section is to describe the design, results, and analysis of our computational experiments. Experiments were conducted to evaluate the running times of our proposed SAT-based approach against various test cases. These running times were also contrasted with the running times of the previous backtracking algorithm proposed in [15] to provide a performance benchmark and for comparative purposes.

The experiments used the same computational environment as in [15]. Namely, we used a standard laptop with a 64-bit Windows 10 operating system equipped with an Intel(R) Core(TM) i7-1070H processor at 2.60 GHz and 16 GB of RAM. The SAT-based approach was implemented using MiniSat—a lightweight C++ library that provides a SAT solver interface and has historically been one of the most influential and widely studied SAT solvers. Although MiniSat is no longer actively maintained, it remains a popular choice for research and education purposes due to its simplicity and stable API. We selected MiniSat because it is implemented in C++, the same language used in [15] for the backtracking approach, ensuring objective and consistent performance evaluation between the two methods. MiniSat also provides a stable baseline with numerous examples and tools built around it. One should note that our main focus is on the SAT encoding rather than solver performance. However, we acknowledge that modern SAT solvers such as Glucose [43], CaDiCaL [44], or Kissat [45] could potentially ofer improved eficiency. Suguru rules and hints were represented using propositional formulas that were translated into MiniSat inputs.

As the experiments in [15], we considered the comprehensive 180 test cases collected from [46]. These test cases include Suguru puzzles of size where Of these test cases, 52 of them are of size . In addition to these test cases, we also randomly generated 50 test cases for further evaluation. These additional test cases are of size where , hence introducing puzzles of larger sizes to the experiments. The hint cells in the additional test cases constitute no more than 40% of the total number of cells. All instances in the test cases, both from [46] and the additional ones, are guaranteed to have a unique solution.

The procedure for generating additional test cases with guaranteed unique solutions is as follows. We first generate random Suguru board structures of size where using a randomized breadth-first search algorithm to create connected regions of cells in each structure. For each blank grid, we employ our SAT-based solver to find a complete solution, then apply a greedy hint minimization algorithm that iteratively removes filled cells while preserving solution uniqueness.

Uniqueness verification for an additional test case is performed using exhaustive SAT-based checking. The algorithm removes the hints one by one. After each hint removal, we solve the SAT instance to obtain the first solution, then add a constraint to exclude this solution, and attempt to solve the puzzle again. To check for another solution, we convert the first solution into a propositional formula, negate it, use the negated formula as a constraint, and try to find the second solution. If a second solution exists, the removed hint is restored as essential. The algorithm continues to remove hints until removing any additional one would result in a puzzle with multiple solutions. This way, the final puzzle is guaranteed to have exactly one solution. Our algorithm is also set so that the final puzzle contains at most 40% of cells as hints.

From multiple generation attempts across diferent board sizes, we successfully created 50 instances with a mathematically guaranteed unique solution. For each board where , we were able to construct 10 Suguru instances that have a unique solution with at most 40% of their cells as hints. The generation process involves multiple SAT solver calls for uniqueness verification, requiring substantial computational time that is separate from the puzzle-solving time, which is the main concern of our experimental investigation. The technical details of the method to generate a Suguru puzzle with a unique solution are described in Additional testcases generator.

We performed ten independent runs for each test case to obtain objective and accurate results regarding the running times for solving instances of Suguru puzzles. The measurements represent real elapsed times (wall clock times) observed during execution. It should be noted that the reported solving times measure only the time needed to solve the final puzzle with hints and do not include the time required to generate the puzzle. The running time data were then classified by grid size, and the average running time for each classification of Suguru puzzle instances was calculated. The C++ scripts, test cases, raw experimental results, and other relevant documents related to the experiment are available at Suguru sat. Our interactive SAT-based Suguru puzzle solver available at Interactive suguru playground.

To provide an objective and comprehensive analysis, we also re-run the experiment in solving the Suguru puzzles using the backtracking approach explained in [15]. Table 1 summarizes and contrasts the running times needed for solving the Suguru puzzles using the backtracking approach in [15] and our proposed SATbased approach. Although there are some diferences between the results in [15, Table 1] and those in Table 1 for the running times of the backtracking algorithm, their diferences are less than 10% and can be considered negligible. These diferences might occur due to some background processes in the computational device during the experiment. To provide more intuitive insight into the experimental results, we present and contrast the distribution of the running times for both backtracking and SAT-based approaches using boxplots in Fig. 4.

From Table 1, we notice that the SAT-based approach solves all instances in less than 12 milliseconds. The data in Table 1 and its representation in Fig. 4 indicate that the average running times of the SAT-based approach are less than that of the backtracking algorithm for larger puzzles, with crossover point as low as . The running time variances of the SAT-based approach are also significantly smaller than those of the backtracking algorithm as indicated in Fig. 4. As discussed in Section 3.2, the running time of our SAT-based approach does not directly depend on the number of hints—the main contributor to this running time is the size of the puzzle. On the other hand, the running time of the backtracking algorithm in [15] depends on the number of regions and hints, specifically the asymptotic running time for solving an m × n Suguru instance containing R regions and H hints is (cf. [15, Corollary 1]).

Although the average running times for the SAT-based approach for solving the puzzles where are higher than those of the backtracking algorithm (with the exception for the puzzles), the maximum running times for solving the instances for SAT-based approach are less than those of the backtracking algorithm for the puzzles of sizes , and . Moreover, one challenging instance of size that takes almost 480 milliseconds to be solved by the backtracking algorithm can be solved in under 2.5 milliseconds by the SATbased approach. This challenging instance—which is also discussed in [15, Fig. 7]—is depicted in Fig. 5. In terms of the minimum running time, the data in Table 1 shows that the SAT-based approach outperforms the backtracking algorithm for solving Suguru instances of sizes n × n where .

Based on the average running times data in Table 1—we see that, on average— our proposed SAT-based approach is at least around 20 times faster than the backtracking algorithm in solving the puzzles for . Furthermore, based on the minimum running times data in Table 1, we see that the SAT-based approach is at least three times faster than the backtracking algorithm in solving the n × n puzzles for . Interesting results occur for the 15 × 15 puzzles, in which the SAT-based approach is at least six times faster than the backtracking algorithm for solving all instances and is up to 50 000 times faster than the backtracking algorithm for solving some specific instance.

One should note that unlike the backtracking technique proposed in [15], the number of regions, the number of hints cells, and the hint cells’ arrangement do not directly afect the asymptotic running time of our SAT-based approach. Based on these experimental results, we might infer that our SAT-based approach is more eficient for solving larger Suguru puzzles—although it is not always eficient in solving the smaller ones.

In this paper, we have demonstrated an eficient SAT-based technique for solving general Suguru puzzles. We express the rules of Suguru puzzles in propositional formulas in CNF and discuss their properties regarding the number of variables, clauses, and literals. In Theorem 3.5, we show that the number of variables and clauses in the resulting formulas is bounded above by some polynomials representing the puzzles’ sizes. Thus, our proposed encoding is polynomially proportional to the dimensions of the puzzles, which allows for the eficient transformation of Suguru instances into SAT problem instances. This encoding also provides a technique for reducing Suguru puzzles into SAT problems.

We utilize MiniSat, implemented in C++, for our experiments. Although MiniSat is no longer actively maintained, it remains widely used in research and educational contexts. For future research, we recommend implementing our SATbased approach using more eficient SAT solvers such as Glucose [43], CaDiCaL [44], or Kissat [45]. The results from such experiments could serve as benchmarks for evaluating algorithmic strategies in solving the Suguru puzzle.

The summary of experimental results in Table 1 and Fig. 4 suggests that our proposed SAT-based approach outperforms the backtracking technique for solving larger puzzles in terms of running time, although it is not always eficient for solving smaller puzzles. We obtained a crossover point as low as for the average running time—meaning that, on average, solving Suguru puzzles using the SAT-based approach is faster than the backtracking technique for . In terms of the maximum running time, we also see that the SAT-based approach is always more eficient than the backtracking technique for solving puzzles for . Moreover, based on the minimum running time, we see that the SAT-based approach is always faster than the backtracking one for solving puzzles for . According to the experimental results, the running time variances of our proposed SAT-based technique are much smaller than those of the backtracking technique. These empirical outcomes support the theoretical result discussed in Section 3, which states that the main contributor to the running time of the SATbased approach is the dimension of the puzzle. Unlike the backtracking approach discussed in [15], the running time of our SAT-based approach does not directly depend on the number of hints, the positions of the hints, and the arrangements of the cells in a region. One should note that, despite the eficiency exhibited by the SAT-based approach for solving Suguru instances of larger sizes, the backtracking technique still prevails in solving smaller puzzles.

There are some interesting open problems related to solving Suguru puzzles. First, we do not prove the optimality of our SAT encoding technique. It might be possible to construct a SAT encoding that is more eficient (in terms of the number of variables and clauses) than our proposed encoding in Section 3.1. A possible improvement can be made by considering a more eficient SAT encoding for the third rule, stating that no adjacent cells contain the same integers. Second, our experimental results are limited to Suguru puzzles, even though the puzzles can be defined over rectangular grids where . The main reason for this is because our test cases are mainly taken from [46] (which is also used in [15]). One can consider additional experiments that use more diverse test cases by employing Suguru instances of size m × n where m , and then can investigate the resulting empirical consequences concerning the theoretical results in Theorem 3.5. Third, our SAT-based algorithm can be used to construct a Suguru puzzle generation algorithm described in Section 4. Our current puzzle generation algorithm employs an exhaustive SAT-based checking approach, which requires a substantial amount of time to generate a puzzle with a unique solution. To our knowledge, investigations into the technique for constructing a Suguru puzzle with a unique solution are still underexplored. Finally, our SAT-based approach can also be modified to solve Suguru puzzle-related problems, such as counting the number of solutions for a given Suguru instance. To our knowledge, theoretical and computational problems related to counting the number of solutions for a Suguru puzzle instance remain an open problem.