diff --git a/README.md b/README.md index 54ee1b7..4d04c0a 100644 --- a/README.md +++ b/README.md @@ -11,7 +11,7 @@ Giving a filename to --visufile \, a json-object specified by [td-vis * cmake 3.2+ * gcc 7+ * Boost Multiprecision -* JsonCpp +* JsonCpp ### Tested with @@ -26,10 +26,15 @@ Giving a filename to --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 @@ -41,32 +46,32 @@ A program call is of the following form ./gpusat [-h] [-s \] [-f \] [-d \] [-n \] [--fitnessFunction \] [--CPU] [--NVIDIA] [--AMD] [--weighted] [--noExp] [-v] [-p] [--dataStructure \] [-m \] [-w \] [-g \] [--visufile \] < $CNFFILE - Options: -* -h,--help: Print this help message and exit. -* -s,--seed \: number used to initialize the pseudorandom number generator. -* -f,--formula \: path to the file containing the sat formula. -* -d,--decomposition \: path to the file containing the tree decomposition. -* -n,--numDecomps \: number of decompositions to generate for the fitness function. -* --fitnessFunction \: 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 \: 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 \: fixes the number of variables after which we need to split the bags -* -w,--combineWidth \: fixes the maximum width to combine bags of the decomposition -* -g,--graph \: filename for saving the decomposition graph -* --visufile \: filename for saving the visualization file + +* -h,--help: Print this help message and exit. +* -s,--seed \: number used to initialize the pseudorandom number generator. +* -f,--formula \: path to the file containing the sat formula. +* -d,--decomposition \: path to the file containing the tree decomposition. +* -n,--numDecomps \: number of decompositions to generate for the fitness function. +* --fitnessFunction \: 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 \: 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 \: fixes the number of variables after which we need to split the bags +* -w,--combineWidth \: fixes the maximum width to combine bags of the decomposition +* -g,--graph \: filename for saving the decomposition graph +* --visufile \: filename for saving the visualization file