Про всякую логику.

[thesz]

Тут zelych занимается решением логических уравнений. Он сделал преобразования Цейтина, и из таблички умеренного размера (100К строк с ограничениями) получил очень большую КНФ в полтора миллиона дизъюнктов.

По идее, можно справиться лучше.

Сперва код:
import Data.Bits

import Debug.Trace

data E = F | T | B Int E E
deriving (Eq, Ord, Show)

true = T
false = F

var v = B v F T

eToCNF :: E -> [[Int]]
eToCNF e = case e of
F -> [[]]
T -> []
B v a b -> map (v:) (eToCNF a) ++ map ((-v):) (eToCNF b)

andE F _ = F
andE T b = b
andE a F = F
andE a T = a
andE x@(B v1 a1 b1) y@(B v2 a2 b2)
| v1 < v2 = B v1 (andE a1 y) (andE b1 y)
| v1 > v2 = B v2 (andE x a2) (andE x b2)
| otherwise = B v1 (andE a1 a2) (andE b1 b2)

instance Bits E where
complement e = case e of
F -> T
T -> F
B v a b -> B v (complement a) (complement b)
a .&. b = simplify $ andE a b
where
simplify (B v a b)
| a' == b' = a'
| otherwise = B v a' b'
where
a' = simplify a
b' = simplify b
simplify e = e
a .|. b = complement (complement a .&. complement b)
xor a b = (complement a .&. b) .|. (a .&. complement b)
bit = undefined
popCount = undefined
bitSize = undefined
isSigned = undefined
testBit = undefined
Это такая несложная реализация BDD. Она использует упорядочение и поэтому довольно эффективна. Из BDD, сконструированной через операции типа .&., можно получить КНФ с помощью eToCNF.

Если я всё правильно понимаю, строки ограничений у Макса связываются через логическое И. Это эквивалентно соединению КНФ простым объединением - через соединение списков с последующим устранением одинаковых элементов.

Так вот, можно попробовать решать его задачу через преобразование каждой отдельной строки ограничений в КНФ через эту вот простую BDD, а потом соединить полученные КНФ. Количество переменных будет таким же, как и в оригинальной задаче. Могут встречаться длинные дизъюнкты, это основной минус, они снижают скорость работы решателя. Но, думаю, скорость работы будет выше, чем при преобразовании Цетина.