PCP Solver is a Java application which (tries to) solve instances of Post's Correspondence Problem.
Post's Correspondence Problem, PCP for short, is mostly of theoretical importance. It is an example of a problem computers cannot solve and goes as follows. You are given a set of dominoes. Each domino has a topstring and a bottomstring. For example, the domino a/ab has topstring a and bottomstring ab. You must determine whether or not there exists a sequence of these dominoes such that the concatenation of the topstrings is the same as the concatenation of the bottomstrings. Such a sequence—called a 'match'—must contain at least one domino and may use any of the given dominoes zero or more times.
For example, the set of dominoes {ab/b, b/a, a/ab} has a match. The concatenation of the topstrings in the sequence a/ab, b/a, ab/b is the same as the concatenation of the bottomstrings: abab.
For more information on PCP, see Wikipedia and Ling Zhao's PCP website.
PCP Solver tries to solve as many PCP instances as possible. It applies an exhaustive Iterative Deepening A* search (implemented by the JSearch library) to find a match. The search finishes either when a match is found, or when all possibilities are explored and no match exists. Since PCP is unsolvable, for some instances the search will continue indefinitely. PCP Solver also implements some simple rules to detect PCP instances without a match and thereby avoids a long unnecessary search in some cases. For more information on the state of the art of solving PCP instances, see Ling Zhao's website.
Download the executable JAR (v1.1, v1.0) and run by double clicking or execute java -jar pcpsolver-1.1-jar-with-dependencies.jar from the commandline.
PCP Solver requires Java 6 or later.
The source code is available on GitHub and is licensed under GPLv3.
Please report any bugs or suggestions via GitHub.
- Ling Zhao provides the C++ source code of his PCP Solver. You must compile it yourself. It is probably the fastest and most advanced PCP Solver available, but only works for PCP instances with a binary alphabet (
0s and1s). The code is also available at GitHub. - There is an online PCP Solver implemented in PHP. It is capable of solving some simple PCP instances, but may crash on harder problems.