Generating non-analytic cuts for boolean formulas with linear programming (2026)
- Authors:
- Autor USP: PEVIDOR, JOÃO FELIPE LOBO - IME
- Unidade: IME
- Sigla do Departamento: MAC
- DOI: 10.11606/D.45.2026.tde-01042026-180812
- Subjects: LÓGICA; PROGRAMAÇÃO INTEIRA E FLUXOS EM REDE; OTIMIZAÇÃO MATEMÁTICA; PROGRAMAÇÃO LINEAR
- Keywords: Aproximação de sistemas lógicos; Otimização; Programação inteira; Satisfabilidade booleana
- Language: Inglês
- Abstract: O problema da satisfatibilidade booleana (SAT) é o problema mais notório e o primeiro já descoberto a ser NP-Completo. Para resolvê-lo, os métodos mais avançados ainda dependem de técnicas que produzem um tempo de execução exponencial no pior caso. O objetivo deste trabalho é estudar métodos usados em problemas correlatos para abordar a resolução de uma instância do SAT de um ângulo diferente, que pode ser visto como a geração de cortes não analíticos apoiados por uma álgebra linear. Em particular, os métodos de programação linear obtiveram bons resultados ao lidar com um problema intimamente relacionado: o problema da satisfatibilidade em lógicas infinitamente valoradas. Com isso em mente, estudaremos o SAT original como um problema de otimização. Apresentamos uma nova maneira de gerar cortes não analíticos para uma fórmula booleana, resolvendo um problema de programação linear específico. A partir da solução linear, valores booleanos são extraídos e uma solução parcial é construída e evoluída até que um conflito seja detectado. Com o conflito, implementamos a aprendizagem de cláusulas para produzir uma nova cláusula. Também apresentamos um algoritmo completo de resolução de SAT projetado para aproveitar esse método, mostramos resultados de soundness (correção) e completude para ele e investigamos o seu desempenho empírico
- Imprenta:
- Data da defesa: 12.03.2026
- Status:
- Nenhuma versão em acesso aberto identificada
-
ABNT
PEVIDOR, João Felipe Lobo. Generating non-analytic cuts for boolean formulas with linear programming. 2026. Dissertação (Mestrado) – Universidade de São Paulo, São Paulo, 2026. Disponível em: https://teses.usp.br/teses/disponiveis/45/45134/tde-01042026-180812/. Acesso em: 11 abr. 2026. -
APA
Pevidor, J. F. L. (2026). Generating non-analytic cuts for boolean formulas with linear programming (Dissertação (Mestrado). Universidade de São Paulo, São Paulo. Recuperado de https://teses.usp.br/teses/disponiveis/45/45134/tde-01042026-180812/ -
NLM
Pevidor JFL. Generating non-analytic cuts for boolean formulas with linear programming [Internet]. 2026 ;[citado 2026 abr. 11 ] Available from: https://teses.usp.br/teses/disponiveis/45/45134/tde-01042026-180812/ -
Vancouver
Pevidor JFL. Generating non-analytic cuts for boolean formulas with linear programming [Internet]. 2026 ;[citado 2026 abr. 11 ] Available from: https://teses.usp.br/teses/disponiveis/45/45134/tde-01042026-180812/
Informações sobre a disponibilidade de versões do artigo em acesso aberto coletadas automaticamente via oaDOI API (Unpaywall).
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
