Boolean satisfiability problems are the set of computational problems whose goal is to assign boolean values to a number of variables, in order to satisfy a list of constraints. In this case 2-SAT is the restricted problem where each clause has exactly two variables.
For example:
Despite this restriction 2-SAT allows to solve many different real life problems such as:
- Conflict-free placement of geometric objects.
- Data clustering.
- Scheduling
- Discrete tomography.
- Inferring business relationships among autonomous subsystems.
- Reconstruction of evolutionary trees.
Many general SAT solvers exist that are not specific to 2-SAT, in many cases implementing Davis–Putnam–Logemann–Loveland (DPLL) algorithm which has time complexity. However a much faster
algorithm exists that was designed only for 2-SAT, the Aspvall-Plass-Tarjan (APT) algorithm.
I will try to implement APT in Haskell as a usable package since currently there is no implementation in Haskell, as far as I am aware.
For speed comparisons we use the mios package. This sat solver uses CDCL which is based on DPLL to solve any kind of sat problem. But as we mentioned early this is not efficient for solving 2-sat.
The criterion benchmark shows that our APT implementation is 5 times faster for 2-sat formulas with 100000 clauses.
- Algorithm implementation.
- Basic examples.
- Property testing.
- Benchmark.
- Profiling.
- Package release.