T-79.194 Tietojenkäsittelyteorian seminaari

Kevät 2003

Kokeellinen osuus

Yleistä

Testeihin käytettävä kone on tt-dhcp-89.tt.hut.fi, johon teille on luotu käyttäjätunnukset.

Konetta ylläpitää Matti Järvisalo (mjj@tcs.hut.fi), jonka puoleen voi kääntyä ongelmatapauksissa.

Kokeet

Tavoitteena on testata tutkittavaa järjestelmää ainakin seuraavilla testitapauksilla:

Satunnaiset 3-SAT -ongelmat:
Käytetään testitapausten generointiin MakeWFF-ohjelmaa (ks. alla). Tavoitteena selvittää, kuinka suuret tapaukset (montako atomia) saadaan ratkaistua "luotettavasti kohtuullisessa ajassa'' faasimuutospisteessä.
Tekijöihinjako:
Käytetään testitapausten generointiin genfacbm-ohjelmaa (ks. alla) ja braun-piirejä. Tavoitteena selvittää, kuinka iso luku (montako bittiä/width) saadaan jaettua tekijöihin/osoitettua alkuluvuksi ``luotettavasti kohtuullisessa ajassa''.
Käytännön esimerkit
Mitkä valmiista mallintarkastustapauksista (ks. alla) tutkittava järjestelmä pystyy ratkaisemaan ``luotettavasti kohtuullisessa ajassa''?

Näiden lisäksi voi käyttää testitapauksina esim. jotain kirjallisuudessa esitettyä testiä. Tällainen ylimääräinen työ vaikuttaa tietysti positiivisesti arvosanaan.

Vastaanotot

Kokeelliseen osaan liittyen järjestetään viikoilla 7-9 vastaanottotunti (ks. alla), jossa voi saada apua kokeellisen osuuden tekemisessä esiin tulleisiin ongelmiin.

to 13.2. klo 11.30-12.30
to 20.2. klo 12-13
to 27.2. klo 12-13
to 6.3. klo 12-14: Yhteenvetotilaisuus, jossa esitellään lyhyesti koetulokset (ei vaikuta arvosteluun)

Käytännön ohjeita

Toteutuvuustarkistimet löytyvät polusta /lhome/solvers/ ja instanssigeneraattorit polusta /lhome/generators/. Kaikki tarvittavat ohjelmistot (tarkistimet zchaff, 2clseq, sp ja unitwalk, sekä generaattorit makewff, genfacbm ja okgenerator) on linkattu polkuun /lhome/bin/. Tämä hakemisto on lisätty käyttäjätunnuksienne PATH-muuttujaan, joten ohjelmien pitäisi toimia sellaisenaan komentoriviltä.

SAT-instanssien syötemuoto DIMACS

Käytettävien toteutuvuustarkistimien syötemuoto on ns. DIMACS-muoto. Esimerkki DIMACS-muotoisesta instanssista:

c kommentti
p cnf 5 7
-1 3 2 0
4 -3 5 1 0
2 5 0
-5 4 2 0
 1 0
1 4 -5 0
3 -4 0

Kirjaimella c alkavat rivit ovat siis kommenttirivejä (tarkastin ei huomioi näitä). Kirjaimella p alkava rivi yllä kertoo, että instanssi on konjunktiivisessa normaalimuodossa (cnf), ja että instanssissa on viisi (5) muuttujaa ja seitsemän (7) klausuulia. Tämän jälkeen tulevat rivit vastaavat klausuuleja; jokaista muuttujaa vastaa tietty kokonaisluku välillä 1 - 5, ja miinus-merkki muuttujan edessä vastaa negaatiota. Nolla-merkki kertoo rivin loppumisesta.

SAT-instanssit

Valmiit instanssit

Tavoitteena on tarkistaa 13 mallintarkastusinstanssin toteutuvuus. Instanssit löytyvät polusta /lhome/instances/bmc/.

SAT-instanssien generointi

MakeWFF

Satunnaisten k-SAT -instanssien luontiin. Käyttö:
```
makewff -cnf k v c
```
missä v = muuttujien määrä ja c = klausuulien määrä. Esimerkiksi
```
makewff -cnf 3 100 420
```
luo 3-SAT -instanssin, jossa 100 muuttujaa ja 420 klausuulia
genfacbm

Luo kokonaislukufaktorointi-instansseja. Käyttö:
```
genfacbm dimacs [sat|unsat] [atree|braun] width seed
```
missä atree ja braun ovat kaksi erilaista faktorointipiirivaihtoehtoa, sat optiolla faktoroinnin kohteeksi valitaan kahden alkuluvun tulo ja unsat optiolla faktoroinnin kohteeksi valitaan alkuluku, width on faktoroitavan kokonaisluvun bittiesityksen bittimäärä, ja seed määrää sen, mikä mahdollisista faktoroinnin kohteista valitaan faktoroitavaksi.

Ylimääräistä

Yleisesti käytettyjä testi-instansseja löytyy muun muassa Satlib:stä, http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/benchm.html

OKGenerator luo satunnaisia SAT-instansseja pohjautuen AES128:aan (128-bittiseen Advanced Encryption Standardiin eli Rjindael-lohkosalaimeen). Käyttö: kokeile komentoa okgenerator -h, kts. lisäksi /lhome/generators/OKRandGen1_3/Documentation/ -hakemiston tiedostoja Usage ja Examples.

Kokeet käytännössä

Kokeiden automatisointiin ja tulosten tarkistamiseen pitää kirjoittaa luultavasti lyhyehkö skripti. Käytettävän kielen jokainen saa valita vapaasti (esim. bash, Perl, C, ...). Mikään skriptiguru ei kuitenkaan tarvitse olla selvitäkseen kokeista.
Tarkista, että toteutuvaksi väitetty instanssi on tosiaan toteutuva, ja että toteutumaton on tosiaan toteutumaton
Käytä sopivaa prioriteettia kokeita tehdessäsi, eli nice -komentoa (nice -n 19 ajoskripti), jotta työaseman yhteiskäyttö sujuu mahdollisimman jouhevasti
Käytä ajoaikojen määrittämiseen komentoa /usr/bin/time -f "%U", eli esim. /usr/bin/time -f "%U" zchaff cnf_tiedosto (huomaa, että /usr/bin/time ei ole sama kuin pelkkä time !)
Kokeiden pitäisi olla täysin toistettavissa; tallenna siis ajoaikojen, käytettyjen muuttuja- ja klausuulimäärien lisäksi myös instanssien generointiin käytetyt siemenluvut yms.
Kätevä työkalu kuvaajien luomiseen on gnuplot

Linkkejä

Perl
- Practical Perl Programming
- Hyvä, käytännönläheinen peruskirja: Learning Perl
Bash
- Advanced Bash-Scripting Guide
- BASH Programming - Introduction HOW-TO
GNUPlot
- GNUPLOT - A Brief Manual and Tutorial