8.01.2009

Rachunek zdań jako środowisko programistyczne dla algebry liniowej

W referacie przedstawimy metodę wykorzystania rachunku zdań i testerów spełnialności SAT, jako środowiska programistycznego do rozwiązywania pewnych interesujących problemów z algebry liniowej, w prostym przypadku problemów własności przestrzeni liniowej nad ciałem dwuelementowym. Pokażemy kodowanie takich własności formułami zdaniowymi w taki sposób, że wartościowanie spełniające te formuły koduje rozwiązanie rozważanego problemu. Przedstawimy projekt wyspecjalizowanego narzędzia do tego rodzaju zadań i dość zachęcające (oraz nie całkiem zachęcające) wyniki eksperymentalne dla zadań takich jak: efektywne wyszukiwanie baz pewnego typu w pewnych przestrzeniach, sprawdzanie warunku ortogonalności macierzy A stopnia n złożonych z wektorów pewnych przestrzeni liniowych, oraz wyznaczanie liczby wszystkich macierzy ortogonalnych (czyli określaniu rzędów tzw. grup ortogonalnych).
Wprowadzimy pojęcie wartościowania wyrażeń arytmetycznych i metodę przekształcania dowolnego wyrażenia arytmetycznego na zbiór klauzul zdaniowych z pominięciem tradycyjnej postaci formuły zdaniowej, w taki sposób by wartościowanie otrzymywanej formuły zdaniowej było zgodne z wartościowaniem wejściowego wyrażenia arytmetycznego. Przykłady zagadnień z algebry dobrane są tak, by były interesujące także dla algebraików. Na przykład, grupom ortogonalnym w odpowiednich przestrzeniach liniowych odpowiadają pewne szczególne automorfizmy pewnej klasy tzw. pierścieni Witta. Wypisanie wszystkich automorfizmów daje możliwość badania ich własności.