Tik-79.154 Logiikka tietotekniikassa: erityiskysymyksiä II

syksy 1997


Harjoitustyöohje

I. YLEISTÄ

Kukin kurssilainen saa oman tehtävän.

Annettu tehtävä ratkaistaan kahdella tavalla:

  1. lauselogiikan toteutuvuusongelmana ja
  2. logiikkaohjelman stabiilin mallien löytämisongelmana.
Tätä varten tehdään käännös tehtävästä
  1. toisaalta lauselogiikkaan siten, että käännöksen mallit vastaavat hyväksyttäviä ratkaisuja tehtävälle ja
  2. toisaalta logiikkaohjelmiin siten, että logiikkaohjelman stabiilit mallit vastaavat hyväksyttäviä ratkaisuja
Sitten haetaan tehtävään ratkaisu käyttäen lauselogiikan ja logiikkaohjelmien toteutuksia. Käännettäessä tehtävää lauselogiikan lauseiksi voi apuna käyttää satplan-ohjelmisto.

Kukin kurssilainen pitää lyhyen (15min) esityksen harjoitustyöstään ti 2.12.1997 klo 14-17.

Hyväksytty harjoitustyö edellyttää kirjallista työselostusta, jossa kuvataan laaditut käännökset ja löydetyt ratkaisut sekä annetaan ajoesimerkit niin, että on periaatteessa mahdollista toistaa tehty ratkaisu. Ratkaisuna tehdyt ajoesimerkit palautetaan myös sähköisessä muodossa siten, että tehtävien tarkastuksen yhteydessä on mahdollista suorittaa tietokoneajoja.

Arvosanaan nostavasti vaikuttavat esim.

Harjoitustyön viimeinen palautuspäivä on pe 12.12.1997.

Harjoitustyö arvostellaan kirjallisen työselostuksen pohjalta. Harjoitustyön arvosanalla voi olla korottava vaikutus kurssin arvosanaa: jos harjoitustyön arvosana on korkeampi kuin tentistä saatu, opintojakson arvosanaksi tulee tentinarvosana korotettuna yhdellä (ei kuitenkaan koske tentin arvosanoja 0 ja 5).

II. TARJOLLA OLEVIA OHJELMISTOJA

Olemme asentaneet harjoitustyön tekemiseen riittävän ohjelmiston LK:n hp-työasemiin ("puut": palisanteri, palmu, pihlaja, ...) Tarjolla on Binaarit löytyvät hakemistosta ~psimons/satplan/system/bin ja käyttöohjeita hakemistosta ~psimons/satplan/doc

Ohjelmistojen käyttö edellyttää polkunimien hoitamista kuntoon. Esim. bash:ia käytettäessä tarvitaan määrittelyt:

SATPLAN=~psimons/satplan/system
export SATPLAN
PATH=$SATPLAN/bin:$PATH

Muille komentotulkeille löytyy ohjeita tiedostosta ~psimons/satplan/README.

III. HARJOITUSTYÖN TEKEMINEN MUILLA KONEILLA

satplan, walksat, ntab ja smodels -ohjelmistoista on käytössä lähdekoodi, joten niiden asentaminen periaatteessa ei ole kovin vaikeaa jos käytössä on normaalit Unix-työkalut: make, gcc, awk, perl, ...
(Huom! ntab ei ole kirjoitettu kovin kannettavasti ja sen asentaminen 64-bittiseen arkkitehtuuriin näyttää hankalalta).

Seuraavassa ohjeita ohjelmien asentamiseen (kun käytössä on normaalit gnu-työkalut).


Ota yhteyttä Ilkka.Niemela@hut.fi tai Patrik.Simons@hut.fi, jos eteen tulee ongelmia tai kysymyksiä.