Post Correspondence Problem (PCP) is a well-known undecidable problem. Solving instances with solutions is straightforward with exploration algorithms, but proving infeasibility is challenging. This research introduces two methods to demonstrate infeasibility, including generating formal proofs in Isabelle/HOL.
The Post Correspondence Problem (PCP), proposed by Post in 1946 [1], is undecidable. PCP instances use tiles with two strings on top and bottom. 100 1 0 100 1 00
In this example, there are three kinds of tiles, each available in infinite quantities. The problem is to determine whether it is possible to arrange one or more tiles in such a way that the reading of the top and bottom strings matches. In this particular instance, a solution (indices of arrangement of tiles) is "1311322", and this shows that both the top and bottom read "1001100100100". For instances that have a solution, it is possible to find the solution within finite time using an exploration algorithm. On the other hand, determining that no solution exists is challenging, and due to the undecidability of the problem, no general algorithm exists for this purpose. Previous research has proposed heuristic algorithms for finding solutions [2,3] and Ling Zhao (2003) [2] attempted to solve all the problems in PCP [3,4] and left 3,170 problems unsolved. PCP [3,4] refers to a set of all instances where the number of tiles is 3, and the maximum length of the written strings is 4.
This research makes the following three main contributions. β’ Propose two novel algorithms to demonstrate that a PCP instance has no solution.
β’ Solve all problems of PCP [3,4] except for 13 problems.
β’ Show an example of automatic proof generation for concrete problems.
We formulate PCP as a string constraint problem. Regarding the string constraint π of the PCP instance πΌ, the satisfiability is undecidable. We consider π β² such that π(π€) βΉ π β² (π€) and is efficiently decidable. Such π β² is referred to as a relaxation problem (simply relaxation) of π. By showing that π β² is unsatisfiable, we would like to show that π is also unsatisfiable. For example, considering only the number of characters |π π (π€)| = |π β (π€)| is suitable as π β² . Additionally, matching Parikh images or the number of specific words is another example of π β² . Generalizing these examples, we have the following proposition.
Proposition 2.3. Let π be an arbitrary total integer-vector-output transducer. Consider
This is a relaxation problem of π and is decidable. We set some π and hope it is infeasible.
Although details are omitted, the condition π (π π (π€)) β© π (π β (π€)) β β can be reduced to the emptiness problem of a Parikh automaton constructed from π, π π , π β , and their product. The Parikh automaton emptiness algorithm we use is largely similar to the one described in Section 3 of [4], so we omit the details. While not detailed here, our algorithm achieved significant speedup by applying two techniques to this algorithm: (1) delaying and dynamically adding constraints related to connectivity, and (2) reducing the problem to a natural form for Mixed Integer Programming and leveraging a cutting-edge MIP solver.
Intuitively, arranging each tile one by one represents a transition, and "the remaining part of the string and whether it is on the top or bottom" represents a state. We call such a pair configuration. PCP can be formulated as a reachability problem: "Is it possible to reach the state of the empty string?" , the next state will be "top, remainder 0111. "
We formulate PCP as a reachability problem. First, we define the transition system of PCP.
. Let πΌ = ((π 1 , β 1 ), β¦ , (π π , β π )) be a PCP instance of size π over Ξ£. We define the transition system π π = (π, π , πΌ πππ‘, π΅ππ) as follows.
β’ State set π = {top, bottom} Γ Ξ£ * .
β’ Transition function π βΆ π β 2 π is defined as follows.
β’ Bad state set π΅ππ = {(top, π), (bottom, π)}.
β’ Intial state set πΌ πππ‘ = π (top, π).
The states after arranging one tile is considered the initial state, as an empty arrangement is not valid.
In the following, π is naturally extended and used as π βΆ 2 π β 2 π . The behavior of the transition π (bottom, π€) is illustrated below. When π€ is the current state, adding (π π , β π ) results in the remaining part becoming the next state π€' . There are two patterns: one where the same side as the previous state continues, and one where the side changes. If πΌ ππ£ exists, then it implies that π΅ππ is unreachable from initial states.
In the following section, we introduce algorithms to discover πΌ ππ£.
For the Reachability Problem, many powerful algorithms like PDR (Property Directed Reachability) [5] exist. We extended PDR and achieved some success (see Section 5). We also devised a novel ad-hoc method specific to PCP, described below.
). Let π β {top, bottom} and π΄ be a finite automaton over Ξ£. We call the pair (π , π΄) the configuration automaton. The language of (s, A) is denoted as πΏ(π , π΄) and defined as follows. This represents a state set of the transition system.
The aim of this algorithm is to discover a pair of configuration automata (for top and bottom) that represents πΌ ππ£. It should be noted that not every πΌ ππ£ has such a pair due to the regularity of the underlying automata, which limits the scope of our consideration.
This algorithm manages a graph πΊ = (π , πΈ) where each node is a configuration automaton. Specifically, each node π£ is associated with a set of states of a transition system. The algorithm proceeds by expanding the overall union πΏ(π ) = β π£ πΏ(π£) until it becomes an invariant.
Intuitively, the edge (π’, π£) in this graph represents a dependency relationship. This relationship means "if π£ cannot reach π΅ππ, then π’ cannot reach π΅ππ either". If we can construct a graph where every node has such dependencies and does not contain any bad state, then πΏ(π ) is an invariant. There are two types of this relation, as follows.
The algorithm is essentially a breadth-first search (BFS). When considering only the transition relation, the process operates similarly to BFS. A distinctive feature of this algorithm is that it proactively abstracts nodes. For example, when a node such as (top, 0011101) appears, the algorithm attempts to create a node like (top, . * 110. * ) (we use a regex to represent an automaton) and draw an edge to it. If this abstracted node can reach π΅ππ, it is removed and backtracking is performed.
So far, we have presented two methods and complicated algorithms. However, there is a significant possibility that my implementations for these algorithms may contain bugs. Even if we successfully solve all instances of PCP [3,4], our results would still be far from being considered trusted facts. Therefore, we decided to have our algorithm output proofs in the form of Isabelle/HOL code. Another possible approach is to use Isabelle/HOL or similar tools to verify the correctness of the algorithm's implementation. However, this makes it difficult to optimize the algorithm for speed. For instance, The first method relies on an external MIP solver for its efficiency, making it challenging. Additionally, for others to quickly trust our results, it is crucial that all instances of ππΆπ [3,4] and their proofs are organized and verified within some proof assistant such as Isabelle/HOL.
Currently, only the second method is capable of outputting a certificate. The first method will be addressed as future work (see Section 6).
Consider the transition system of a PCP instance. By defining the invariant concretely in Isabelle/HOL and proving each of the invariant conditions (see Definition 3.4), we can validate it. This method is independent of the implementation details used in the second method and can be utilized by various algorithms discovering invariants.
Our implementation of the second method generates the following code. Proofs such as "the existence of πΌ ππ£ implies that the PCP has no solution" were conducted manually in advance. Examples of complete proofs are found on the author's GitHub repository [6]. [3,4] In this research, we address the instances of PCP [3,4]. Ling Zhao (2003) [2] attempted to solve all these instances but left 3,170 unsolved. The list of these instances is available on his website [7]. Our goal was to solve all instances of PCP [3,4], gradually reducing the number of unsolved problems. As shown in Figure 5, the initial 3,170 unsolved problems were reduced to 127 using the first method. After several additional methods, only 13 problems remained unsolved. These remaining problems are listed on the author's website [8].
PDR, SAT, Method2(1), and Method2(2) are techniques for discovering πΌ ππ£. Certificate generation is implemented for those methods. The method SAT uses a SAT solver to discover πΌ ππ£, while Method2(1) and Method2(2) differ in their abstraction methods.
We have been working for a complete resolution of PCP [3,4] and came close, with only 13 instances remaining unsolved. To have these results accepted as trusted facts, we also aim to provide formal proofs using Isabelle/HOL for each instance, which has been achieved for the second method. Although both goals are yet to be fully achieved, we believe they are attainable as outlined below.
To solve the remaining 13 problems, we consider two possibilities. One is to solve these instances manually. We predict that most of the 13 problems do not have solutions, and providing ad-hoc proofs by humans might be the quickest way. The other possibility involves devising new variants of the methods in this paper or investing additional computational resources. Since the manual approach can also help gain deeper insights into individual instances and PCP itself, we would like to first aim for manual resolution.
Generating certificates for the first method is challenging because it uses an external Mixed Integer Programming (MIP) solver as a subroutine. Generating a certificate for the feasibility of an MIP is straightforward, as it merely requires providing a specific solution. However, generating a certificate for infeasibility is more difficult. Cheung et al. (2017) [9] extended the existing MIP solver SCIP to output easily verifiable certificates in their own format. We believe that we can overcome this difficulty by converting these certificates into Isabelle/HOL code.
This work was supported by JSPS KAKENHI Grant Number 19K11899 and 24K14891.