Na konferencii, kde som, maju hracku SAT solver. Video: http://lipa.ms.mff.cuni.cz/~stevko/sat_solver/sat_solver.webm

Mohli by sme nieco podobne vyrobit u nas?

Z videa a nazvu je snad jasne, co to robi, ale ak nie, tak popis:

Mame premenne, ktore mozeu byt true alebo false a prepiname im hodnotu prepinacmi. Stav premennej zobrazuje LEDka nad (true) alebo pod (false) prepinacom. Dalej mame klauzule, ktore su disjunkcia (OR) literalov (premenna alebo negacia). Ak je klauzula splnena aktualnym nastavenim premennych, tak svieti. Pod prepinacmi s premennymi je pocitadlo prepnuti - kolko krat sa prehodil niektory prepinac - a jeho resetovatko.

Cielom je rozsvietit (splnit vsetky klauzule), idealne v co najkratsom case.

Mohla by to byt aj pekna hracka na predvadzanie - ukazka, ze uz pri desiatich premennych je to sakra tazke a dlho to trva (hlavne ak vyberieme podobne hnusne klauzuly ako maju tam.

Stevko