Fast SAT Solver (C++, GAlib)
Fast SAT Solver je program, který řeší problém splnitelnosti množiny výrokových proměnných pomocí genetického algoritmu. Tento problém je znám v literatuře jako SAT problém (z angl. SATisfiability problem). Jedná se o tzv. rozhodovací problém, který je zadán množinou formulí výrokové logiky. Úkolem je rozhodnout, jestli existuje takové ohodnocení výrokových proměnných, pro které jsou všechny formule splněné.
Z hlediska časové složitosti spadá tento problém do třídy NP - netriviální problémy spadající do této třídy časové složitosti není možné řešit běžnými algoritmy na současném HW v rozumném čase. Tento program řeší SAT problém pomocí genetického algoritmu, díky kterému je možné řešit (některé) instance tohoto problému ve výrazně kratším čase, než který odpovídá teoretické složitosti. Nevýhodou tohoto přístupu je, že není zaručeno, že bude řešení nalezeno v konečném čase, pokud existuje. Fast SAT Solver dokáže zadaný SAT problém řešit jak pomocí genetického algoritmu, tak pomocí slepého algoritmu (hrubou silou). V dokumentaci jsou tyto přístupy porovnány na různých instancích SAT problému.
Zdrojové soubory
Stáhnout (včetně zdrojových kódů GAlib)
Procházet
READMEBuild/installation
Build system CMake is required for successful build. Just type make to build GAlib, compile fss and link against GAlib:
$ make
On successful build, binaries will be in directory build. For now only GNU/Linux is supported, but source code is intended to be portable.
Prezentace