This Python program serves as a basic implementation of a Boolean Satisfiability (SAT) solver. The solver determines whether a given propositional logic expression can be satisfied by assigning truth values to its variables.
- Solves SAT problems using a brute-force approach.
- Handles basic logical symbols: AND (^, ∧), OR (v, ∨), NOT (~, ¬), THEN (>), IFF (<>).
- Supports single-character variable names.
- Generates all possible interpretations to check satisfiability.
satsolver.py: The main Python script that implements the SAT solver.formuls.txt: Some samples for the input of this script.README.md: This file, provides an overview of the SAT solver and instructions.
- Clone this repository to your local machine:
git clone https://github.com/iman2693/SAT-Solver.git
cd SAT-Solver This solver uses a basic brute-force approach and is suitable for small expressions. For larger or more complex expressions, consider using more advanced SAT-solving algorithms.
This project is licensed under the MIT License.