Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
  • Loading branch information
VaeterchenFrost committed May 4, 2020
2 parents 08cd9c5 + d395e79 commit 32b91cb
Showing 1 changed file with 35 additions and 30 deletions.
65 changes: 35 additions & 30 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ Giving a filename to --visufile \<visufile\>, a json-object specified by [td-vis
* cmake 3.2+
* gcc 7+
* Boost Multiprecision
* JsonCpp
* JsonCpp

### Tested with

Expand All @@ -26,10 +26,15 @@ Giving a filename to --visufile \<visufile\>, a json-object specified by [td-vis
## How to Build

The following commands can be used to build `GPUSAT`
```

```console
git clone https://github.com/Budddy/GPUSAT
cd GPUSAT
```

change *include_directories*, *find_library* to your needs

```console
mkdir build && cd build
cmake ..
make
Expand All @@ -41,32 +46,32 @@ 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] [-v] [-p] [--dataStructure \<dataStructure\>] [-m \<maxBagSize\>] [-w \<combineWidth\>] [-g \<graphfile\>] [--visufile \<visufile\>] < $CNFFILE


Options:
* -h,--help: Print this help message and exit.
* -s,--seed \<seed\>: number used to initialize the pseudorandom number generator.
* -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
* -v,--verbose: output more verbose/debug information
* -p,--nopreprocess: skips the preprocessing step for debugging- and visualisation-purpose
* --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
* -g,--graph \<graphfile\>: filename for saving the decomposition graph
* --visufile \<visufile\>: filename for saving the visualization file

* -h,--help: Print this help message and exit.
* -s,--seed \<seed\>: number used to initialize the pseudorandom number generator.
* -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
* -v,--verbose: output more verbose/debug information
* -p,--nopreprocess: skips the preprocessing step for debugging- and visualisation-purpose
* --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
* -g,--graph \<graphfile\>: filename for saving the decomposition graph
* --visufile \<visufile\>: filename for saving the visualization file

0 comments on commit 32b91cb

Please sign in to comment.