[{"_1":2,"_169":-5,"_170":-5},"loaderData",{"_3":4,"_13":14,"_21":22,"_144":145},"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,"_135":-5,"_136":11,"_137":17,"_138":11,"_139":-5,"_140":11,"_141":-5,"_142":143},"canonicalUrl","https://hub.docker.com/r/msoos/cryptominisat/tags","mcpServer","canSeeDockerfile","canSeeAutobuilds","namespace","msoos","reponame","cryptominisat","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":58,"_60":61,"_62":-5,"_63":64,"_65":66,"_67":11,"_68":29,"_69":70,"_75":11,"_76":77,"_81":29,"_82":83},"categories",[],"content_types",[40],"image","date_registered","2017-09-23T20:03:40.572109Z","description","cryptominisat, a state-of-the-art SAT solver","is_private","last_updated","2021-10-20T13:37:52.784606Z","last_modified","2024-10-16T13:48:34.145251Z","media_types",[52],"application/vnd.docker.container.image.v1+json","name","pull_count",3718,"repository_type","star_count",1,"status","status_description","active","source","collaborator_count",0,"full_description","[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)\n[![Liunux&Mac build](https://travis-ci.org/msoos/cryptominisat.svg?branch=master)](https://travis-ci.org/msoos/cryptominisat)\n[![Windows build](https://ci.appveyor.com/api/projects/status/8d000iy63xu7eau5?svg=true)](https://ci.appveyor.com/project/msoos/cryptominisat)\n![build](https://github.com/msoos/cryptominisat/workflows/build/badge.svg)\n[![Coverity](https://scan.coverity.com/projects/507/badge.svg)](https://scan.coverity.com/projects/507)\n[![Codacy Badge](https://app.codacy.com/project/badge/Grade/f7b6a138a30c47378343fe2ef13d0f0d)](https://www.codacy.com/gh/msoos/cryptominisat/dashboard?utm_source=github.com&utm_medium=referral&utm_content=msoos/cryptominisat&utm_campaign=Badge_Grade)\n[![Docker Hub](https://img.shields.io/badge/docker-latest-blue.svg)](https://hub.docker.com/r/msoos/cryptominisat/)\n\n\nCryptoMiniSat SAT solver\n===========================================\n\nThis system provides CryptoMiniSat, an advanced incremental SAT solver. The system has 3\ninterfaces: command-line, C++ library and python. The command-line interface\ntakes a [cnf](http://en.wikipedia.org/wiki/Conjunctive_normal_form) as an\ninput in the [DIMACS](http://www.satcompetition.org/2009/format-benchmarks2009.html)\nformat with the extension of XOR clauses. The C++ and python interface mimics this and also\nallows for incremental use: assumptions and multiple `solve` calls.\nA C compatible wrapper is also provided.\n\nWhen citing, always reference our [SAT 2009 conference paper](https://link.springer.com/chapter/10.1007%2F978-3-642-02777-2_24), bibtex record is [here](http://dblp.uni-trier.de/rec/bibtex/conf/sat/SoosNC09).\n\nLicense\n-----\n\nPlease read LICENSE.txt for a discussion. Everything that is needed to build is MIT licensed. The M4RI library (not included) is GPL, so in case you have M4RI installed, you must build with `-DNOM4RI=ON` or `-DMIT=ON` in case you need a pure MIT build.\n\n\nDocker usage\n-----\n\nTo run on file `myfile.cnf`:\n\n```\ncat myfile.cnf | docker run --rm -i msoos/cryptominisat\n```\n\nTo run on the file `/home/myfolder/myfile.cnf.gz` by mounting it (may be faster):\n\n```\ndocker run --rm -v /home/myfolder/myfile.cnf.gz:/f msoos/cryptominisat f\n```\n\n\nCompiling in Linux\n-----\n\nTo build and install, issue:\n\n```\nsudo apt-get install build-essential cmake\n# not required but very useful\nsudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev libsqlite3-dev help2man\ntar xzvf cryptominisat-version.tar.gz\ncd cryptominisat-version\nmkdir build && cd build\ncmake ..\nmake\nsudo make install\nsudo ldconfig\n```\n\nCompiling in Mac OSX\n-----\n\nFirst, you must get Homebrew from https://brew.sh/ then:\n\n```\nbrew install cmake boost zlib\ntar xzvf cryptominisat-version.tar.gz\ncd cryptominisat-version\nmkdir build && cd build\ncmake ..\nmake\nsudo make install\n```\n\nCompiling in Windows\n-----\n\nYou will need python installed, then for Visual Studio 2015:\n\n```\nC:\\> [ download cryptominisat-version.zip ]\nC:\\> unzip cryptominisat-version.zip\nC:\\> rename cryptominisat-version cms\nC:\\> cd cms\nC:\\cms> mkdir build\nC:\\cms> cd build\n\nC:\\cms\\build> [ download http://sourceforge.net/projects/boost/files/boost/1.59.0/boost_1_59_0.zip ]\nC:\\cms\\build> unzip boost_1_59_0.zip\nC:\\cms\\build> mkdir boost_1_59_0_install\nC:\\cms\\build> cd boost_1_59_0\nC:\\cms\\build\\boost_1_59_0> bootstrap.bat --with-libraries=program_options\nC:\\cms\\build\\boost_1_59_0> b2 --with-program_options address-model=64 toolset=msvc-14.0 variant=release link=static threading=multi runtime-link=static install --prefix=\"C:\\cms\\build\\boost_1_59_0_install\" > boost_install.out\nC:\\cms\\build\\boost_1_59_0> cd ..\n\nC:\\cms\\build> git clone https://github.com/madler/zlib\nC:\\cms\\build> cd zlib\nC:\\cms\\build\\zlib> git checkout v1.2.8\nC:\\cms\\build\\zlib> mkdir build\nC:\\cms\\build\\zlib> mkdir myinstall\nC:\\cms\\build\\zlib> cd build\nC:\\cms\\build\\zlib\\build> cmake -G \"Visual Studio 14 2015 Win64\" -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=C:\\cms\\build\\zlib\\myinstall ..\nC:\\cms\\build\\zlib\\build> msbuild /t:Build /p:Configuration=Release /p:Platform=\"x64\" zlib.sln\nC:\\cms\\build\\zlib\\build> msbuild INSTALL.vcxproj\nC:\\cms\\build> cd ..\\..\n\nC:\\cms\\build> cmake -G \"Visual Studio 14 2015 Win64\" -DCMAKE_BUILD_TYPE=Release -DSTATICCOMPILE=ON -DZLIB_ROOT=C:\\cms\\build\\zlib\\myinstall -DBOOST_ROOT=C:\\cms\\build\\boost_1_59_0_install ..\nC:\\cms\\build> cmake --build --config Release .\n```\n\nYou now have the static binary under `C:\\cms\\build\\Release\\cryptominisat5.exe`\n\nCommand-line usage\n-----\n\nLet's take the file:\n```\np cnf 3 3\n1 0\n-2 0\n-1 2 3 0\n```\n\nThe file has 3 variables and 3 clauses, this is reflected in the header\n`p cnf 3 3` which gives the number of variables as the first number and the number of clauses as the second.\nEvery clause is ended by '0'. The clauses say: 1 must be True, 2\nmust be False, and either 1 has to be False, 2 has to be True or 3 has to be\nTrue. The only solution to this problem is:\n```\ncryptominisat5 --verb 0 file.cnf\ns SATISFIABLE\nv 1 -2 3 0\n```\n\nWhich means, that setting variable 1 True, variable 2 False and variable 3 True satisfies the set of constraints (clauses) in the CNF. If the file had contained:\n```\np cnf 3 4\n1 0\n-2 0\n-3 0\n-1 2 3 0\n```\n\nThen there is no solution and the solver returns `s UNSATISFIABLE`.\n\nIncremental Python Usage\n-----\nThe python module works with both Python 2 and Python 3. It must be compiled as per (notice \"python-dev\"):\n\n```\nsudo apt-get install build-essential cmake\nsudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev libsqlite3-dev help2man\nsudo apt-get install python3-setuptools python3-dev\ntar xzvf cryptominisat-version.tar.gz\ncd cryptominisat-version\nmkdir build && cd build\ncmake ..\nmake\nsudo make install\nsudo ldconfig\n\n```\n\nYou can then use it in incremental mode as:\n\n```\n>>> from pycryptosat import Solver\n>>> s = Solver()\n>>> s.add_clause([1])\n>>> s.add_clause([-2])\n>>> s.add_clause([-1, 2, 3])\n>>> sat, solution = s.solve()\n>>> print sat\nTrue\n>>> print solution\n(None, True, False, True)\n>>> sat, solution = s.solve([-3])\n>> print sat\nFalse\n>>> sat, solution = s.solve()\n>>> print sat\nTrue\n>>> s.add_clause([-3])\n>>> sat, solution = s.solve()\n>>> print sat\nFalse\n\n```\n\nWe can also try to assume any variable values for a single solver run:\n```\n>>> sat, solution = s.solve([-3])\n>>> print sat\nFalse\n>>> print solution\nNone\n>>> sat, solution = s.solve()\n>>> print sat\nTrue\n>>> print solution\n(None, True, False, True)\n```\n\nFor more detailed usage instructions, please see the README.rst under the `python`\ndirectory.\n\nIncremental Library Usage\n-----\nThe library uses a variable numbering scheme that starts from 0. Since 0 cannot\nbe negated, the class `Lit` is used as: `Lit(variable_number, is_negated)`. As\nsuch, the 1st CNF above would become:\n\n```\n#include \n#include \n#include \nusing std::vector;\nusing namespace CMSat;\n\nint main()\n{\n SATSolver solver;\n vector clause;\n\n //Let's use 4 threads\n solver.set_num_threads(4);\n\n //We need 3 variables. They will be: 0,1,2\n //Variable numbers are always trivially increasing\n solver.new_vars(3);\n\n //add \"1 0\"\n clause.push_back(Lit(0, false));\n solver.add_clause(clause);\n\n //add \"-2 0\"\n clause.clear();\n clause.push_back(Lit(1, true));\n solver.add_clause(clause);\n\n //add \"-1 2 3 0\"\n clause.clear();\n clause.push_back(Lit(0, true));\n clause.push_back(Lit(1, false));\n clause.push_back(Lit(2, false));\n solver.add_clause(clause);\n\n lbool ret = solver.solve();\n assert(ret == l_True);\n std::cout\n << \"Solution is: \"\n << solver.get_model()[0]\n << \", \" << solver.get_model()[1]\n << \", \" << solver.get_model()[2]\n << std::endl;\n\n //assumes 3 = FALSE, no solutions left\n vector assumptions;\n assumptions.push_back(Lit(2, true));\n ret = solver.solve(&assumptions);\n assert(ret == l_False);\n\n //without assumptions we still have a solution\n ret = solver.solve();\n assert(ret == l_True);\n\n //add \"-3 0\"\n //No solutions left, UNSATISFIABLE returned\n clause.clear();\n clause.push_back(Lit(2, true));\n solver.add_clause(clause);\n ret = solver.solve();\n assert(ret == l_False);\n\n return 0;\n}\n```\n\nThe library usage also allows for assumptions. We can add these lines just\nbefore the `return 0;` above:\n```\nvector assumptions;\nassumptions.push_back(Lit(2, true));\nlbool ret = solver.solve(&assumptions);\nassert(ret == l_False);\n\nlbool ret = solver.solve();\nassert(ret == l_True);\n```\n\nSince we assume that variable 2 must be false, there is no solution. However,\nif we solve again, without the assumption, we get back the original solution.\nAssumptions allow us to assume certain literal values for a _specific run_ but\nnot all runs -- for all runs, we can simply add these assumptions as 1-long\nclauses.\n\nMultiple solutions\n-----\n\nTo find multiple solutions to your problem, just run the solver in a loop\nand ban the previous solution found:\n\n```\nwhile(true) {\n lbool ret = solver->solve();\n if (ret != l_True) {\n assert(ret == l_False);\n //All solutions found.\n exit(0);\n }\n\n //Use solution here. print it, for example.\n\n //Banning found solution\n vector ban_solution;\n for (uint32_t var = 0; var < solver->nVars(); var++) {\n if (solver->get_model()[var] != l_Undef) {\n ban_solution.push_back(\n Lit(var, (solver->get_model()[var] == l_True)? true : false));\n }\n }\n solver->add_clause(ban_solution);\n}\n```\n\nThe above loop will run as long as there are solutions. It is __highly__\nsuggested to __only__ add into the new clause(`bad_solutions` above) the\nvariables that are \"important\" or \"main\" to your problem. Variables that were\nonly used to translate the original problem into CNF should not be added.\nThis way, you will not get spurious solutions that don't differ in the main,\nimportant variables.\n\nRust bindings\n-----\n\nTo build the Rust bindings:\n\n```\ngit clone https://github.com/msoos/cryptominisat-rs/\ncd cryptominisat-rs\ncargo build --release\ncargo test\n```\n\nYou can use it as per the [README](https://github.com/msoos/cryptominisat-rs/blob/master/README.markdown) in that repository. To include CryptoMiniSat in your Rust project, add the dependency to your `Cargo.toml` file:\n\n```\ncryptominisat = { git = \"https://github.com/msoos/cryptominisat-rs\", branch= \"master\" }\n```\n\nYou can see an example project using CryptoMiniSat in Rust [here](https://github.com/msoos/caqe/).\n\n\nPreprocessor usage\n-----\n\nRun cryptominisat5 as:\n\n```\n./cryptominisat5 -p1 input.cnf simplified.cnf\nsome_sat_solver simplified.cnf > output\n./cryptominisat5 -p2 output\n```\n\nwhere `some_sat_solver` is a SAT solver of your choice that outputs a solution in the format of:\n\n```\ns SATISFIABLE\nv [solution] 0\n```\n\nor\n\n```\ns UNSATISFIABLE\n```\n\nYou can tune the schedule of simplifications by issuing `--sched \"X,Y,Z...\"`. The default schedule for preprocessing is:\n\n```\nhandle-comps,scc-vrepl, cache-clean, cache-tryboth,sub-impl, intree-probe, probe,\nsub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl,occ-backw-sub-str,\nocc-xor, occ-clean-implicit, occ-bve, occ-bva, occ-gates,str-impl, cache-clean,\nsub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl,str-impl, sub-impl,\nsub-str-cls-with-bin, occ-backw-sub-str, occ-bve,check-cache-size, renumber\n```\n\nIt is a good idea to put `renumber` as late as possible, as it renumbers the variables for memory usage reduction.\n\nGauss-Jordan elimination\n-----\nSince CryptoMiniSat 5.8, Gauss-Jordan elimination is compiled into the solver by default. However, it will turn off automatically in case the solver observes GJ not to perform too well. To use Gaussian elimination, provide a CNF with xors in it (either in CNF or XOR+CNF form) and either run with default setup, or, tune it to your heart's desire:\n\n```\nGauss options:\n --iterreduce arg (=1) Reduce iteratively the matrix that is updated.We\n effectively are moving the start to the last\n column updated\n --maxmatrixrows arg (=3000) Set maximum no. of rows for gaussian matrix. Too\n large matrixes should be discarded for reasons of\n efficiency\n --autodisablegauss arg (=1) Automatically disable gauss when performing badly\n --minmatrixrows arg (=5) Set minimum no. of rows for gaussian matrix.\n Normally, too small matrixes are discarded for\n reasons of efficiency\n --savematrix arg (=2) Save matrix every Nth decision level\n --maxnummatrixes arg (=3) Maximum number of matrixes to treat.\n```\n\nIn particular, you may want to set `--autodisablegauss 0` in case you are sure it'll help.\n\nTesting\n-----\nFor testing you will need the GIT checkout and build as per:\n\n```\nsudo apt-get install build-essential cmake git\nsudo apt-get install zlib1g-dev libboost-program-options-dev libm4ri-dev libsqlite3-dev help2man\nsudo apt-get install git python3-pip python3-setuptools python3-dev\nsudo pip3 install --upgrade pip\nsudo pip3 install lit\ngit clone https://github.com/msoos/cryptominisat.git\ncd cryptominisat\ngit submodule update --init\nmkdir build && cd build\ncmake -DENABLE_TESTING=ON ..\nmake -j4\nmake test\nsudo make install\nsudo ldconfig\n```\n\nFuzzing\n-----\nBuild for test as per above, then:\n\n```\ncd ../cryptominisat/scripts/fuzz/\n./fuzz_test.py\n```\n\n\nCrystalBall\n-----\n\nBuild and use instructions below. Please see the [associated blog post](https://www.msoos.org/2019/06/crystalball-sat-solving-data-gathering-and-machine-learning/) for more information.\n\n```\n# prerequisites on a modern Debian/Ubuntu installation\nsudo apt-get install build-essential cmake git\nsudo apt-get install zlib1g-dev libsqlite3-dev\nsudo apt-get install libboost-program-options-dev\nsudo apt-get install python3-pip\nsudo pip3 install sklearn pandas numpy lit matplotlib\n\n# getting the code\ngit clone https://github.com/msoos/cryptominisat\ncd cryptominisat\ngit checkout crystalball\ngit submodule update --init\nmkdir build && cd build\nln -s ../scripts/crystal/* .\nln -s ../scripts/build_scripts/* .\n\n# Let's get an unsatisfiable CNF\nwget https://www.msoos.org/largefiles/goldb-heqc-i10mul.cnf.gz\ngunzip goldb-heqc-i10mul.cnf.gz\n\n# Gather the data, denormalize, label, output CSV,\n# create the classifier, generate C++,\n# and build the final SAT solver\n./ballofcrystal.sh --csv goldb-heqc-i10mul.cnf\n[...compilations and the full data pipeline...]\n\n# let's use our newly built tool\n# we are using configuration number short:3 long:3\n./cryptominisat5 --predshort 3 --predlong 3 goldb-heqc-i10mul.cnf\n[ ... ]\ns UNSATISFIABLE\n\n# Let's look at the data\ncd goldb-heqc-i10mul.cnf-dir\nsqlite3 mydata.db\nsqlite> select count() from sum_cl_use;\n94507\n```\n\nThe CNFs go through the following set of transformations to become the generated code:\n\n1. `./cryptominisat` dumps the data. Options: `--cldatadumpratio 0.08`, `--gluecut0 100`\n2. `./drat-trim`\n3. `./add_lemma_ind.py`\n4. `./clean_update_data.py`\n5. `./rem_data.py` Options: `--fair`, etc.\n6. `./vardata_gen_pandas.py`. Options: `--limit`\n7. `./gen_pandas.py` Options: `--limit`, `--confs`\n8. `./concat_pandas.py`\n9. `./predict.py` Options: `--forest/--tree/etc`, `--depth/--split/etc`\n\nConfiguring a build for a minimal binary&library\n-----\nThe following configures the system to build a bare minimal binary&library. It needs a compiler, but nothing much else:\n\n```\ncmake -DONLY_SIMPLE=ON -DNOZLIB=ON -DNOM4RI=ON -DSTATS=OFF -DNOVALGRIND=ON -DENABLE_TESTING=OFF .\n```\n\nCMake Arguments\n-----\nThe following arguments to cmake configure the generated build artifacts. To use, specify options prior to running make in a clean subdirectory: `cmake ..`\n\n- `-DSTATICCOMPILE=` -- statically linked library and binary\n- `-DUSE_GAUSS=` -- Gauss-Jordan Elimination support. On by default.\n- `-DSTATS=` -- advanced statistics (slower)\n- `-DENABLE_TESTING=` -- test suite support\n- `-DMIT=` -- MIT licensed components only\n- `-DNOM4RI=` -- without toplevel Gauss-Jordan Elimination support\n- `-DREQUIRE_M4RI=` -- abort if M4RI is not present\n- `-DNOZLIB=` -- no gzip DIMACS input support\n- `-DONLY_SIMPLE=` -- only the simple binary is built\n- `-DNOVALGRIND=` -- no extended valgrind memory checking support\n- `-DLARGEMEM=` -- more memory available for clauses (but slower on most problems)\n\nGetting learnt clauses\n-----\nAs an experimental feature, you can get the learnt clauses from the system with the following code, where `lits` is filled with learnt clauses every time `get_next_small_clause` is called. The example below will eventually return all clauses of size 4 or less. You can call `end_getting_small_clauses` at any time.\n\n```\nSATSolver s;\n//fill the solver, run solve, etc.\n\n//Get all clauses of size 4 or less\n\ns->start_getting_small_clauses(4);\n\nvector lits;\nbool ret = true;\nwhile (ret) {\n bool ret = s->get_next_small_clause(lits);\n if (ret) {\n //deal with clause in \"lits\"\n add_to_my_db(lits);\n }\n}\ns->end_getting_small_clauses();\n```\n\nC usage\n-----\nSee src/cryptominisat_c.h.in for details. This is an experimental feature.\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",9480583495,"orgData","recentTags",[87,125],{"_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":61,"_124":17},"content_type","creator",310244,"full_size",10869952,"id",15676722,"images",[97],{"_98":99,"_100":101,"_102":103,"_104":105,"_106":107,"_108":109,"_110":103,"_111":-5,"_112":92,"_59":61,"_113":-5},"architecture","amd64","digest","sha256:7261d86e2f8c35bf11492868f1b7c79151db2792b98b29047eda6fae6300a36b","features","","last_pulled","2026-09-24T22:39:31.041287468Z","last_pushed","2021-10-20T13:37:53Z","os","linux","os_features","os_version","size","variant","2021-10-20T13:37:52.491753Z","last_updater","last_updater_username","media_type","latest","repository",1848244,"tag_last_pulled","tag_last_pushed","tag_status","v2",{"_88":40,"_89":90,"_91":126,"_93":127,"_95":128,"_46":133,"_115":90,"_116":29,"_117":52,"_53":134,"_119":120,"_121":131,"_122":133,"_123":61,"_124":17},63680211,79129348,[129],{"_98":99,"_100":130,"_102":103,"_104":131,"_106":132,"_108":109,"_110":103,"_111":-5,"_112":126,"_59":61,"_113":-5},"sha256:ea27b276c467b1d1255b6e4f469471b9c7bb09b0204b0a351c022e20012f259b","2026-09-19T18:50:26.17087344Z","2019-12-09T03:08:48Z","2019-12-09T03:08:47.437838Z","winterschool","sbxKitMetadata","isPotentialSpam","isHubSbxKitsEnabled","showSbxLogoOverride","sbxTrademarkText","displaySecurityMetadata","tagAttestations","tagsHaveAttestations",[],"routes/_layout.r.$namespace.$reponame.tags",{"_34":146,"_153":154,"_142":167,"_168":11},{"_36":147,"_38":148,"_41":42,"_43":44,"_45":11,"_46":47,"_48":49,"_50":149,"_53":31,"_28":29,"_54":55,"_56":40,"_57":58,"_59":58,"_60":61,"_62":-5,"_63":64,"_65":66,"_67":11,"_68":29,"_69":150,"_75":11,"_76":152,"_81":29,"_82":83},[],[40],[52],{"_71":11,"_72":151},[74],{"_78":17,"_79":11,"_80":11},"tags",{"_155":156,"_157":-5,"_158":-5,"_159":160},"count",2,"next","previous","results",[161,164],{"_88":40,"_89":90,"_91":92,"_93":94,"_95":162,"_46":114,"_115":90,"_116":29,"_117":52,"_53":118,"_119":120,"_121":105,"_122":114,"_123":61,"_124":17},[163],{"_98":99,"_100":101,"_102":103,"_104":105,"_106":107,"_108":109,"_110":103,"_111":-5,"_112":92,"_59":61,"_113":-5},{"_88":40,"_89":90,"_91":126,"_93":127,"_95":165,"_46":133,"_115":90,"_116":29,"_117":52,"_53":134,"_119":120,"_121":131,"_122":133,"_123":61,"_124":17},[166],{"_98":99,"_100":130,"_102":103,"_104":131,"_106":132,"_108":109,"_110":103,"_111":-5,"_112":126,"_59":61,"_113":-5},[],"canDeleteTags","actionData","errors"]

msoos/cryptominisat

Tags for msoos/cryptominisat