GPUSAT

KO | EN

gitlite — search

#hacktoberfest #react #typescript #llm #golang #machine-learning #docker #macos #windows #awesome #cli #kubernetes #vue #mcp

(★ 12)

No description available.

GPUSAT Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# GPUSAT3

A #SAT solver based on dynamic programming running on the GPU.
Version 3 contains new additional improvements and is based on the CUDA framework.

## Dependencies

* htd 1.2.0 - https://github.com/mabseher/htd (build with cmake option -DBUILD_SHARED_LIBS=OFF)
* CUDA 10.2
* cmake 3.2+
* gcc 7+
* Boost Multiprecision

## How to Build

The following commands can be used to build `GPUSAT`
```
git clone https://github.com/vroland/GPUSAT
cd GPUSAT
mkdir build && cd build
cmake ..
make
```

## Usage

A program call is of the following form

./gpusat [-h] [-s \<seed\>] [-f \<formulaPath\>] [-d \<decompositionPath\>] [-n \<numberOfDecompositions\>] [--fitnessFunction \<fitness\>] [--CPU] [--NVIDIA] [--AMD] [--weighted] [--noExp] [--dataStructure \<dataStructure\>] [-m \<maxBagSize\>] [-w \<combineWidth\>] < $CNFFILE

Options:
*  -h,--help: Print this help message and exit.
*  -s,--seed \<seed\>: path to the file containing the sat formula.
*  -f,--formula \<formulaPath\>: path to the file containing the sat formula.
*  -d,--decomposition \<decompositionPath\>: path to the file containing the tree decomposition.
*  -n,--numDecomps \<numberOfDecompositions\>: number of decompositions to generate for the fitness function.
*  --fitnessFunction \<function\>: use the fitnessfunction to optimize the tree decomposition.
    * Permitted Values:
        * numJoin: minimize the number of joins
        * joinSize: minimize the numer of variables in a join node
        * width_cutSet: minimize the width and then the cut set size (default)
        * cutSet_width: minimize the cut set size and then the width
*  --CPU: run the solver on a cpu
*  --NVIDIA: run the solver on an NVIDIA device
*  --AMD: run the solver on an AMD device
*  --weighted: use weighted model count
*  --noExp: don't use extended exponents
*  --dataStructure \<dataStructure\>: data structure for storing the solution.
    * Permitted Values:
        * array: use an array to store the solutions
        * tree: use a tree structure to store the solutions
        * combined: use a combination of tree and array structure (default)
*  -m,--maxBagSize \<maxBagSize\>: fixes the number of variables after which we need to split the bags
*  -w,--combineWidth \<combineWidth\>: fixes the maximum width to combine bags of the decomposition

GPUSAT

GPUSAT Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

GPUSAT

GPUSAT Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README