79 lines
2.3 KiB
Markdown
79 lines
2.3 KiB
Markdown
# BSSolver
|
|
|
|
BSSolver (Bottler Sat Solver) es un sistema que resuelve múltiples fórmulas proposicionales en CNF
|
|
de forma distribuida.
|
|
|
|
## Table de contenidos
|
|
* [Requisitos](#requisitos)
|
|
* [Compilación](#compilación)
|
|
* [Ejecución](#ejecución)
|
|
* [Testeos](#tests)
|
|
|
|
## Requisitos <a name="requisitos"></a>
|
|
|
|
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. De todos modos, puede construirlo desde la [fuente](https://github.com/niklasso/minisat).
|
|
|
|
## Compilación <a name="compilación"></a>
|
|
|
|
Para compilar todos los archivos se debe hacer:
|
|
|
|
```bash
|
|
make all
|
|
```
|
|
|
|
## Ejecución <a name="ejecución"></a>
|
|
|
|
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)
|
|
```
|
|
|
|
3) 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 <a name="tests"></a>
|
|
|
|
En orden de realizar un análisis estático del sistema usted debe tener instalado [cppcheck](http://cppcheck.net/) y [pvs-studio](https://pvs-studio.com/). Luego, puede correrlos con:
|
|
|
|
```bash
|
|
make test
|
|
```
|
|
|
|
Por último, si quiere hacer un análisis dinámico (usando [valgrind](https://valgrind.org/)) debe ejecutar el programa `valAnalysis.sh` pasandole como argumento la carpeta con los archivos `.cnf` o directamente los archivos:
|
|
|
|
```bash
|
|
./valAnalysis.sh $(CNF_FILES)
|
|
```
|
|
|
|
# Autores
|
|
- Barmasch, Juan Martín (61033)
|
|
- Bellver, Ezequiel (61268)
|
|
- Lo Coco, Santiago (61301)
|