5 ms·
I wonder if they'll write a followup on the SMT revolution that happened after the CDCL breakthroughs for SAT. The lazy approach to SMT was a huge step forward
by xavxav 3y ago
I wonder if they'll write a followup on the SMT revolution that happened after the CDCL breakthroughs for SAT.
The lazy approach to SMT was a huge step forward, but itself spawned a whole lineage of refinements, alternatives and changed the state of automated reasoning entirely.
A lot of work today seems to be going into theory combinations so that you can efficiently answer problems for example involve arrays and integers in a manner that has dependencies between the two.
'Solving' (it's an undecidable problem) SMT would open up a bunch of new possibilities..
- maweki 3y ago> it's an undecidable problem In what sense? People often use SMT (Satisfiability modulo theories) but don't state _which_ theories. I often SMT-solve with decidable theories, like Presburger Arithmetic.
- xavxav 3y agoI almost exclusively use it with quantifiers which makes it equivalent to FOL. But even without quantifiers, theory combinations can introduce undecidability. There’s the auxiliary problem that decidable but slow can often be equivalent to undecidable.