| Campo Dublin Core | Valor | Língua |
|---|
| dc.contributor.advisor | Ribas, Bruno César | - |
| dc.contributor.author | Chaves, Felipe Borges de Souza | - |
| dc.identifier.citation | CHAVES, Felipe Borges de Souza. PluSAT: um resolvedor SAT modular. 2022. 41 f., il. Trabalho de Conclusão de Curso (Bacharelado em Engenharia de Software) — Universidade de Brasília, Brasília, 2022. | pt_BR |
| dc.description | Trabalho de Conclusão de Curso (graduação) — Universidade de Brasília, Faculdade UnB Gama, Engenharia de Software, 2022. | pt_BR |
| dc.description.abstract | Este trabalho apresenta um novo resolvedor SAT nomeado PluSAT, um resolvedor com estrutura modular e extensível que possibilita que seus usuários possam modificar o seu comportamento usando plugins. A estrutura interna do resolvedor é baseada em resolvedores CDCL (Conflict-Driven Clause Learning), nossa interface de extensão possibilita a alteração do comportamento de etapas como: heurística de decisão, retrocessos, BCP (Boolean Constraint Propagation), reinícios e análise de conflitos. A estrutura do PluSAT procura oferecer aos desenvolvedores de resolvedores uma forma rápida para implementar esse tipo de solução, enquanto aqueles interessados em iniciar seus estudos podem trabalhar em cada componente separadamente, sem se preocupar com todo o fluxo de um resolvedor comum diminuindo assim a curva de aprendizado necessária para implementar um resolvedor na prática. Toda implementação deste resolvedor está disponibilizada de forma open source. | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.subject.keyword | Lógica booleana | pt_BR |
| dc.subject.keyword | PluSAT | pt_BR |
| dc.title | PluSAT : um resolvedor SAT modular | pt_BR |
| dc.type | Trabalho de Conclusão de Curso - Graduação - Bacharelado | pt_BR |
| dc.date.accessioned | 2023-02-28T20:25:08Z | - |
| dc.date.available | 2023-02-28T20:25:08Z | - |
| dc.date.submitted | 2022-05-05 | - |
| dc.identifier.uri | https://bdm.unb.br/handle/10483/33934 | - |
| dc.language.iso | Português | pt_BR |
| dc.rights.license | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor que autoriza a Biblioteca Digital da Produção Intelectual Discente da Universidade de Brasília (BDM) a disponibilizar o trabalho de conclusão de curso por meio do sítio bdm.unb.br, com as seguintes condições: disponível sob Licença Creative Commons 4.0 International, que permite copiar, distribuir e transmitir o trabalho, desde que seja citado o autor e licenciante. Não permite o uso para fins comerciais nem a adaptação desta. | pt_BR |
| dc.description.abstract1 | This work presents a new SAT solver called PluSAT, a solver with a modular structure and pluggable, that makes possible to users change solver behavior without implement all features necessary to create a SAT solver. The internal structure of this solver is based on CDCL (Conflict-Driven Clause Learning), our interface makes possible to change: branch-heuristic, conflict solving, BCP (Boolean Constraint Propagation) and restarts. This architecture seek to provide to developers a fast way to implement kind of algorithm, while newbies can understand what a SAT solver is and can work in each component individually without paying to much attention in all steps that a solver needs to do in the first place. All implementation of PluSAT are open source. | pt_BR |
| Aparece na Coleção: | Engenharia de Software
|
