Pavel Surynek's Home Page

sigmaSAT is an experimental package for solving Boolean satisfiability and to conduct experiments with it.

Currently, it comprises of the following three modules:

encodeSIGMA
A collection of functions for generating arithmetic operators and relations over bit vectors as Boolean formulas. For example, bit-wise addition, equality, comparison, ... are implemented.

localSIGMA
A local search based SAT solver. The main framework is based on WalkSAT. One-literal watching scheme is used to speed-up search for satisfied and unsatisfied clauses. A careful maintenance of a set of unsatisfied clauses to make the selection of a random unsatisfied clause easier is implemented.

systemSIGMA
A systematic DPLL based SAT solver. Some features from modern state-of-the-art SAT solvers are implemented.

Relelease notes

Version 0.59
- Chronological backtracking replaced by conflict directed backjumping.
- Reorganization of the code.

Version 0.03
- Simple chronological backtracking with two-literal watching scheme.
- WalkSAT with one-literal watching.

Download sigmaSAT

Date	Title	Filename	Size
03/2011	sigmaSAT 0.59 source code	sigmaSAT‑0.59‑join.rls.tgz	25 937 bytes
06/2010	sigmaSAT 0.03 source code	sigmaSAT‑0.03‑join.rls.tgz	11 299 bytes

Keywords: SAT, local search, WalkSAT, literal watching