Pavel Surynek's Academic Page | sigmaSAT


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

Currently, it comprises of the following three modules:

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.

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.

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