2R-SAT
Napsal: 17. 1. 2011 14:05
Zdravim,
koukal jsem, ze se tady na foru resil 2R-SAT, trochu jsem to hledal a prijde mi velmi srozumitelne toto reseni:
http://www.cc.gatech.edu/classes/AY2008 ... rsions.pdf - str. 3
Rezoluce se vyklada treba na Umele Inteligenci (UI) nebo na log. programku. Uplny a korektni algoritmus vykladany na UI generuje z klazuli pomoci rezoluce vsech moznych kombinaci dvou klazuli a ceka se, az se tento proces ustali.
Asi by to chtelo jeste argument, ze kdyz mam promenne x a y a pro obe bych mohl provest rezoluci ve dvou klauzulich, tak je jedno, pro kterou to provedu drive. Provedu-li rezoluci pro x, tak dostanu klauzuli, ve ktere bude obsazeno: y v -y .. a tuto klauzuli teda mohu v nasledujicim kroku odebrat jako splnitelnou.
koukal jsem, ze se tady na foru resil 2R-SAT, trochu jsem to hledal a prijde mi velmi srozumitelne toto reseni:
http://www.cc.gatech.edu/classes/AY2008 ... rsions.pdf - str. 3
Rezoluce se vyklada treba na Umele Inteligenci (UI) nebo na log. programku. Uplny a korektni algoritmus vykladany na UI generuje z klazuli pomoci rezoluce vsech moznych kombinaci dvou klazuli a ceka se, az se tento proces ustali.
Asi by to chtelo jeste argument, ze kdyz mam promenne x a y a pro obe bych mohl provest rezoluci ve dvou klauzulich, tak je jedno, pro kterou to provedu drive. Provedu-li rezoluci pro x, tak dostanu klauzuli, ve ktere bude obsazeno: y v -y .. a tuto klauzuli teda mohu v nasledujicim kroku odebrat jako splnitelnou.