slococo-uni
/
bssolver
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
Bottler Sat Solver
10 Commits 1 Branch 0 Tags 62 KiB
C 92.5%
Makefile 4%
Shell 3.5%
Go to file
Santiago Lo Coco 2ff817394d Create a more modularized code 
Co-authored-by: Ezequiel Bellver <ebellver@itba.edu.ar>
Co-authored-by: Juan Barmasch <jbarmasch@itba.edu.ar>
 		2021-09-10 20:47:36 -03:00
Makefile Create a more modularized code 2021-09-10 20:47:36 -03:00
README.md Create a more modularized code 2021-09-10 20:47:36 -03:00
error.c Create a more modularized code 2021-09-10 20:47:36 -03:00
error.h Add master (with pipes working) and change slave printing (and reading) 2021-09-04 09:36:00 -03:00
master.c Create a more modularized code 2021-09-10 20:47:36 -03:00
master.h Create a more modularized code 2021-09-10 20:47:36 -03:00
shr_mem.c Create a more modularized code 2021-09-10 20:47:36 -03:00
shr_mem.h Create a more modularized code 2021-09-10 20:47:36 -03:00
siglib.c Create a more modularized code 2021-09-10 20:47:36 -03:00
siglib.h Create a more modularized code 2021-09-10 20:47:36 -03:00
slave.c Create a more modularized code 2021-09-10 20:47:36 -03:00
view.c Create a more modularized code 2021-09-10 20:47:36 -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.

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 los testeos usted debe tener instalado valgrind, cppcheck y pvs-studio. Luego, puede correr los testeos con:

make test

Autores

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