=Paper=
{{Paper
|id=Vol-3754/paper14
|storemode=property
|title=Methods for solving the Post correspondence problem and certificate generation
|pdfUrl=https://ceur-ws.org/Vol-3754/paper14.pdf
|volume=Vol-3754
|authors=Omori Akihiro,Minamide Yasuhiko
|dblpUrl=https://dblp.org/rec/conf/sycss/AkihiroY24
}}
==Methods for solving the Post correspondence problem and certificate generation==
https://ceur-ws.org/Vol-3754/paper14.pdf
Methods for Solving the Post Correspondence
Problem and Certificate Generation
Akihiro Omori1 , Yasuhiko Minamide2
1
Department of Mathematical and Computing Science, Tokyo Institute of Technology, Tokyo, Japan
2
Department of Mathematical and Computing Science, Tokyo Institute of Technology, Tokyo, Japan
Abstract
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.
Keywords
Post’s Correspondence Problem, Formal Verification, Reachability Problem, Automata
1. Introduction
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 0 1
1 100 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”.
100 1 100 100 1 0 0
1 00 1 1 00 100 100
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.
SCSS 2024: 10th International Symposium on Symbolic Computation in Software Science, August 28–30, 2024, Tokyo,
Japan
Envelope-Open omori.a.ab@m.titech.ac.jp (A. Omori); minamide@c.titech.ac.jp (Y. Minamide)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
92
• 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.
2. The First Method: String Constraint Formulation
We formulate PCP as a string constraint problem.
Example 2.1 (Example of 𝑇𝑔 and 𝑇ℎ ). Let PCP instance 𝐼 = ((1111, 1110), (1101, 1), (11, 1111)).
We denote the top and bottom strings on the 𝑖-th tile by 𝑔𝑖 and ℎ𝑖 , respectively. Let 𝑇𝑔 and 𝑇ℎ be
transducers as defined below. Intuitively, the transducer 𝑇𝑔 outputs 𝑔1 for ‘1’, 𝑔2 for ‘2’, and does
not accept the empty string. The string 𝑤 is a solution to the PCP if and only if 𝑇𝑔 (𝑤) = 𝑇ℎ (𝑤).
1/1111 1/1111 1/1110
1/1110
2/1101 2/1
𝑞0 𝑞𝑓 2/1101 𝑞0 𝑞𝑓 2/1
3/11 3/1111
3/11 3/1111
Figure 1: 𝑇𝑔 Figure 2: 𝑇ℎ
Definition 2.2 (String Constraint of PCP). The constraint 𝑇𝑔 (𝑤) = 𝑇ℎ (𝑤) created in this way is
called the string constraint of instance 𝐼.
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
𝑊 (𝑇𝑔 (𝑤)) ∩ 𝑊 (𝑇ℎ (𝑤)) ≠ ∅ (1)
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.
93
3. The Second Method: Transition System Formulation
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?”
Example 3.1. When arranging two tiles like 100 10 , the state representing it is “top,
1 0
remainder 010.” If a transition is made by appending 111 , the next state will be “top, remainder
01
0111.”
3.1. Problem Definition
We formulate PCP as a reachability problem. First, we define the transition system of PCP.
Definition 3.2 (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.
𝑇 (bottom, 𝑤) = {(bottom, 𝑤 ′ ) ∣ ∃𝑖 ≤ 𝑠. 𝑤ℎ𝑖 = 𝑔𝑖 𝑤 ′ } ∪ {(top, 𝑤 ′ ) ∣ ∃𝑖 ≤ 𝑠. 𝑤ℎ𝑖 𝑤 ′ = 𝑔𝑖 }
𝑇 (top, 𝑤) = {(top, 𝑤 ′ ) ∣ ∃𝑖 ≤ 𝑠. 𝑤𝑔𝑖 = ℎ𝑖 𝑤 ′ } ∪ {(bottom, 𝑤 ′ ) ∣ ∃𝑖 ≤ 𝑠. 𝑤𝑔𝑖 𝑤 ′ = ℎ𝑖 }
• 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.
𝑔𝑖 𝑤′ 𝑔𝑖
𝑤 ℎ𝑖 𝑤 ℎ𝑖 𝑤′
(a) Pattern where the side doesn’t change (b) Pattern where the side changes
Definition 3.3 (Reachability Problem of PCP). Does there exist 𝑛 such that
𝑇 𝑛 (𝐼 𝑛𝑖𝑡) ∩ 𝐵𝑎𝑑 ≠ ∅
94
Definition 3.4 (Inductive Invariant of PCP). A set 𝐼 𝑛𝑣 that satisfies the following three condi-
tions is called an inductive invariant (simply invariant).
• 𝐼 𝑛𝑖𝑡 ⊆ 𝐼 𝑛𝑣
• 𝐼 𝑛𝑣 is closed under 𝑇: 𝑇 (𝐼 𝑛𝑣) ⊆ 𝐼 𝑛𝑣
• 𝐼 𝑛𝑣 does not include 𝜖: 𝐵𝑎𝑑 ∩ 𝐼 𝑛𝑣 = ∅
Lemma 3.5. If 𝐼 𝑛𝑣 exists, then it implies that 𝐵𝑎𝑑 is unreachable from initial states.
In the following section, we introduce algorithms to discover 𝐼 𝑛𝑣.
3.2. Algorithm
For the Reachability Problem, many powerful algorithms like PDR (Property Directed Reacha-
bility)[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.
Definition 3.6 (Configuration Automaton). 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 relation-
ship 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.
1. Inclusion relation: 𝐿(𝑢) ⊊ 𝐿(𝑣)
2. Transition relation: 𝑇 (𝐿(𝑢)) = 𝐿(𝑣)
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.
Figure 4 shows a successful execution example for 1111 0 1 . The square nodes
1 11 1100
represent nodes with singleton languages, and the round nodes are abstracted nodes with
regular expressions appearing in their labels. The dotted lines represent inclusion relations, and
the solid lines represent transition relations. Note that in this figure, the transition relations are
extended to 𝑛 (where 𝑛 ≥ 1) steps, with intermediate steps omitted.
95
bottom,00 bottom,11 bottom,11100
top,111
bottom,11001100
top,.*1.* top,1
bottom,.*0110.*
top,.*0.* top,.*00.*
bottom,001100
bottom,100
Figure 4: Example of Graph of Invariant
4. Certificate Generation
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).
4.1. Certificate: Pair of Automata
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.
1. Definition of the PCP instance
2. Definition of 𝐼 𝑛𝑣
a) The top-side Automaton
b) The bottom-side Automaton
3. Proof of the closedness of 𝐼 𝑛𝑣
a) Definition of 𝑇 (𝐼 𝑛𝑣) (in the form of a specific pair of deterministic automata)
96
b) Concrete definition of the automaton for 𝐼 𝑛𝑣 ∩ 𝑇 (𝐼 𝑛𝑣)
c) Proof of 𝐼 𝑛𝑣 ∩ 𝑇 (𝐼 𝑛𝑣) = ∅
d) Proof of 𝐼 𝑛𝑣 ∩ 𝑇 (𝐼 𝑛𝑣) similarly, and show that 𝑇 (𝐼 𝑛𝑣) ⊆ 𝐼 𝑛𝑣
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 reposi-
tory [6].
5. Application to PCP[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 gener-
ation 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.
Method 1 PDR
3170 cases 127 cases 73 cases
SAT Method 2(1) Method 2(2)
71 cases 26 cases 13 cases
Figure 5: Journey of Solving PCP[3,4]
6. Conclusion and Future Work
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,
97
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.
Acknowledgments
This work was supported by JSPS KAKENHI Grant Number 19K11899 and 24K14891.
References
[1] E. L. Post, A variant of a recursively unsolvable problem, Bulletin of the American
Mathematical Society 52 (1946) 264–268.
[2] L. Zhao, Tackling Post’s correspondence problem, in: Computers and Games, Springer
Berlin Heidelberg, 2003, pp. 326–344.
[3] R. J. Lorentz, Creating difficult instances of the post correspondence problem, in: Computers
and Games, Springer Berlin Heidelberg, Berlin, Heidelberg, 2001, pp. 214–228.
[4] N. Verma, H. Seidl, T. Schwentick, On the complexity of equational horn clauses, 2005, pp.
337–352. doi:10.1007/11532231_25 .
[5] A. R. Bradley, Sat-based model checking without unrolling, in: Proceedings of the 12th
International Conference on Verification, Model Checking, and Abstract Interpretation,
VMCAI’11, Springer-Verlag, Berlin, Heidelberg, 2011, p. 70–87.
[6] A. Omori, pcp-proof, https://github.com/Mojashi/pcp-proof, 2024.
[7] L. Zhao, Pcp documents, 2002. URL: https://webdocs.cs.ualberta.ca/~games/PCP.
[8] A. Omori, Unresolved problems, 2024. URL: https://pcp-vis.pages.dev/gallery.
[9] K. K. H. Cheung, A. Gleixner, D. E. Steffy, Verifying integer programming results, in:
F. Eisenbrand, J. Koenemann (Eds.), Integer Programming and Combinatorial Optimization,
Springer International Publishing, Cham, 2017, pp. 148–160.
98