This is a soduko solver which can solve 4*4 Soduko given any initial number.
Using propositional logic I designed a knowledge base of the solver that describes all rules and initial information about the sudoku game with the propositional variable(see generate_knowledge.py)