Никого не трогаю, смотрю доклад по пакетной системе #opkg из #OpenEmbedded . И внезапно оттуда начинает изливаться #МАТАН: задача выполнимости булевых формул (SAT), NP-полная задача, conflict-driven clause learning. Радостно!