slococo-uni
/
bssolver
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
Bottler Sat Solver
16 Commits 1 Branch 0 Tags 62 KiB
C 92.5%
Makefile 4%
Shell 3.5%
Go to file
Santiago Lo Coco 28ec64d07e
Update LICENSE.md 		2022-04-02 07:38:19 -03:00
include Update Makefile and create src folder 2021-11-09 23:50:10 -03:00
src Update Makefile and create src folder 2021-11-09 23:50:10 -03:00
LICENSE.md Update LICENSE.md 2022-04-02 07:38:19 -03:00
Makefile Update Makefile and create src folder 2021-11-09 23:50:10 -03:00
README.md Make the last changes 2021-09-11 13:21:50 -03:00
valAnalysis.sh Fix a minor bug and tidy up the code... 2021-09-12 21:15:00 -03:00

README.md

BSSolver

BSSolver (Bottler Sat Solver) es un sistema que resuelve múltiples fórmulas proposicionales en CNF de forma distribuida.

Table de contenidos

Requisitos

Debe instalar minisat. Este se encuentra disponible en el repositorio de la vasta mayoría de distribuciones de Linux/macOS.

Debian/Ubuntu: apt install minisat
macOS (con homebrew): brew install minisat

Si tiene otra distribución consulte cómo hacerlo. De todos modos, puede construirlo desde la fuente.

Compilación

Para compilar todos los archivos se debe hacer:

make all

Ejecución

Ahora, tendrá dos ejecutables: view y solve.

Para ejecutar el programa que se encarga de resolver usted debe pasarle los archivos CNF como parámetros.

./solve $(CNF_FILES)

Este enviará por salida estándar la cantidad de archivos a resolver y su PID, los cuales son necesarios para el programa view. Por lo tanto, usted tiene dos posibles modos de uso del sistema:

  1. Enviar el output de solve directamente a view (con el uso de pipes):
./solve $(CNF_FILES) | ./view
  1. Correr primero solve y luego en otra terminal (o en la misma si se corrió en background) ejecutar view pasándole como argumentos la cantidad de archivos y el PID.
./solve $(CNF_FILES)

./view $(TOTAL_FILES) $(PID)
  1. No correr el proceso view.

Debe notar que en todos los casos se escribirá el output un archivo llamado ouputFile.txt.

Además, dispondrá de 5 segundos para correr el programa view.

Testeos

En orden de realizar un análisis estático del sistema usted debe tener instalado cppcheck y pvs-studio. Luego, puede correrlos con:

make test

Por último, si quiere hacer un análisis dinámico (usando valgrind) debe ejecutar el programa valAnalysis.sh pasandole como argumento la carpeta con los archivos .cnf o directamente los archivos:

./valAnalysis.sh $(CNF_FILES)

Autores

  • Barmasch, Juan Martín (61033)
  • Bellver, Ezequiel (61268)
  • Lo Coco, Santiago (61301)