Description

SIGmA (SAT sImplifications on GPU Architectures) is a SAT (Satisfiability) preprocessor that simplifies SAT problems on NVIDIA GPUs in order to accelerate SAT solving. The tool takes a SAT formula in DIMACS format and produce an output (simplified) formula also in DIMACS. The output can then be read and solved independently with state-of-the-art SAT solvers. SIGmA performs various types of simplification, such as variable elimination, subsumption elimination, blocked clause elimination.

Requirements

  • CUDA-capable device with at least (3.5) compute capability.
  • Install CUDA toolkit v9.2 or later for compiling the source code on a local machine.

Installation

  1. Linux-based OS
    • Download sigma.zip and extract the content into a new folder. For instance “sigma” in your home directory.
    • Run the command-line “make” on the local directory of sigma. The binary file “SIGmA” should be available after a successful compilation.
  2. Windows
    • Install a sufficient version of CUDA toolkit and Visual C++ IDE (Microsoft visual studio or Eclipse).
    • Create a new project using NVIDIA template in your IDE. Add the source files in “sigma.zip” to the created project then build.

Running SIGmA

SIGmA should be run from the command line (type -h or –help for more info on those options.). The basic usage of the tool is

SIGmA  [<option> …] [<input_file>.<cnf>] [<option> …]

The input file is in DIMACS format which encodes a SAT formula into an integer-number format (https://www.satcompetition.org/2009/format-benchmarks2009.html). SIGmA will automatically generate an output file in the local directory with the suffix “_simp” embed to the name of the input formula (i.e. <input_file><_simp>.<cnf>). 

Here (all_set or small_set) you can download a SAT benchmark set collected from the industrial track of the 2013, 2016 and 2017 SAT competitions (https://satcompetition.org/). The (all_set) consists of all problems from those tracks that are more than 1 MB in file size. The largest size of problems occurring in this set is 1.2 GB. Also, any occurring unit clauses in these problems were propagated. The presence of unit clauses immediately leads to simplification of the formula. By only considering formulas without unit clauses, the benchmark results directly indicate the true impact of our preprocessing algorithms.

For example, running SIGmA with options “-ve -hre”,

SIGmA  -ve  -hre  newton.5.1.i.smt2-cvc4.cnf 

will execute the simplification methods “variable elimination” followed by “hidden redundancy elimination” on the input formula “newton.5.1.i.smt2-cvc4.cnf “. The simplified formula will be produced and written in “newton.5.1.i.smt2-cvc4_simp.cnf”. 

The amount of reductions on variables, clauses and lietrals will be also printed out on the screen. Providing the tool option “-perf” gives a detailed report about the execution time in milliseconds.

For solving the simplified formula, use the output file as input to any SAT solver such as MiniSat.