SMT-Solver może być używany do rozwiązywania ograniczeń. Jak wiemy, rozwiązania CSP są również stosowane do rozwiązywania problemów przez wiele lat. Jakie są zalety rozwiązania SMT w stosunku do solverów CSP?Co jest zaletą rozwiązania SMT do rozwiązywania problemów z CSP-solver w rozwiązywaniu ograniczeń?
To całkowicie zależy od tego, co chcesz zrobić. Możesz tłumaczyć zarówno na SAT, jak i rozwiązywać problemy związane z więzami jako problem SAT. Rozwiązania ograniczające zwykle oferują najwyższy poziom abstrakcji, jeśli chodzi o modelowanie problemu. Rozwiązania SAT są bardzo szybkie, ale w zależności od twojego problemu SMT lub solver może być szybszy.
Nie ma ogólnej odpowiedzi na twoje pytanie. To zależy od konkretnego przypadku użycia.
Tak, masz rację, dziękuję ~ I chcę wiedzieć, kiedy solverowie SMT działają szybciej niż solwery CSP? lub jakie problemy są lepiej dostosowane do rozwiązań SMT i odwrotnie? Czy osoby rozwiązujące SMT mogą poradzić sobie z problemami optymalizacyjnymi, które mogą być obsługiwane przez solistów CSP? – user1393905
Oba ograniczenia i SMT mogą poradzić sobie z problemami optymalizacyjnymi, chociaż uważam, że wsparcie dla tego w rzeczywistych rozwiązaniach jest bardziej powszechne w ograniczeniach. Nie ma ustalonych reguł, gdy SMT/ograniczenia/SAT jest lepsze/szybsze/... To naprawdę zależy od rzeczywistego problemu, który próbujesz rozwiązać. –
OK, dziękuję bardzo ~ – user1393905