Artificial intelligence (AI) is concerned with enabling machines to make "intelligent choices". In AI planning, the branch of artificial intelligence involving intelligent agents, autonomous robots, and crewless vehicles, the "intelligent choices" are based on finding a strategy based on a description of the world, the desired goals, and the possible actions to achieve the given goals. Finding these strategies is a very complex problem. Therefore, such search problems are often transformed into the boolean satisfiability problem (SAT), which often can be solved effectively using modern SAT solvers. At first glance, it is surprising that the above method is effective at all, as it is expected to be impossible to solve the SAT problem in polynomial time (this is the famous P ≠ NP conjecture). However, the SAT problems in AI planning can be solved highly effectively, even in high-dimensional settings with more than a million variables. This is presumed to be due to the fact that only a small fraction of SAT problems are difficult to solve (requires exponential time). These problems lie at the interface where the SAT problem goes from under-restricted to over-restricted. This project aims to make a mathematical proof of the validity of this famous conjecture.
