A Python program that solves Knights and Knaves logic puzzles using propositional logic and model-checking algorithms. Determine the truthfulness of characters based on their statements to solve these classic logic puzzles.

Program that solves Raymond Smullyan's “Knights and Knaves” logic puzzles. It uses logical inference rules and the puzzle's conditions as a knowledge base.