[{"_1":2,"_155":-5,"_156":-5},"loaderData",{"_3":4,"_13":14,"_21":22,"_134":135},"root",{"_5":-5,"_6":-7,"_7":8,"_9":-7,"_10":11,"_12":-7},"currentUser","primaryEmail","siteVerification","6LeIxAcTAAAAAJcZVRqyHh71UMIEGNQ_MXjiZKhI","toast","enableDev",false,"incidentStatus","routes/_layout",{"_15":-5,"_16":17,"_18":17,"_19":11,"_20":11},"username","isAskGordonEnabled",true,"isUsingNewTemplate","showMinimalLanding","showHoneypotTrap","routes/_layout.r.$namespace.$reponame",{"_23":24,"_25":-5,"_26":11,"_27":11,"_28":29,"_30":31,"_32":-5,"_33":11,"_34":35,"_84":-5,"_85":86,"_125":-5,"_126":11,"_127":17,"_128":11,"_129":-5,"_130":11,"_131":-5,"_132":133},"canonicalUrl","https://hub.docker.com/r/msoos/unigen/tags","mcpServer","canSeeDockerfile","canSeeAutobuilds","namespace","msoos","reponame","unigen","cloudBuildSource","isAutobuildsAvailable","repo",{"_36":37,"_38":39,"_41":42,"_43":44,"_45":11,"_46":47,"_48":49,"_50":51,"_53":31,"_28":29,"_54":55,"_56":40,"_57":58,"_59":60,"_61":62,"_63":-5,"_64":58,"_65":66,"_67":11,"_68":29,"_69":70,"_75":11,"_76":77,"_81":29,"_82":83},"categories",[],"content_types",[40],"image","date_registered","2020-07-06T22:17:38.436203Z","description","UniGen approximately uniform sampler","is_private","last_updated","2021-03-30T16:53:02.755837Z","last_modified","2024-10-16T13:48:34.145251Z","media_types",[52],"application/vnd.docker.container.image.v1+json","name","pull_count",269,"repository_type","star_count",0,"status",1,"status_description","active","source","collaborator_count","full_description","[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)\n![build](https://github.com/meelgroup/unigen/workflows/build/badge.svg)\n[![Docker Hub](https://img.shields.io/badge/docker-latest-blue.svg)](https://hub.docker.com/r/msoos/unigen/)\n\n# UniGen3: Almost-Uniform Sampler\nUniGen3 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).\n\n\n\n## Docker image\nIf you don't have or don't know what an independent set is, first run our MIS tool:\n```\ndocker run --rm -v `pwd`/formula.cnf:/in msoos/mis --timeout 300 /in\n[...]\n** Copy-paste the following line in the top of your CNF for UniGen **\nc ind 3 4 7 8 10 11 14 17 18 26 30 35 36 39 42 47 60 62 67 0\n```\nThen copy-paste that line into your CNF.\n\nThen run the updated CNF through unigen:\n```\ncat formula.cnf | docker run --rm -i -a stdin -a stdout msoos/unigen\n```\n\n## How to Build\nTo build on Linux:\n\n```\nsudo apt-get install build-essential cmake\nsudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev\ngit clone https://github.com/msoos/cryptominisat\ncd cryptominisat\nmkdir build && cd build\ncmake -DUSE_GAUSS=ON ..\nmake\nsudo make install\ncd ../..\ngit clone https://github.com/meelgroup/approxmc/\ncd approxmc\nmkdir build && cd build\ncmake ..\nmake\nsudo make install\ncd ../..\ngit clone https://github.com/meelgroup/unigen/\ncd unigen\nmkdir build && cd build\ncmake ..\nmake\nsudo make install\n```\n\n### Sampling Set\n\nFor 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:\n\n```\n$ cat myfile.cnf\nc ind 1 3 4 6 7 8 10 0\np cnf 500 1\n3 4 0\n```\nAbove, using the `c ind` line, we declare that only variables 1, 3, 4, 6, 7, 8 and 10 form part of the sampling set out of the CNF's 500 variables `1,2...500`. This line must end with a 0. Naturally, if your sampling set only contains 7 variables, then the maximum number of solutions restricted to sampling set can only be at most 2^7 = 128. This is true even if your CNF has thousands of variables.\n\n### Independent set\nFor most applications, we are want all solutions to the problem. To do this, you need to use the [MIS](https://github.com/meelgroup/mis) tool to find a small independent set of variables to your CNF. For example, for `formula.cnf` we can do:\n\n```\ndocker run --rm -v `pwd`/formula.cnf:/in msoos/mis --timeout 300 /in\n[...]\n** Copy-paste the following line in the top of your CNF for UniGen **\nc ind 3 4 7 8 10 11 14 17 18 26 30 35 36 39 42 47 60 62 67 0\n```\n\nYou must copy the line starting with `c ind ...` to the top of your CNF before running ApproxMC.\n\n### Library Use\nBelow is an example library use:\n\n```\n#include \nusing namespace CMSat;\nusing namespace UniGen;\nusing std::cout;\nusing std::endl;\n\nvoid mycallback(const std::vector& solution, void*)\n{\n for(uint32_t i = 0; i < solution.size(); i++) {\n cout << solution[i] << \" \";\n }\n cout << \"0\" << endl;\n}\n\nint main () {\n auto appmc = new ApproxMC::AppMC;\n auto unigen = new UniG(appmc);\n appmc->set_verbosity(verbosity);\n unigen->set_callback(mycallback, NULL);\n vector lits;\n\n appmc->add_variables(3);\n lits.clear();\n lits.push_back(Lit(0, true));\n lits.push_back(Lit(1, true));\n appmc->addClause(lits);\n\n auto sol_count = appmc->count();\n unigen->sample(&sol_count, num_samples);\n\n lits.clear();\n lits.push_back(Lit(0, true));\n lits.push_back(Lit(2, true));\n appmc->addClause(lits);\n\n sol_count = appmc->count();\n unigen->sample(&sol_count, num_samples);\n return 0;\n}\n```\n\n\n### Guarantees\nUniGen ensures that the generated distribution is within (1+\\epsilon)-multiplicative factor of the ideal uniform distribution. \n\n\n### Issues, questions, bugs, etc.\nPlease click on \"issues\" at the top and [create a new issue](https://github.com/meelgroup/unigen/issues/new). All issues are responded to promptly.\n\n## How to Cite\nIf you use UniGen, please cite the following papers: [CAV20](https://www.comp.nus.edu.sg/~meel/bib/SGM20.bib), [TACAS15](https://www.comp.nus.edu.sg/~meel/bib/CFMSV15a.bib), and [DAC14](https://www.comp.nus.edu.sg/~meel/bib/CMV14.bib).\n\nUniGen builds on a series of papers on hashing-based approach: [Related Publications](https://www.comp.nus.edu.sg/~meel/publications.html)\n\n## Contributors\nUniGen is based on research papers published over the period of 2012-20 and co-authored by (in alphabetical order): Supratik Chakraborty, Daniel Fremont, Stephan Gocht, Kuldeep S. Meel, Sanjit A. Seshia, Mate Soos, and Moshe Y. Vardi. \n\n\n","has_starred","hub_user","immutable_tags_settings",{"_71":11,"_72":73},"enabled","rules",[74],".*","is_automated","permissions",{"_78":17,"_79":11,"_80":11},"read","write","admin","user","storage_size",156287161,"orgData","recentTags",[87],{"_88":40,"_89":90,"_91":92,"_93":94,"_95":96,"_46":114,"_115":90,"_116":29,"_117":52,"_53":118,"_119":120,"_121":105,"_122":114,"_123":62,"_124":17},"content_type","creator",310244,"full_size",11024761,"id",107521316,"images",[97],{"_98":99,"_100":101,"_102":103,"_104":105,"_106":107,"_108":109,"_110":103,"_111":-5,"_112":92,"_59":62,"_113":-5},"architecture","amd64","digest","sha256:c4d9665982251f5ccb9b8db4d86804f986b2a801cbc9cc1142cd5d903fcd094d","features","","last_pulled","2026-09-24T22:27:28.246243649Z","last_pushed","2021-03-30T16:53:03Z","os","linux","os_features","os_version","size","variant","2021-03-30T16:53:02.460121Z","last_updater","last_updater_username","media_type","latest","repository",9399484,"tag_last_pulled","tag_last_pushed","tag_status","v2","sbxKitMetadata","isPotentialSpam","isHubSbxKitsEnabled","showSbxLogoOverride","sbxTrademarkText","displaySecurityMetadata","tagAttestations","tagsHaveAttestations",[],"routes/_layout.r.$namespace.$reponame.tags",{"_34":136,"_143":144,"_132":153,"_154":11},{"_36":137,"_38":138,"_41":42,"_43":44,"_45":11,"_46":47,"_48":49,"_50":139,"_53":31,"_28":29,"_54":55,"_56":40,"_57":58,"_59":60,"_61":62,"_63":-5,"_64":58,"_65":66,"_67":11,"_68":29,"_69":140,"_75":11,"_76":142,"_81":29,"_82":83},[],[40],[52],{"_71":11,"_72":141},[74],{"_78":17,"_79":11,"_80":11},"tags",{"_145":60,"_146":-5,"_147":-5,"_148":149},"count","next","previous","results",[150],{"_88":40,"_89":90,"_91":92,"_93":94,"_95":151,"_46":114,"_115":90,"_116":29,"_117":52,"_53":118,"_119":120,"_121":105,"_122":114,"_123":62,"_124":17},[152],{"_98":99,"_100":101,"_102":103,"_104":105,"_106":107,"_108":109,"_110":103,"_111":-5,"_112":92,"_59":62,"_113":-5},[],"canDeleteTags","actionData","errors"]

msoos/unigen

Tags for msoos/unigen