Mémoire de Maîtrise
DOI
https://doi.org/10.11606/D.76.2021.tde-02092021-162034
Document
Auteur
Nom complet
Heitor Pascoal de Bittencourt
Unité de l'USP
Domain de Connaissance
Date de Soutenance
Editeur
São Carlos, 2021
Directeur
Jury
Fontanari, Jose Fernando (Président)
Gomes, Paulo Freitas
Rosas, Alexandre da Silva

Titre en anglais
Search strategies and phase transition in the Random Boolean satisfiability problem
Mots-clés en anglais
Boolean satisfiability problem
Local search algorithms
NP-complete problem
Phase transitions
Random problems
Resumé en anglais
The Boolean Satisfiability Problem is the problem of deciding if a given Boolean formula, such as (x1 ∨ x2 ∨ ¬x3) ∧ (¬x1) ∧ (x2 ∨ x3) is satisfiable, that is, if there is an assignment of True or False to the logical variables x1, x2 and x3 such that the formula evaluates to True. This was the first problem proved to be NP-complete, which means that there is no known algorithm that can solve it with a running time that scales polynomially with the problem size in a worst-case scenario. Here we study random Boolean formulas with fixed number of variables N and number of clauses M that are generated by choosing randomly the variables that appear in each clause and negating them with probability 1/2. We solve those formulas using a random-walk based, local search algorithm known as WalkSAT. We show that the WalkSAT can be used to study a remarkable property of the ensemble of random Boolean formulas – there is a critical value of the clauses-to-variables ratio M/N that separates satisfiable from unsatisfiable formulas in the limit of large N – and we characterize the critical region, or the sharpness of the transition, for finite N using finite-size scaling. From the perspective of computer science, this transition is important because satisfiable random formulas with the ratio M/N near the transition point are hard to solve, in the sense that WalkSAT requires much more time to find their solutions than in the case that ratio is far from the critical region. We show that a collective search strategy where several WalkSATs run in parallel and halt when one of them finds the solution results in a sub-linear speedup, that is, the speedup is less than the number of WalkSATs used in the collective search.

Titre en portugais
Estratégias de busca e transição de fase no problema da satisfatibilidade Booliana aleatório
Mots-clés en portugais
Algoritmos de busca local
Problema NP-completo
Problemas aleatórios
Transição de fase
Resumé en portugais