2-SAT: проверка выполнимости

Дано n булевых переменных (0..n-1) и список дизъюнктов clauses - каждый задаёт условие (литерал ИЛИ литерал), которое должно выполняться. Литерал кодируется числом: 2*i - переменная i истинна, 2*i+1 - переменная i ложна (то есть НЕ i). Верните true, если существует присваивание переменным, при котором ВСЕ дизъюнкты одновременно истинны. Классическое решение: постройте граф импликаций (¬a влечёт b и ¬b влечёт a для каждого дизъюнкта a∨b), найдите компоненты сильной связности (алгоритм Тарьяна) - формула выполнима тогда и только тогда, когда для каждой переменной её "истина" и "ложь" лежат в разных компонентах.