diff --git a/README.md b/README.md new file mode 100644 index 0000000..7c41879 --- /dev/null +++ b/README.md @@ -0,0 +1,62 @@ +# BSSolver + +BSSolver (Bottler Sat Solver) es un sistema que resuelve múltiples fórmulas proposicionales en CNF +de forma distribuida. + + +## 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](https://brew.sh/)): `brew install minisat` + +Si tiene otra distribución consulte cómo hacerlo. + +## Compilación + +Para compilar todos los archivos se debe hacer: + +```bash +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. + +```bash +./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): + +```bash +./solve $(CNF_FILES) | ./view +``` + +2) 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. + +```bash +./solve $(CNF_FILES) +``` +```bash +./view $(TOTAL_FILES) $(PID) +``` +Debe notar que dispondrá de 5 segundos para correr el programa `view`. + +## Test + +En orden de realizar los testeos usted debe tener instalado [valgrind](https://valgrind.org/), [cppcheck](http://cppcheck.net/) y [pvs-studio](https://pvs-studio.com/). Luego, puede correr los testeos con: + +```bash +make test +``` + +# Autores +- Barmasch, Juan Martín (61033) +- Bellver, Ezequiel (61268) +- Lo Coco, Santiago (61301)