# 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)