Rectangle puzzle és automatikus tételbizonyítás
Dátum
Szerzők
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.