• JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
 
  Bookmark and Share
 
 
Dissertação de Mestrado
DOI
https://doi.org/10.11606/D.76.2021.tde-02092021-162034
Documento
Autor
Nome completo
Heitor Pascoal de Bittencourt
E-mail
Unidade da USP
Área do Conhecimento
Data de Defesa
Imprenta
São Carlos, 2021
Orientador
Banca examinadora
Fontanari, Jose Fernando (Presidente)
Gomes, Paulo Freitas
Rosas, Alexandre da Silva
Título em inglês
Search strategies and phase transition in the Random Boolean satisfiability problem
Palavras-chave em inglês
Boolean satisfiability problem
Local search algorithms
NP-complete problem
Phase transitions
Random problems
Resumo em inglês
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.
Título em português
Estratégias de busca e transição de fase no problema da satisfatibilidade Booliana aleatório
Palavras-chave em português
Algoritmos de busca local
Problema de satisfatibilidade booliana
Problema NP-completo
Problemas aleatórios
Transição de fase
Resumo em português
O problema da satisfatibilidade booliana é o problema de decidir se uma determinada fórmula booliana, como (x1 ∨ x2 ∨ ¬x3) ∧ (¬x1) ∧ (x2 ∨ x3) é satisfatível, ou seja, se há uma atribuição de True ou False às variáveis lógicas x1, x2 e x3 de modo que a fórmula seja avaliada como True. Este foi o primeiro problema provado ser NP-completo, o que significa que não há algoritmo conhecido que pode resolvê-lo com um tempo de execução que escale polinomialmente com o tamanho do problema em um cenário de pior caso. Nessa dissertação, estudamos fórmulas boolianas aleatórias com número fixo de variáveis N e número de cláusulas M que são geradas escolhendo aleatoriamente as variáveis que aparecem em cada cláusula e negando-as com probabilidade 1/2. Resolvemos essas fórmulas usando um algoritmo de busca local baseado em passeio aleatório conhecido como WalkSAT. Mostramos que o WalkSAT pode ser usado para estudar uma propriedade notável do conjunto de fórmulas boolianas aleatórias – há um valor crítico da razão entre cláusulas e variáveis M/N que separa as fórmulas satisfatíveis das insatisfatíveis no limite de N grande – e caracterizamos a região crítica, ou a agudeza da transição, para N finito usando a teoria de escala de tamanho finito. Do ponto de vista da ciência da computação, essa transição é importante porque fórmulas aleatórias satisfatíveis com a razão M/N perto do ponto de transição são difíceis de resolver, no sentido que o WalkSAT requer muito mais tempo para encontrar suas soluções do que no caso em essa razão está longe da região crítica. Mostramos que uma estratégia de busca coletiva onde vários WalkSATs rodam em paralelo e param quando um deles encontra a solução resulta em um aumento sublinear da velocidade da busca, ou seja, o aumento de velocidade é menor do que o número de WalkSATs usados na busca coletiva.
 
AVISO - A consulta a este documento fica condicionada na aceitação das seguintes condições de uso:
Este trabalho é somente para uso privado de atividades de pesquisa e ensino. Não é autorizada sua reprodução para quaisquer fins lucrativos. Esta reserva de direitos abrange a todos os dados do documento bem como seu conteúdo. Na utilização ou citação de partes do documento é obrigatório mencionar nome da pessoa autora do trabalho.
Data de Publicação
2021-09-06
 
AVISO: Saiba o que são os trabalhos decorrentes clicando aqui.
Todos os direitos da tese/dissertação são de seus autores
CeTI-SC/STI
Biblioteca Digital de Teses e Dissertações da USP. Copyright © 2001-2021. Todos os direitos reservados.