41554 blogs · [ { "id": "01a0c6a1-ae38-70d9-965b-8e204bf5fd65", "title": "CryptoMiniSat on XNF Benchmarks, Revisited", "url": "https://www.msoos.org/2026/09/cryptominisat-on-xnf-benchmarks-revisited/", "published_at": "2026-09-13T19:54:33+00:00" }, { "id": "01a087aa-2652-70fa-9182-43d39acbf04c", "title": "Ganak Architecture in Broad Strokes", "url": "https://www.msoos.org/2026/07/ganak-architecture-in-broad-strokes/", "published_at": "2026-07-18T15:31:03+00:00" }, { "id": "01a087aa-2652-70fa-9182-43d39bc8b2cf", "title": "Ganak: The Making of a Versatile, High Performance Model Counter", "url": "https://www.msoos.org/2026/03/ganak-the-making-of-a-versatile-high-performance-model-counter/", "published_at": "2026-03-01T18:34:45+00:00" }, { "id": "01a087aa-2652-70fa-9182-43d39c577822", "title": "Ganakv2 Released", "url": "https://www.msoos.org/2025/05/ganakv2-released/", "published_at": "2025-05-12T02:17:50+00:00" }, { "id": "01a087aa-2652-70fa-9182-43d39cd7ed12", "title": "Ethereum in the age of AOL", "url": "https://www.msoos.org/2025/03/ethereum-in-the-age-of-aol/", "published_at": "2025-03-21T09:56:20+00:00" }, { "id": "01a087aa-2652-70fa-9182-43d39dc4563e", "title": "Computing Tricky Probabilities", "url": "https://www.msoos.org/2025/02/computing-tricky-probabilities/", "published_at": "2025-02-09T14:33:24+00:00" }, { "id": "01a0bb97-996f-7039-965b-61e39b691250", "title": "Some food for thought: great content on the Internet", "url": "https://www.msoos.org/2024/12/some-food-for-thought-great-content-on-the-internet/", "published_at": "2024-12-19T21:49:39+00:00" }, { "id": "01a0bb97-996f-7039-965b-61e39c4117ad", "title": "On SAT/SMT Model Counting", "url": "https://www.msoos.org/2024/10/on-sat-smt-model-counting/", "published_at": "2024-10-24T22:18:14+00:00" }, { "id": "01a0bb97-996f-7039-965b-61e39c56c81f", "title": "Our tools for solving, counting and sampling", "url": "https://www.msoos.org/2024/02/our-tools-for-solving-counting-and-sampling/", "published_at": "2024-02-18T20:46:58+00:00" }, { "id": "01a0bb97-996f-7039-965b-61e39d02e012", "title": "The Inprocessing API of CryptoMiniSat", "url": "https://www.msoos.org/2023/10/the-inprocessing-api-of-cryptominisat/", "published_at": "2023-10-01T14:08:37+00:00" }, { "id": "01a0bb9f-de5e-70f6-9fe7-767c90bba465", "title": "Pepin, our Probabilistic Approximate Volume Counter", "url": "https://www.msoos.org/2023/09/pepin-our-probabilistic-approximate-volume-counter/", "published_at": "2023-09-23T19:24:06+00:00" }, { "id": "01a0bb9f-de5e-70f6-9fe7-767c910bfe9c", "title": "Arjun, our New CNF Model Counting Preprocessor", "url": "https://www.msoos.org/2022/08/arjun-our-new-cnf-model-counting-preprocessor/", "published_at": "2022-08-24T19:34:27+00:00" }, { "id": "01a0bb9f-de5e-70f6-9fe7-767c9129b069", "title": "Checking Uniform-Like Samplers", "url": "https://www.msoos.org/2022/06/checking-uniform-like-samplers/", "published_at": "2022-06-23T09:53:56+00:00" }, { "id": "01a0bb9f-de5e-70f6-9fe7-767c914eead0", "title": "A Tale of Shift Left, Shift Right, and MEV", "url": "https://www.msoos.org/2022/05/a-tale-of-shift-left-shift-right-and-mev/", "published_at": "2022-05-13T21:26:32+00:00" }, { "id": "01a0bb9f-de5e-70f6-9fe7-767c91d8a6c6", "title": "Proof Traces for SAT solvers", "url": "https://www.msoos.org/2022/04/proof-traces-for-sat-solvers/", "published_at": "2022-04-12T20:56:11+00:00" }, { "id": "01a0bba5-9407-714a-8547-d3d08a5608f2", "title": "CMSGen, a Fast Uniform-Like Sampler", "url": "https://www.msoos.org/2021/09/cmsgen-a-fast-uniform-like-sampler/", "published_at": "2021-09-18T09:03:22+00:00" }, { "id": "01a0bba5-9407-714a-8547-d3d08af8f7e5", "title": "CryptoMiniSat 5.8.0 Released", "url": "https://www.msoos.org/2020/07/cryptominisat-5-8-0-released/", "published_at": "2020-07-26T21:05:19+00:00" }, { "id": "01a0bba5-9407-714a-8547-d3d08b30245a", "title": "Weighted to Unweighted Counting and Sampling", "url": "https://www.msoos.org/2019/12/weighted-to-unweighted-counting-and-sampling/", "published_at": "2019-12-23T19:15:20+00:00" }, { "id": "01a0bba5-9407-714a-8547-d3d08bfa2ae7", "title": "CrystalBall: SAT solving, Data Gathering, and Machine Learning", "url": "https://www.msoos.org/2019/06/crystalball-sat-solving-data-gathering-and-machine-learning/", "published_at": "2019-06-14T18:34:17+00:00" }, { "id": "01a0bba5-9407-714a-8547-d3d08ced6695", "title": "SAT Solvers as Smart Search Engines", "url": "https://www.msoos.org/2019/02/sat-solvers-as-smart-search-engines/", "published_at": "2019-02-13T21:47:15+00:00" }, { "id": "01a0bbaa-9d03-710b-99d8-bbbb6b38029e", "title": "Bosphorus, an ANF and CNF simplifier and converter", "url": "https://www.msoos.org/2019/01/bosphorus-an-anf-and-cnf-simplifier-and-converter/", "published_at": "2019-01-04T23:46:12+00:00" }, { "id": "01a0bbaa-9d03-710b-99d8-bbbb6c134640", "title": "How Approximate Model Counting Works", "url": "https://www.msoos.org/2018/12/how-approximate-model-counting-works/", "published_at": "2018-12-09T14:39:21+00:00" }, { "id": "01a0bbaa-9d03-710b-99d8-bbbb6c972c1d", "title": "ApproxMCv3, a modern approximate model counter", "url": "https://www.msoos.org/2018/11/approxmcv3-a-modern-approximate-model-counter/", "published_at": "2018-11-25T20:33:16+00:00" }, { "id": "01a0bbaa-9d03-710b-99d8-bbbb6ca8dd11", "title": "The Cult of Security/Privacy By Design", "url": "https://www.msoos.org/2018/09/the-cult-of-security-privacy-by-design/", "published_at": "2018-09-13T17:21:03+00:00" }, { "id": "01a0bbaa-9d03-710b-99d8-bbbb6d855c44", "title": "CryptoMiniSat and Parallel SAT Solving", "url": "https://www.msoos.org/2018/07/cryptominisat-and-parallel-sat-solving/", "published_at": "2018-07-15T10:53:15+00:00" }, { "id": "01a0bbaf-9ef5-726e-8f6d-aeb9db79de2c", "title": "CryptoMiniSat 5.6.3 Released", "url": "https://www.msoos.org/2018/06/cryptominisat-5-6-3-released/", "published_at": "2018-06-11T07:21:29+00:00" }, { "id": "01a0bbaf-9ef5-726e-8f6d-aeb9db8fa87d", "title": "IT Security Differently", "url": "https://www.msoos.org/2017/12/security_differently/", "published_at": "2017-12-25T00:50:08+00:00" }, { "id": "01a0bbaf-9ef5-726e-8f6d-aeb9dc647dad", "title": "Testing and pentesting, a road to effectiveness", "url": "https://www.msoos.org/2017/05/testing-and-pentesting/", "published_at": "2017-05-27T11:06:30+00:00" }, { "id": "01a0bbaf-9ef5-726e-8f6d-aeb9dca80bb2", "title": "Non-reproducible results with MapleCOMSPS", "url": "https://www.msoos.org/2017/02/non-reproducible-maplecomsps/", "published_at": "2017-02-22T00:11:31+00:00" }, { "id": "01a0bbaf-9ef5-726e-8f6d-aeb9dd0f9563", "title": "Why Most Published Research Findings Are False", "url": "https://www.msoos.org/2017/01/why-most-published-research-false/", "published_at": "2017-01-27T00:10:02+00:00" }, { "id": "01a0bbb4-6f82-7208-8c18-c22874a9db37", "title": "CryptoMiniSat 5.0.1 released — with MIT license", "url": "https://www.msoos.org/2016/09/cryptominisat-5-0-1-released-with-mit-license/", "published_at": "2016-09-10T14:17:29+00:00" }, { "id": "01a0bbb4-6f82-7208-8c18-c22874c2e644", "title": "Texas Executed Offenders’ Last Words", "url": "https://www.msoos.org/2016/07/texas-executed-offenders-last-words/", "published_at": "2016-07-17T11:01:22+00:00" }, { "id": "01a0bbb4-6f82-7208-8c18-c22875487dd7", "title": "CryptoMiniSat 5.0.0 released", "url": "https://www.msoos.org/2016/07/cryptominisat-5-0-0-released/", "published_at": "2016-07-06T12:28:59+00:00" }, { "id": "01a0bbb4-6f82-7208-8c18-c22875f0f2f1", "title": "Eight Pro Tips on Creating Better Software", "url": "https://www.msoos.org/2016/04/eight-pro-tips-on-creating-better-software/", "published_at": "2016-04-05T19:45:13+00:00" }, { "id": "01a0bbb4-6f82-7208-8c18-c22876d3f8eb", "title": "Memory layout of clauses in MiniSat", "url": "https://www.msoos.org/2016/03/memory-layout-of-clauses-in-minisat/", "published_at": "2016-03-30T00:30:12+00:00" }, { "id": "01a0bbba-008e-7138-8d46-805c54e39c5e", "title": "Benchmark randomisation for SAT Comp’16", "url": "https://www.msoos.org/2016/03/benchmark-randomisation-sat-competition2016/", "published_at": "2016-03-07T22:00:27+00:00" }, { "id": "01a0bbba-008e-7138-8d46-805c559544bc", "title": "On Testing and Security Engineering", "url": "https://www.msoos.org/2015/11/on-testing-and-security-engineering/", "published_at": "2015-11-11T23:45:20+00:00" }, { "id": "01a0bbba-008e-7138-8d46-805c562f0ddc", "title": "Testing CryptoMiniSat using GoogleTest", "url": "https://www.msoos.org/2015/11/testing-cryptominisat-using-googletest/", "published_at": "2015-11-01T22:13:46+00:00" }, { "id": "01a0bbba-008e-7138-8d46-805c569f4a7b", "title": "CryptoMiniSat: 8000 commits later", "url": "https://www.msoos.org/2015/10/cryptominisat-8000-commits-later/", "published_at": "2015-10-18T18:36:23+00:00" }, { "id": "01a0bbba-008e-7138-8d46-805c56e43c39", "title": "STP and CryptoMiniSat in the competitions of 2015", "url": "https://www.msoos.org/2015/09/sat-race15-the-smt-comp15-cryptominisat-stp/", "published_at": "2015-09-26T15:11:31+00:00" }, { "id": "01a0bbbe-5bb9-71e2-8ee2-aff9855bd131", "title": "Setting up encrypted mail in Chrome and Gmail", "url": "https://www.msoos.org/2015/09/setting-up-encrypted-mail-in-chrome-and-gmail/", "published_at": "2015-09-05T20:29:45+00:00" }, { "id": "01a0bbbe-5bb9-71e2-8ee2-aff985969024", "title": "Machine Learning and SAT", "url": "https://www.msoos.org/2015/08/machine-learning-and-sat/", "published_at": "2015-08-09T10:25:47+00:00" }, { "id": "01a0bbbe-5bb9-71e2-8ee2-aff985e6aedb", "title": "Towards CryptoMiniSat 5.0", "url": "https://www.msoos.org/2015/06/towards-cryptominisat-5/", "published_at": "2015-06-14T15:42:40+00:00" }, { "id": "01a0bbbe-5bb9-71e2-8ee2-aff9861ef7eb", "title": "The past half year of SAT and SMT", "url": "https://www.msoos.org/2015/05/the-past-half-year-of-sat-and-smt/", "published_at": "2015-05-25T17:52:45+00:00" }, { "id": "01a0bbbe-5bb9-71e2-8ee2-aff98698373a", "title": "Faster cleaning of the learnt clause database", "url": "https://www.msoos.org/2014/11/cleaning-the-learnt-clause-database-faster/", "published_at": "2014-11-16T17:46:28+00:00" }, { "id": "01a0bbc2-d6ec-7348-bb47-d202c7afded5", "title": "TreeLook and transitive reduction", "url": "https://www.msoos.org/2014/08/treelook-and-transitive-reduction/", "published_at": "2014-08-23T16:53:28+00:00" }, { "id": "01a0bbc2-d6ec-7348-bb47-d202c7da03e5", "title": "On using less memory for binary clauses in lingeling’s watchlists", "url": "https://www.msoos.org/2014/08/on-using-less-memory-for-binary-clauses-in-lingeling/", "published_at": "2014-08-18T18:28:06+00:00" }, { "id": "01a0bbc2-d6ec-7348-bb47-d202c7fafd4c", "title": "CryptoMiniSat 4.2 released", "url": "https://www.msoos.org/2014/07/cryptominisat-4-2-released/", "published_at": "2014-07-17T00:43:07+00:00" }, { "id": "01a0bbc2-d6ec-7348-bb47-d202c815757a", "title": "SMT Competition’14 and STP", "url": "https://www.msoos.org/2014/06/smt-competition14-and-stp/", "published_at": "2014-06-24T22:27:18+00:00" }, { "id": "01a0bbc2-d6ec-7348-bb47-d202c8b31065", "title": "Multi-threading and startup speed", "url": "https://www.msoos.org/2014/05/multi-threading-and-startup-speed/", "published_at": "2014-05-16T16:10:31+00:00" }, { "id": "01a0bbc9-db23-71da-a44c-f264408b7c74", "title": "Final polish of my SAT competition entry", "url": "https://www.msoos.org/2014/05/final-polish-of-sat-competition-2014-entry/", "published_at": "2014-05-05T18:01:20+00:00" }, { "id": "01a0bbc9-db23-71da-a44c-f264414d8fd7", "title": "My SAT Competition 2014 entry", "url": "https://www.msoos.org/2014/04/my-sat-competition-2014-entry/", "published_at": "2014-04-29T06:13:09+00:00" }, { "id": "01a0bbc9-db23-71da-a44c-f2644238ab92", "title": "Multi-threading", "url": "https://www.msoos.org/2014/04/multi-threading/", "published_at": "2014-04-22T23:04:18+00:00" }, { "id": "01a0bbc9-db23-71da-a44c-f26442eb88e7", "title": "Why it’s hard to eliminate variables", "url": "https://www.msoos.org/2014/04/why-its-hard-to-eliminate-variables/", "published_at": "2014-04-16T15:39:47+00:00" }, { "id": "01a0bbc9-db23-71da-a44c-f26443ae6d7e", "title": "CryptoMiniSat 4 released", "url": "https://www.msoos.org/2014/04/cryptominisat-4-released/", "published_at": "2014-04-09T20:07:20+00:00" }, { "id": "01a0bbce-e3a4-700d-b7ee-47ba75428b84", "title": "Speeding up MiniSat with a one-liner", "url": "https://www.msoos.org/2014/03/speeding-up-minisat-with-a-one-liner/", "published_at": "2014-03-12T22:31:28+00:00" }, { "id": "01a0bbce-e3a4-700d-b7ee-47ba7634f298", "title": "On variable renumbering", "url": "https://www.msoos.org/2013/12/on-variable-renumbering/", "published_at": "2013-12-18T01:34:15+00:00" }, { "id": "01a0bbce-e3a4-700d-b7ee-47ba76cfec84", "title": "A note on learnt clauses", "url": "https://www.msoos.org/2013/12/a-note-on-learnt-clauses/", "published_at": "2013-12-06T17:29:24+00:00" }, { "id": "01a0bbce-e3a4-700d-b7ee-47ba76e71c91", "title": "MiniSat in your browser", "url": "https://www.msoos.org/2013/09/minisat-in-your-browser/", "published_at": "2013-09-29T19:37:34+00:00" }, { "id": "01a0bbce-e3a4-700d-b7ee-47ba76f932cb", "title": "My SAT solver fuzzing setup", "url": "https://www.msoos.org/2013/08/my-sat-solver-fuzzing-setup/", "published_at": "2013-08-25T15:12:03+00:00" }, { "id": "01a0bbd2-c621-710b-abbc-4d5b27f850bc", "title": "Why CryptoMiniSat 3.3 doesn’t have XORs", "url": "https://www.msoos.org/2013/08/why-cryptominisat-3-3-doesnt-have-xors/", "published_at": "2013-08-01T10:23:12+00:00" }, { "id": "01a0bbd2-c621-710b-abbc-4d5b2891777e", "title": "Handling disconnected components", "url": "https://www.msoos.org/2013/07/handling-disconnected-components/", "published_at": "2013-07-31T12:06:52+00:00" }, { "id": "01a0bbd2-c621-710b-abbc-4d5b2944b95f", "title": "CryptoMiniSat 3.3 released", "url": "https://www.msoos.org/2013/07/cryptominisat-3-3-released/", "published_at": "2013-07-10T18:52:36+00:00" }, { "id": "01a0bbd2-c621-710b-abbc-4d5b2a42ee42", "title": "Clause glues are a mystery to me", "url": "https://www.msoos.org/2013/07/clause-glues-are-a-mystery-to-me/", "published_at": "2013-07-08T16:48:41+00:00" }, { "id": "01a0bbd2-c621-710b-abbc-4d5b2af2b033", "title": "CryptoMiniSat 3.2.0 released", "url": "https://www.msoos.org/2013/04/cryptominisat-3-2-0-released/", "published_at": "2013-04-29T20:12:58+00:00" }, { "id": "01a0bbd6-9ce8-7160-b3ee-d5bf3543557f", "title": "GCC 4.5.2 at the SAT Competition’13", "url": "https://www.msoos.org/2013/04/gcc-4-5-2-at-sat-competition-201/", "published_at": "2013-04-26T23:17:35+00:00" }, { "id": "01a0bbd6-9ce9-7350-8244-d7c8d891c345", "title": "Certified UNSAT and CryptoMiniSat", "url": "https://www.msoos.org/2013/04/certified-unsat-and-cryptominisat/", "published_at": "2013-04-25T19:49:13+00:00" }, { "id": "01a0bbd6-9ce9-7350-8244-d7c8d91ed159", "title": "A variable elimination improvement", "url": "https://www.msoos.org/2013/04/a-variable-elimination-improvement/", "published_at": "2013-04-21T15:55:57+00:00" }, { "id": "01a0bbd6-9ce9-7350-8244-d7c8d98e607d", "title": "CryptoMinisat 3.1 released", "url": "https://www.msoos.org/2013/04/cryptominisat-3-1-released/", "published_at": "2013-04-14T17:29:50+00:00" }, { "id": "01a0bbd6-9ce9-7350-8244-d7c8da05d6fc", "title": "CryptoMiniSat 3.0 released", "url": "https://www.msoos.org/2013/04/cryptominisat-3-0-released/", "published_at": "2013-04-01T15:57:57+00:00" }, { "id": "01a0bbda-4911-722b-91db-fdf1210a1adc", "title": "On benchmark randomization", "url": "https://www.msoos.org/2013/03/on-benchmark-randomization/", "published_at": "2013-03-10T14:10:11+00:00" }, { "id": "01a0bbda-4911-722b-91db-fdf12184bfa9", "title": "Collecting solver data", "url": "https://www.msoos.org/2012/11/collecting-solver-data/", "published_at": "2012-11-21T16:02:09+00:00" }, { "id": "01a0bbda-4911-722b-91db-fdf121d578f2", "title": "My Dell Vostro 3560 review", "url": "https://www.msoos.org/2012/08/my-dell-vostro-3560-review/", "published_at": "2012-08-26T14:11:21+00:00" }, { "id": "01a0bbda-4911-722b-91db-fdf122cc32cc", "title": "How to use CryptoMiniSat 2.9 as a library", "url": "https://www.msoos.org/2012/06/how-to-use-cryptominisat-2-9-as-a-library/", "published_at": "2012-06-20T10:43:29+00:00" }, { "id": "01a0bbda-4911-722b-91db-fdf122f0202b", "title": "Visualizing SAT solving", "url": "https://www.msoos.org/2012/06/visualizing-sat-solving/", "published_at": "2012-06-16T13:02:55+00:00" }, { "id": "01a0bbdd-ed86-7101-b357-8819c9b46243", "title": "Q-DIMM, an “innovation” by ASUS", "url": "https://www.msoos.org/2012/05/q-dimm-an-innovation-by-asus/", "published_at": "2012-05-27T14:55:40+00:00" }, { "id": "01a0bbdd-ed86-7101-b357-8819ca51d692", "title": "On hyper-binary resolution", "url": "https://www.msoos.org/2012/05/on-hyper-binary-resolution/", "published_at": "2012-05-17T09:34:01+00:00" }, { "id": "01a0bbdd-ed86-7101-b357-8819ca536b99", "title": "A nifty way of saving time with OpenCL", "url": "https://www.msoos.org/2012/01/a-nifty-way-of-saving-time-with-opencl/", "published_at": "2012-01-17T21:14:17+00:00" }, { "id": "01a0bbdd-ed86-7101-b357-8819cb13d267", "title": "AMD’s OpenCL heaven and hell", "url": "https://www.msoos.org/2012/01/amds-opencl-heaven-and-hell/", "published_at": "2012-01-05T21:01:17+00:00" }, { "id": "01a0bbdd-ed86-7101-b357-8819cbb39e32", "title": "Thoughts on SAT@home", "url": "https://www.msoos.org/2011/12/thoughts-on-sat-at-home/", "published_at": "2011-12-11T21:05:58+00:00" }, { "id": "01a0bbe1-4bac-7233-bcec-5a964e2cf670", "title": "CCC Camp’11", "url": "https://www.msoos.org/2011/08/ccc-camp11/", "published_at": "2011-08-15T20:17:41+00:00" }, { "id": "01a0bbe1-4bac-7233-bcec-5a964ed99c23", "title": "Failed literal probing and UIP", "url": "https://www.msoos.org/2011/08/failed-literal-probing-and-uip/", "published_at": "2011-08-04T09:50:02+00:00" }, { "id": "01a0bbe1-4bac-7233-bcec-5a964f624acb", "title": "Note to self: higher level autarkies", "url": "https://www.msoos.org/2011/07/note-to-self-higher-level-autarkies/", "published_at": "2011-07-16T11:22:46+00:00" }, { "id": "01a0bbe1-4bac-7233-bcec-5a964fa1dc9a", "title": "Learnt clause graphs", "url": "https://www.msoos.org/2011/07/learnt-clause-graphs/", "published_at": "2011-07-07T15:31:19+00:00" }, { "id": "01a0bbe1-4bac-7233-bcec-5a964fa5561d", "title": "Fun facts about SAT solving (part 1)", "url": "https://www.msoos.org/2011/07/fun-facts-about-sat-solving-part-1/", "published_at": "2011-07-01T14:33:49+00:00" }, { "id": "01a0bbe4-83f5-70cc-a6fb-2d66266386f8", "title": "CryptoMiniSat won two gold medals at SAT Comp’11", "url": "https://www.msoos.org/2011/06/cryptominisat-won-two-gold-medals-at-sat-comp11/", "published_at": "2011-06-27T16:49:58+00:00" }, { "id": "01a0bbe4-83f5-70cc-a6fb-2d6626d465ee", "title": "Dreaming up a parallel SAT architecture", "url": "https://www.msoos.org/2011/06/dreaming-up-a-parallel-sat-architecture/", "published_at": "2011-06-06T12:26:15+00:00" }, { "id": "01a0bbe4-83f5-70cc-a6fb-2d66275964a2", "title": "Understanding Implication Graphs", "url": "https://www.msoos.org/2011/05/understanding-implication-graphs/", "published_at": "2011-05-27T22:18:17+00:00" }, { "id": "01a0bbe4-83f5-70cc-a6fb-2d6627f0e710", "title": "Presentation at Hackito Ergo Sum", "url": "https://www.msoos.org/2011/04/presentation-at-hackito-ergo-sum/", "published_at": "2011-04-13T18:04:56+00:00" }, { "id": "01a0bbe4-83f5-70cc-a6fb-2d662864ce0c", "title": "Come to Hackito Ergo Sum’11", "url": "https://www.msoos.org/2011/03/come-to-hackito-ergo-sum11/", "published_at": "2011-03-28T12:07:06+00:00" }, { "id": "01a0bbe7-be85-71d9-8602-f78aa9afad63", "title": "Recovering XORs from a CNF", "url": "https://www.msoos.org/2011/03/recovering-xors-from-a-cnf/", "published_at": "2011-03-16T17:53:33+00:00" }, { "id": "01a0bbe7-be85-71d9-8602-f78aa9fdb6e4", "title": "CryptoMiniSat in SAT Competition’11", "url": "https://www.msoos.org/2011/03/cryptominisat-in-sat-competition11/", "published_at": "2011-03-06T18:21:47+00:00" }, { "id": "01a0bbe7-be85-71d9-8602-f78aaa8e7e23", "title": "Visiting Linz", "url": "https://www.msoos.org/2011/02/visiting-linz/", "published_at": "2011-02-15T13:52:40+00:00" }, { "id": "01a0bbe7-be85-71d9-8602-f78aaac9e1f3", "title": "Delayed updates", "url": "https://www.msoos.org/2011/02/delayed-updates/", "published_at": "2011-02-05T21:38:50+00:00" }, { "id": "01a0bbe7-be85-71d9-8602-f78aab2bb3c3", "title": "On the New Watchlist Scheme", "url": "https://www.msoos.org/2011/01/on-the-new-watchlist-scheme/", "published_at": "2011-01-23T10:12:24+00:00" }, { "id": "01a0bbeb-f2f8-72ae-9807-bd6e7a45922b", "title": "CryptoMiniSat 2.9.0 released", "url": "https://www.msoos.org/2011/01/cryptominisat-2-9-0-released/", "published_at": "2011-01-20T22:41:57+00:00" }, { "id": "01a0bbeb-f2f8-72ae-9807-bd6e7ab82289", "title": "Changing the Watchlist Scheme", "url": "https://www.msoos.org/2011/01/changing-the-watchlist-scheme/", "published_at": "2011-01-14T12:18:59+00:00" }, { "id": "01a0bbeb-f2f8-72ae-9807-bd6e7ad4bb0c", "title": "The variable speed of SAT solving", "url": "https://www.msoos.org/2011/01/the-variable-speed-of-sat-solving/", "published_at": "2011-01-02T22:37:46+00:00" }, { "id": "01a0bbeb-f2f8-72ae-9807-bd6e7b58f1e7", "title": "Extended resolution is working!", "url": "https://www.msoos.org/2010/12/extended-resolution-is-working/", "published_at": "2010-12-28T22:13:08+00:00" }, { "id": "01a0bbeb-f2f8-72ae-9807-bd6e7bb958ca", "title": "CCC madness", "url": "https://www.msoos.org/2010/12/ccc-madness/", "published_at": "2010-12-26T23:04:47+00:00" } ] posts Claim your blog

Back to msoos.org

Blog · corpus.blog/blogs/msoos.org/posts

msoos.org

msoos.org

2026

CryptoMiniSat on XNF Benchmarks, Revisited original ↗

13 Sept 2026

Ganak Architecture in Broad Strokes original ↗

18 Jul 2026

Ganak: The Making of a Versatile, High Performance Model Counter original ↗

1 Mar 2026

2025

Ganakv2 Released original ↗

12 May 2025

Ethereum in the age of AOL original ↗

21 Mar 2025

Computing Tricky Probabilities original ↗

9 Feb 2025

2024

Some food for thought: great content on the Internet original ↗

19 Dec 2024

On SAT/SMT Model Counting original ↗

24 Oct 2024

Our tools for solving, counting and sampling original ↗

18 Feb 2024

2023

The Inprocessing API of CryptoMiniSat original ↗

1 Oct 2023

Pepin, our Probabilistic Approximate Volume Counter original ↗

23 Sept 2023

2022

Arjun, our New CNF Model Counting Preprocessor original ↗

24 Aug 2022

Checking Uniform-Like Samplers original ↗

23 Jun 2022

A Tale of Shift Left, Shift Right, and MEV original ↗

13 May 2022

Proof Traces for SAT solvers original ↗

12 Apr 2022

2021

CMSGen, a Fast Uniform-Like Sampler original ↗

18 Sept 2021

2020

CryptoMiniSat 5.8.0 Released original ↗

26 Jul 2020

2019

Weighted to Unweighted Counting and Sampling original ↗

23 Dec 2019

CrystalBall: SAT solving, Data Gathering, and Machine Learning original ↗

14 Jun 2019

SAT Solvers as Smart Search Engines original ↗

13 Feb 2019

Bosphorus, an ANF and CNF simplifier and converter original ↗

4 Jan 2019

2018

How Approximate Model Counting Works original ↗

9 Dec 2018

ApproxMCv3, a modern approximate model counter original ↗

25 Nov 2018

The Cult of Security/Privacy By Design original ↗

13 Sept 2018

CryptoMiniSat and Parallel SAT Solving original ↗

15 Jul 2018

CryptoMiniSat 5.6.3 Released original ↗

11 Jun 2018

2017

IT Security Differently original ↗

25 Dec 2017

Testing and pentesting, a road to effectiveness original ↗

27 May 2017

Non-reproducible results with MapleCOMSPS original ↗

22 Feb 2017

Why Most Published Research Findings Are False original ↗

27 Jan 2017

2016

CryptoMiniSat 5.0.1 released — with MIT license original ↗

10 Sept 2016

Texas Executed Offenders’ Last Words original ↗

17 Jul 2016

CryptoMiniSat 5.0.0 released original ↗

6 Jul 2016

Eight Pro Tips on Creating Better Software original ↗

5 Apr 2016

Memory layout of clauses in MiniSat original ↗

30 Mar 2016

Benchmark randomisation for SAT Comp’16 original ↗

7 Mar 2016

2015

On Testing and Security Engineering original ↗

11 Nov 2015

Testing CryptoMiniSat using GoogleTest original ↗

1 Nov 2015

CryptoMiniSat: 8000 commits later original ↗

18 Oct 2015

STP and CryptoMiniSat in the competitions of 2015 original ↗

26 Sept 2015

Setting up encrypted mail in Chrome and Gmail original ↗

5 Sept 2015

Machine Learning and SAT original ↗

9 Aug 2015

Towards CryptoMiniSat 5.0 original ↗

14 Jun 2015

The past half year of SAT and SMT original ↗

25 May 2015

2014

Faster cleaning of the learnt clause database original ↗

16 Nov 2014

TreeLook and transitive reduction original ↗

23 Aug 2014

On using less memory for binary clauses in lingeling’s watchlists original ↗

18 Aug 2014

CryptoMiniSat 4.2 released original ↗

17 Jul 2014

SMT Competition’14 and STP original ↗

24 Jun 2014

Multi-threading and startup speed original ↗

16 May 2014

Final polish of my SAT competition entry original ↗

5 May 2014

My SAT Competition 2014 entry original ↗

29 Apr 2014

Multi-threading original ↗

22 Apr 2014

Why it’s hard to eliminate variables original ↗

16 Apr 2014

CryptoMiniSat 4 released original ↗

9 Apr 2014

Speeding up MiniSat with a one-liner original ↗

12 Mar 2014

2013

On variable renumbering original ↗

18 Dec 2013

A note on learnt clauses original ↗

6 Dec 2013

MiniSat in your browser original ↗

29 Sept 2013

My SAT solver fuzzing setup original ↗

25 Aug 2013

Why CryptoMiniSat 3.3 doesn’t have XORs original ↗

1 Aug 2013

Handling disconnected components original ↗

31 Jul 2013

CryptoMiniSat 3.3 released original ↗

10 Jul 2013

Clause glues are a mystery to me original ↗

8 Jul 2013

CryptoMiniSat 3.2.0 released original ↗

29 Apr 2013

GCC 4.5.2 at the SAT Competition’13 original ↗

26 Apr 2013

Certified UNSAT and CryptoMiniSat original ↗

25 Apr 2013

A variable elimination improvement original ↗

21 Apr 2013

CryptoMinisat 3.1 released original ↗

14 Apr 2013

CryptoMiniSat 3.0 released original ↗

1 Apr 2013

On benchmark randomization original ↗

10 Mar 2013

2012

Collecting solver data original ↗

21 Nov 2012

My Dell Vostro 3560 review original ↗

26 Aug 2012

How to use CryptoMiniSat 2.9 as a library original ↗

20 Jun 2012

Visualizing SAT solving original ↗

16 Jun 2012

Q-DIMM, an “innovation” by ASUS original ↗

27 May 2012

On hyper-binary resolution original ↗

17 May 2012

A nifty way of saving time with OpenCL original ↗

17 Jan 2012

AMD’s OpenCL heaven and hell original ↗

5 Jan 2012

2011

Thoughts on SAT@home original ↗

11 Dec 2011

CCC Camp’11 original ↗

15 Aug 2011

Failed literal probing and UIP original ↗

4 Aug 2011

Note to self: higher level autarkies original ↗

16 Jul 2011

Learnt clause graphs original ↗

7 Jul 2011

Fun facts about SAT solving (part 1)original ↗

1 Jul 2011

CryptoMiniSat won two gold medals at SAT Comp’11 original ↗

27 Jun 2011

Dreaming up a parallel SAT architecture original ↗

6 Jun 2011

Understanding Implication Graphs original ↗

27 May 2011

Presentation at Hackito Ergo Sum original ↗

13 Apr 2011

Come to Hackito Ergo Sum’11 original ↗

28 Mar 2011

Recovering XORs from a CNF original ↗

16 Mar 2011

CryptoMiniSat in SAT Competition’11 original ↗

6 Mar 2011

Visiting Linz original ↗

15 Feb 2011

Delayed updates original ↗

5 Feb 2011

On the New Watchlist Scheme original ↗

23 Jan 2011

CryptoMiniSat 2.9.0 released original ↗

20 Jan 2011

Changing the Watchlist Scheme original ↗

14 Jan 2011

The variable speed of SAT solving original ↗

2 Jan 2011

2010

Extended resolution is working!original ↗

28 Dec 2010

CCC madness original ↗

26 Dec 2010