Silniki rozstrzygające spełnialność formuł logiki zdań (SAT) i formuł z teoriami tła, np. arytmetyką czy tablicami (SMT).
Engines deciding satisfiability of propositional formulas (SAT) and of formulas with background theories such as arithmetic or arrays (SMT).
Programy, które błyskawicznie sprawdzają, czy da się spełnić naraz tysiące logicznych warunków, i podają przykład takiego rozwiązania.
Programs that quickly check whether thousands of logical conditions can all hold at once, and give an example solution.
Wiele zadań, od planowania po sprawdzanie programów, wymaga przeszukania astronomicznej liczby kombinacji, czego nie da się zrobić ręcznie.
Many tasks, from scheduling to checking programs, require searching an astronomical number of combinations, impossible by hand.
Jak bardzo sprytny rozwiązywacz łamigłówek: próbuje, a po każdej sprzeczności zapisuje lekcję, żeby nie wpadać w ten sam błąd.
Like a very clever puzzle solver: it tries, and after each contradiction records a lesson so it never repeats the same mistake.
Narzędzie programisty wskazuje, przy jakich danych wejściowych program może się wysypać, zanim zrobi to użytkownik.
A developer tool points out which inputs could make a program crash before a user hits them.