<commit_before># LVR_team5

## <NAME>

### team5_sat_solver
Modul team5_sat_solver vsebuje ogrodje za kontrukcijo in obravnavo logičnih izrazov izjavnega računa. Priložen je reševalnik problema SAT in nekaj primerov prevedb znanih problemov na SAT.
Zavoljo čiste vesti so dodani tudi enotski testi.

### Algoritem
Uporabili smo algoritem [DPLL](https://en.wikipedia.org/wiki/DPLL_algorithm) (Davis–Putnam–Logemann–Loveland).
Algoritem smo nadgradili s sortiranjem  seznama stavkov po velikosti (krajše stavke obdelamo prej) na vsakem koraku in z absorbcijo ponavljajočih se podizrazov.

### Datoteke
V modulu boste našli naslednje datoteke:
- **cnf.py** - vsebuje metodo za pretvorbo poljubnega izraza v konjuktivno normalno obliko in ostale sorodne metode,
- **dpll.py** - vsebuje algoritem DPLL in sorodne metode,
- **operands.py** - razredi za delo z logičnimi izrazi (konjunkcija, disjunkcija itd.),
- **preveba_coloring.py** - prevedba problema barvanja grafa na problem SAT,
- **preveba_hadamard.py** - prevedba problema [Hadamardove matrike](https://en.wikipedia.org/wiki/Hadamard_matrix) na problem SAT,
- **preveba_sudoku.py** - prevedba problema rešvanje zagonetenke *sudoku* na problem SAT,
- **primeri_uporabe.py** - (**TO JE ZANIMIVO**) demonstracija uporabe celotnega projekta, uporabljena večina funkcij iz vseh modulov, dodani so tudi izpisi, ki prikazujejo potek izvajanja programa. Notri so tudi primerjave optimiziranih in neoptimiziranih procedur (npr. prevedbe in resevanja Hadamardove matrike).
- **simplify.py** - metode za poenostavljanje logičnih izrazov,
- **UnitTests.py** - enotski testi,
- **utils.py** - pomožne metode, štoparica za merjenje izvajalnih časov.
               
Pri razvoju smo uporabljali python 2.7.5.
Zunanje odvisnosti: unittest, time, itertools (vse priloženo pythonu).

Spodnja slika prikazuje graf medsebojnih odvisnosti zgoraj navedenih datotek.

![Graf dependecyjev](http://imgur.com/RvuqM2x)

### Uporaba
Glej **primeri_uporabe.py**. Na kratko: gradimo poljuben izraz  z operands ali pa uporabimo eno od prevedb; dobljeno formulo lahko nato obdelujemo z metodami iz cnf.py, simplify.py ali pa preprosto poženemo algoritem iz dpll.py, da dobimo rešitev problema SAT (za dano formulo).
<commit_msg>Popravek linka na graf dependencyjev.<commit_after># LVR_team5

## Jani, Jaka

### team5_sat_solver
Modul team5_sat_solver vsebuje ogrodje za kontrukcijo in obravnavo logičnih izrazov izjavnega računa. Priložen je reševalnik problema SAT in nekaj primerov prevedb znanih problemov na SAT.
Zavoljo čiste vesti so dodani tudi enotski testi.

### Algoritem
Uporabili smo algoritem [DPLL](https://en.wikipedia.org/wiki/DPLL_algorithm) (Davis–Putnam–Logemann–Loveland).
Algoritem smo nadgradili s sortiranjem  seznama stavkov po velikosti (krajše stavke obdelamo prej) na vsakem koraku in z absorbcijo ponavljajočih se podizrazov.

### Datoteke
V modulu boste našli naslednje datoteke:
- **cnf.py** - vsebuje metodo za pretvorbo poljubnega izraza v konjuktivno normalno obliko in ostale sorodne metode,
- **dpll.py** - vsebuje algoritem DPLL in sorodne metode,
- **operands.py** - razredi za delo z logičnimi izrazi (konjunkcija, disjunkcija itd.),
- **preveba_coloring.py** - prevedba problema barvanja grafa na problem SAT,
- **preveba_hadamard.py** - prevedba problema [Hadamardove matrike](https://en.wikipedia.org/wiki/Hadamard_matrix) na problem SAT,
- **preveba_sudoku.py** - prevedba problema rešvanje zagonetenke *sudoku* na problem SAT,
- **primeri_uporabe.py** - (**TO JE ZANIMIVO**) demonstracija uporabe celotnega projekta, uporabljena večina funkcij iz vseh modulov, dodani so tudi izpisi, ki prikazujejo potek izvajanja programa. Notri so tudi primerjave optimiziranih in neoptimiziranih procedur (npr. prevedbe in resevanja Hadamardove matrike).
- **simplify.py** - metode za poenostavljanje logičnih izrazov,
- **UnitTests.py** - enotski testi,
- **utils.py** - pomožne metode, štoparica za merjenje izvajalnih časov.
               
Pri razvoju smo uporabljali python 2.7.5.
Zunanje odvisnosti: unittest, time, itertools (vse priloženo pythonu).

Spodnja slika prikazuje graf medsebojnih odvisnosti zgoraj navedenih datotek.

[Graf dependecyjev](http://imgur.com/RvuqM2x)

### Uporaba
Glej **primeri_uporabe.py**. Na kratko: gradimo poljuben izraz  z operands ali pa uporabimo eno od prevedb; dobljeno formulo lahko nato obdelujemo z metodami iz cnf.py, simplify.py ali pa preprosto poženemo algoritem iz dpll.py, da dobimo rešitev problema SAT (za dano formulo).

{'fraction_non_alphanumeric': 0.08416169648774023, 'fraction_numerical': 0.0030925557764523966, 'mean_word_length': 5.127198917456021, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 4, 'https://': 4, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7069511', 'n_tokens_mistral': 1831, 'n_tokens_neox': 1781, 'n_words': 503}