• Software to download
  • nucad (C++, GAlib, Boost)
  • Digital Watermarking (C++, Qt3, gnulib)
  • rob08 (C++, Qt4, Flex, Readline, Boost)
  • vyp08 (Flex, Bison, C++, Boost)
  • Fast SAT Solver (C++, GAlib)
  • RRV (C++, OpenGL)
• Web components
  • CharsetDetector (PHP)
  • QuickMenu (Javascript, PHP)
• Study
  • Programming fundamentals (IZP)
  • Algorithms (IAL)
  • Software engineering (IUS)
• Archive
  • FileBrowser (Javascript, PHP, Smarty)
  • SGVis (Java, Prefuse)
  • Share Library (C++)
  • emulT9 (C++, Qt4)
  • FastPad (Assembler)
  • GED 2006 (C++)
  • IFJ 05 (C language)
  • Tiny programs (C, C++, C#, ...)
• Contact

Fast SAT Solver (C++, GAlib)

Fast SAT Solver is an program, which solves the Boolean satisfiability problem. Complexity of this problem is NP-completeness, non-trivial problems of this complexity can not be solved on current HW in reasonable time while using ordinary algorithms.

This program solves problem using genetic algorithm (GA). Thanks to GA, (some) instances of this problem can be solved much faster than problem's theoretical complexity expects to. Disadvantage of this approach is fact, that there is not guarantee to find solution if any exists. Fast SAT Solver can solve this problem using either GA, or by blind algorithm (brute force).

The software for this work used the GAlib genetic algorithm package, written by Matthew Wall at the Massachusetts Institute of Technology.

Source code

Build/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.

Documentation