Pavel Surynek's Academic Page | sigmaSAT

sigmaSAT

Hide menu   Show menu   Jump to the bottom   Print 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

Copyright © 2003-2014  

Hide menu   Show menu   Jump to the top   Print page