Как строятся современные решатели по модулю теорий
https://homepages.dcc.ufmg.br/~hbarbosa/papers/tacas2022.pdf
Стр. 4: "Currently, cvc5 implements 34 (preprocessing - sz) passes, executed in a fixed order."
Ну как так?
А вообще интересно - используется накопление ограничений по модулю теорий, CDCL(T). Я знаю, как это сделать для псевдологических (pseudo boolean) задач и для логических задач, а тут описана архитектура для произвольных теорий.
Примечательно, что используется MiniSAT в качестве основного решателя. MiniSAT довольно прост и, откровенно говоря, довольно стар - практически всего его находки уже использованы и превзойдены. Почему MiniSAT, непонятно, поэтому продолжу читать.
Стр. 4: "Currently, cvc5 implements 34 (preprocessing - sz) passes, executed in a fixed order."
Ну как так?
А вообще интересно - используется накопление ограничений по модулю теорий, CDCL(T). Я знаю, как это сделать для псевдологических (pseudo boolean) задач и для логических задач, а тут описана архитектура для произвольных теорий.
Примечательно, что используется MiniSAT в качестве основного решателя. MiniSAT довольно прост и, откровенно говоря, довольно стар - практически всего его находки уже использованы и превзойдены. Почему MiniSAT, непонятно, поэтому продолжу читать.