Scalability of Prolog: Real-world logic applications
Abstract
Applications of Logic vary from Verification of Systems, Scheduling, and Solving Puzzles like Sudoku and Magic Square. Satisfiability Problem on Propositional Logic is decidable , but NP Complete. Prolog is a famous language for Logic Paradigm. It also solves the Satisfiability Problem, just not for Propositional Logic. It finds all satisfying solutions which is one of the reasons it is slow. It barely manages to solve a 3x3 magic square puzzle in 5 minutes. But, in many cases, we require only one satisfying solution. SAT solvers work on Propositional Logic and find a satisfying solution quite quickly by using well-known algorithms and heuristics. SMT solvers extend SAT Solvers to higher order logic. A demo of nxn magic square puzzle, graph coloring using Z3 and a tutorial on solving problems with PyZ3 concludes the lecture.
