Rectangle puzzle és automatikus tételbizonyítás

Dátum
2013-06-07T08:55:18Z
Folyóirat címe
Folyóirat ISSN
Kötet címe (évfolyam száma)
Kiadó
Absztrakt

A Rectangle puzzle ember által viszonylag könnyen, azonban számítógéppel nehezen megoldható. Éppen ezért a mesterséges intelligencia területén már bevált módszereket alkalmazzuk: az automatikus tételbizonyítást, a kényszer-kielégítést és a visszalépéses keresőt. Ezek segítségével az egyébként exponenciálisan növekvő keresési tér, nagy mértékben leszűkíthető. A kényszereknek eleget nem tévő állapotok nem vezethetnek megoldáshoz, éppen ezért elhagyjuk őket a további keresés során. A visszalépéses kereső használatával az állapottérhez tartozó teljes keresési fát végigjárjuk, közben levágva a kényszerek által elhagyásra ítélt ágakat. Ezzel nem csak egy, hanem az összes megoldáshoz eljutunk. Ugyanakkor, ha a probléma egyértelműen megoldható, akkor a visszalépéses keresésre nincs is szükség. Önmagukban a kényszerek meghatározzák a megoldást.

Leírás
Kulcsszavak
automatikus tételbizonyítás, kényszer-kielégítés
Forrás