The satisfiability problem also known as Boolean Satisfiability Problem is a (yes/no) decision problem, which, given a propositional logic formula, determines whether there is an assignment of the propositional variables that makes the formula satisfiable (true).
SAT occupies a central place in artificial intelligence. The satisfiability of logical formulas, more precisely CNF forms (conjunctive normal forms) of zero order, means that we are on the side of problem solving, automatic reasoning and in any other axis of AI or logic is necessary.
For this project, We are interested in the instances of the benchmark uf75-325 / uuf75-325 defined as follows:
Instance :
𝑋= 𝑥1𝑥2𝑥3 ... ... ... ... 𝑥75 :Set of Boolean variables.
𝐶= 𝑐1𝑐2𝑐3 ... ... ... ... 𝑐325 :Set of Clauses where ci is a disjunction of literals.
A literal is a Boolean variable with or without the negation connector.
Question:
Is there an instantiation (a set of Boolean values associated with variables) of X such that the conjunction of the clauses of C is true (SAT)?
For this purpose, we will solve this instance by studying 3 different parts:
- Using blind methods : the depth-first search (DFS) algorithm.
- Using heuristic methods: the A* algorithm.
.
- Using Bio Inspired and Evolutionary Methods: The Genetic Algorithm.
- Using methods from the family of swarm-based algorithms: Ant Colony System (ACS).
In order to test the implemented algorithms of search in depth first and A* we considered the 100 instances of benchmark UUF75 and we carried out executions of 5 minutes of duration, and for GA and ACS we give the following parameters:
- GA : 2500, 25, 50, 50 are the number of ilterations, population size, crossing rate, and mutation rate, respectively.
- ACS: 2.1, 0.03, 0.001, 30, 0.001, 70 are the following parameters: alpha, Ro, Beta, Ants Numbers, Q0, and Ilteration number, respectively.
the results obtained are illustrated in the following table:
| Algorithm | Average number of clauses | Average rate | Best Number Of SAT Clause | Worst Number Of SAT Clause |
|---|---|---|---|---|
| DFS | 280 | 86.40% | 291 | 264 |
| A* | 299 | 92% | 311 | 284 |
| GA | 321 | 98.93% | 325 | 317 |
| ACS | 302 | 93.14% | 313 | 294 |
After observing the results of the blind (DFS) and heuristic (A*) methods and those obtained using the genetic algorithm and the ACS, on the given instances of SAT problem, it is clearly observed that the genetic algorithm allows to provide better quality solutions.
In terms of time, GA is clearly much faster than other methods (premature convergence) a large satisfiability rate in less than one minute.
We can clearly see that some instance only satisfies less than 320 clauses and this is because some clauses are difficult to solve or they are not satisfiable.