SAT e SMT solvers: fundamentos e aplicação ao problema de alocação de frequências (2019)
- Authors:
- Autor USP: CARVALHO, YURI CASTRO NEO DE - EESC
- Unidade: EESC
- Subjects: ALGORITMOS; ENGENHARIA ELÉTRICA; LÓGICA
- Keywords: Frequency assignment problem; Logic; Lógica; Problema de alocação de frequências; SAT; SMT; Z3
- Language: Português
- Abstract: O problema da satisfatibilidade booleana (Boolean Satisfiability, ou simplesmente SAT) é decidir se existe alguma interpretação para uma dada fórmula booleana de maneira que avaliação da fórmula seja verdadeiro. Desde seus primeiros algoritmos na década de 1960, os SAT solvers evoluíram muito, não só incorporando conceitos como aprendizado, mas também permitindo representações mais compactas e expressivas com o uso de solvers específicos para uma dada teoria, conhecido como Satisfiability Modulo Theories (SMT). Antes restritos a apenas algumas centenas de variáveis, SAT e SMT solvers alcançaram capacidade de lidar com problemas industriais, lidando com milhões de variáveis e restrições. Possuem aplicações práticas em diversas áreas como Electronic Design Automation (EDA), Verificação, Inteligência Artificial e Pesquisa Operacional. O presente trabalho fornece o embasamento teórico de lógica e a evolução dos principais algoritmos até atingir o estado-da-arte. No contexto de uma aplicação militar, existe o problema de se alocar frequências para pares de links de rádios (RLFAP), de maneira que as interferências sejam evitadas. Neste trabalho, o problema de RLFAP foi abordado utilizando-se com sucesso o Z3 SMT Solver da Microsoft e um conhecido conjunto de dados construído a partir de redes reais e fornecido pelo CELAR (Centro de Eletrônica do Exército Francês)
- Imprenta:
- Publisher place: São Carlos
- Date published: 2019
-
ABNT
CARVALHO, Yuri Castro Neo de. SAT e SMT solvers: fundamentos e aplicação ao problema de alocação de frequências. 2019. Trabalho de Conclusão de Curso (Graduação) – Escola de Engenharia de São Carlos, Universidade de São Paulo, São Carlos, 2019. Disponível em: https://bdta.abcd.usp.br/directbitstream/243e4a7e-cd01-41a1-a70b-723a55c666fd/Carvalho_Yuri_Castro_tcc.pdf. Acesso em: 22 mar. 2025. -
APA
Carvalho, Y. C. N. de. (2019). SAT e SMT solvers: fundamentos e aplicação ao problema de alocação de frequências (Trabalho de Conclusão de Curso (Graduação). Escola de Engenharia de São Carlos, Universidade de São Paulo, São Carlos. Recuperado de https://bdta.abcd.usp.br/directbitstream/243e4a7e-cd01-41a1-a70b-723a55c666fd/Carvalho_Yuri_Castro_tcc.pdf -
NLM
Carvalho YCN de. SAT e SMT solvers: fundamentos e aplicação ao problema de alocação de frequências [Internet]. 2019 ;[citado 2025 mar. 22 ] Available from: https://bdta.abcd.usp.br/directbitstream/243e4a7e-cd01-41a1-a70b-723a55c666fd/Carvalho_Yuri_Castro_tcc.pdf -
Vancouver
Carvalho YCN de. SAT e SMT solvers: fundamentos e aplicação ao problema de alocação de frequências [Internet]. 2019 ;[citado 2025 mar. 22 ] Available from: https://bdta.abcd.usp.br/directbitstream/243e4a7e-cd01-41a1-a70b-723a55c666fd/Carvalho_Yuri_Castro_tcc.pdf
Download do texto completo
| Tipo | Nome | Link | |
|---|---|---|---|
 |
Carvalho_Yuri_Castro_tcc.... | Direct link |
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
