SMT и рост сложности: сколько логики выдержит решатель. Никита Борсов, Райффайзен банк