The Satisfiability Problem (SAT) and Tabu Search

Question 1

Describe the satisfiability problem.

Answer 1

SAT is a class in which you have some conditions to be satisfied (eg. a list of boolean expressions). The problem comes when you want to satisfy as many of them as possible.

Question 2

Describe the gist of tabu search.

Answer 2

The idea is to create a list of solutions or changes which are taboo for some time. You’re not allowed to go back to a solution on the tabu list, nor are you allowed to change a variable on the list.

This can either be implemented as a list with some capacity (Eg. sorted by age), or a sa list describing how many iterations you can’t change each variable for.

Question 3

Describe how Noureddine has run tabu search on boolean expressions.

Answer 3

1) During each iteration, he has created a list where he’s bitflipped all variables that are not taboo.
2) He’s then ranked them and selected the flip which caused the biggest gain, and sett this as the new solution.
3) Afterwards, he’s updated the tabu list to say this variable is not to be changed for some iterations.