PluSAT1 é um SAT solver extensível simples, foi desenvolvido como projeto de TCC do, então, estudante Felipe Borges.
O principal objetivo do PluSAT é permitir que pessoas, enquanto aprendem sobre SAT Solvers, tenham a capacidade de implementar as principais funções de um Solver, sem a necessidade de se preocupar com a estrutura de dados inicial e nem com o parser da fórmula, permitindo, assim, um ambiente honesto para realização de benchmark de várias ideias.
Para este problema o seu objetivo é efetuar o clone do repositório2 do PluSAT e desenvolver um novo plugin de processamento.
O plugin básico está disponível no diretório src/plugin/simple.c, que contém o esqueleto
básico das funções que devem ser desenvolvidas, sendo elas:
PreProcessingDecideBCPresolveConflictO principal foco, neste exercício específico, é avaliar o
desenvolvimento de um BCP mais eficiente,
bem como a implementação de alguma heurística, mesmo que simples, para a
função de decisão Decide.
O processo de retrocesso, pela função resolveConflict, pode permanecer o padrão, que é
o processo do DPLL padrão.
A função de PreProcessing também pode
permanecer sem instrução. No entanto, você pode utilizar a função de
pré-processamento para realizar algum trabalho em cima da estrutura de
dados como, por exemplo, copiar a fórmula para uma estrutura mais
eficiente que a fornecida, bem como iniciar a estrutura de literais
observados.
A entrada para o problema será sempre uma fórmula CNF no padrão DIMACS. Você pode baixar as fórmulas do benchmark SATLIB3, comece pelas fórmulas Uniform Random-3-SAT, teste tanto fórmulas SAT como UNSAT.
A saída deve ser a informação de que a fórmula é SAT ou UNSAT e uma linha contendo o modelo da fórmula.
O formato de saída é o que o PluSAT gera, mas talvez seja necessário um patch para se adequar ao ambiente da competição SAT. O patch contendo esta modificação dará +10 pontos para o grupo que o fizer.
Você deverá submeter um único arquivo contendo as 4 funções do plugin. Este arquivo será compilado como um plugin do PluSAT.