From 45644bbe7af18a3bce61350cd098f56e687c4780 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 4 Oct 2020 10:26:14 +0200 Subject: [PATCH 1/5] Create build.yml --- .github/workflows/build.yml | 69 +++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 .github/workflows/build.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000..75dd8b6 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,69 @@ +name: CMake + +on: [push] + +env: + # Customize the CMake build type here (Release, Debug, RelWithDebInfo, etc.) + BUILD_TYPE: Release + +jobs: + build: + # The CMake configure and build commands are platform agnostic and should work equally + # well on Windows or Mac. You can convert this to a matrix build if you need + # cross-platform coverage. + # See: https://docs.github.com/en/actions/configuring-and-managing-workflows/configuring-a-workflow#configuring-a-build-matrix + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + + - name: Create Build Environment + # Some projects don't allow in-source building, so create a separate build directory + # We'll use this as our working directory for all subsequent commands + run: cmake -E make_directory ${{runner.workspace}}/build + + - name: Get Dependencies + run: sudo apt-get update && sudo apt-get install -yq libboost1.65-dev libboost-program-options-dev help2man + + - name: Build CMS + run: | + mkdir cms_git && cd cms_git + git clone --depth 1 https://github.com/msoos/cryptominisat + cd cryptominisat + mkdir build && cd build + cmake .. + make + cd ../../.. + + - name: Build AppMC + run: | + mkdir appmc_git && cd appmc_git + git clone --depth 1 https://github.com/meelgroup/approxmc + cd approxmc + mkdir build && cd build + cmake .. + make + cd ../../.. + + - name: Configure CMake + # Use a bash shell so we can use the same syntax for environment variable + # access regardless of the host operating system + shell: bash + working-directory: ${{runner.workspace}}/build + # Note the current convention is to use the -S and -B options here to specify source + # and build directories, but this is only available with CMake 3.13 and higher. + # The CMake binaries on the Github Actions machines are (as of this writing) 3.12 + run: cmake $GITHUB_WORKSPACE -DCMAKE_BUILD_TYPE=$BUILD_TYPE + + - name: Build + working-directory: ${{runner.workspace}}/build + shell: bash + # Execute the build. You can specify a specific target with "--target " + run: cmake --build . --config $BUILD_TYPE + + - name: Test + working-directory: ${{runner.workspace}}/build + shell: bash + # Execute tests defined by the CMake configuration. + # See https://cmake.org/cmake/help/latest/manual/ctest.1.html for more detail + run: ctest -C $BUILD_TYPE From a4a0b0c7320f038a61a67d510efcca8e62db14ec Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 4 Oct 2020 10:28:33 +0200 Subject: [PATCH 2/5] Update build.yml --- .github/workflows/build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 75dd8b6..77aaf03 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,4 +1,4 @@ -name: CMake +name: build on: [push] From ca2903202e8f4bfd8337eabc729e59d4eb06e4ac Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 4 Oct 2020 10:29:04 +0200 Subject: [PATCH 3/5] Update README.md --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 8950069..e035e00 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,5 @@ [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) +![build](https://github.com/meelgroup/unigen/workflows/build/badge.svg) # UniGen3: Almost-Uniform Sampler UniGen3 is the state of the art almost-uniform sampler utilizing an improved version of CryptoMiniSat to handle problems of size and complexity that were not possible before. The current version is based on work Mate Soos, Stephan Gocht, and Kuldeep S. Meel, as [published in CAV-20](http://comp.nus.edu.sg/~meel/Papers/cav20-sgm.pdf). Please see below for credits. A large part of the work is in CryptoMiniSat [here](https://github.com/msoos/cryptominisat). From be87a202738ea7367e73d83d9caa8a9ecd767691 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 4 Oct 2020 10:31:39 +0200 Subject: [PATCH 4/5] Update README.md --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index e035e00..da5526a 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,6 @@ [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) ![build](https://github.com/meelgroup/unigen/workflows/build/badge.svg) +[![Docker Hub](https://img.shields.io/badge/docker-latest-blue.svg)](https://hub.docker.com/r/msoos/unigen/) # UniGen3: Almost-Uniform Sampler UniGen3 is the state of the art almost-uniform sampler utilizing an improved version of CryptoMiniSat to handle problems of size and complexity that were not possible before. The current version is based on work Mate Soos, Stephan Gocht, and Kuldeep S. Meel, as [published in CAV-20](http://comp.nus.edu.sg/~meel/Papers/cav20-sgm.pdf). Please see below for credits. A large part of the work is in CryptoMiniSat [here](https://github.com/msoos/cryptominisat). From 22ee6b466d5ddd2287d7939eed9b36f763d440a9 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 13 Nov 2020 21:12:20 +0100 Subject: [PATCH 5/5] Update README.md --- README.md | 56 +++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 46 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index da5526a..f6e8c3f 100644 --- a/README.md +++ b/README.md @@ -23,14 +23,11 @@ cat formula.cnf | docker run --rm -i -a stdin -a stdout msoos/unigen ``` ## How to Build -To build on Linux, you will need the following: +To build on Linux: + ``` sudo apt-get install build-essential cmake sudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev -``` - -Then, build CryptoMiniSat, ApproxMC, and UniGen: -``` git clone https://github.com/msoos/cryptominisat cd cryptominisat mkdir build && cd build @@ -53,9 +50,6 @@ make sudo make install ``` -## How to Use -First, you must translate your problem to CNF and just pass your file as input to UniGen. Voila -- and it will print the set of samples. - ### Sampling Set For some applications, one is not interested in solutions over all the variables and instead interested in sampling over the solutions projected to a subset of variables, called sampling set. UniGen allows you to specify the sampling set using the following modified version of DIMACS format: @@ -80,11 +74,53 @@ c ind 3 4 7 8 10 11 14 17 18 26 30 35 36 39 42 47 60 62 67 0 You must copy the line starting with `c ind ...` to the top of your CNF before running ApproxMC. -### Running UniGen +### Library Use +Below is an example library use: +``` +#include +using namespace CMSat; +using namespace UniGen; +using std::cout; +using std::endl; + +void mycallback(const std::vector& solution, void*) +{ + for(uint32_t i = 0; i < solution.size(); i++) { + cout << solution[i] << " "; + } + cout << "0" << endl; +} + +int main () { + auto appmc = new ApproxMC::AppMC; + auto unigen = new UniG(appmc); + appmc->set_verbosity(verbosity); + unigen->set_callback(mycallback, NULL); + vector lits; + + appmc->add_variables(3); + lits.clear(); + lits.push_back(Lit(0, true)); + lits.push_back(Lit(1, true)); + appmc->addClause(lits); + + auto sol_count = appmc->count(); + unigen->sample(&sol_count, num_samples); + + lits.clear(); + lits.push_back(Lit(0, true)); + lits.push_back(Lit(2, true)); + appmc->addClause(lits); + + sol_count = appmc->count(); + unigen->sample(&sol_count, num_samples); + return 0; +} +``` -### Guarantees +### Guarantees UniGen ensures that the generated distribution is within (1+\epsilon)-multiplicative factor of the ideal uniform distribution.