SAT Problem solved by using a genetic algorithm for the Analysis of Algorithms course.
This implementation of SAT takes each clause as a collection of OR's.
The program takes as input a file that must be formatted in a specific way.
Each variable must be a number from 1 to (Amount of variables), to represent a NOT simply put the same number but as a negative.
Format
- First Line: Amount of variables
- Second Line: Amount of clauses
- Next Lines: Clauses (Each variable must be separated by a space)
5
4
1 3 4
-5 -2
1 2
-3
This translates to:
- 5 Variables (A, B, C, D, E)
- 4 Clauses
- A or C or D
- (not E) or (not B)
- A or B
- not C