The Curious Engineer

All blogs / Algorithms / data structures

Wonderings of a SAT geek

msoos.org

A blog about SAT solving and cryptography

Algorithms / data structuresMathSecurity

’10’15’20’25
Posts
155 from 12 Sep 2008 to 3 Oct 2026
Posting
now and then (3 in the last year)
Kind
personal blog
Feed
https://www.msoos.org/feed/

2026 3

  1. Incentives in Academic Research
  2. CryptoMiniSat on XNF Benchmarks, Revisited
  3. Ganak: The Making of a Versatile, High Performance Model Counter

2025 3

  1. Ganakv2 Released
  2. Ethereum in the age of AOL
  3. Computing Tricky Probabilities

2024 3

  1. Some food for thought: great content on the Internet
  2. On SAT/SMT Model Counting
  3. Our tools for solving, counting and sampling

2023 2

  1. The Inprocessing API of CryptoMiniSat
  2. Pepin, our Probabilistic Approximate Volume Counter

2022 4

  1. Arjun, our New CNF Model Counting Preprocessor
  2. Checking Uniform-Like Samplers
  3. A Tale of Shift Left, Shift Right, and MEV
  4. Proof Traces for SAT solvers

2021 1

  1. CMSGen, a Fast Uniform-Like Sampler

2020 1

  1. CryptoMiniSat 5.8.0 Released

2019 4

  1. Weighted to Unweighted Counting and Sampling
  2. CrystalBall: SAT solving, Data Gathering, and Machine Learning
  3. SAT Solvers as Smart Search Engines
  4. Bosphorus, an ANF and CNF simplifier and converter

2018 5

  1. How Approximate Model Counting Works
  2. ApproxMCv3, a modern approximate model counter
  3. The Cult of Security/Privacy By Design
  4. CryptoMiniSat and Parallel SAT Solving
  5. CryptoMiniSat 5.6.3 Released

2017 4

  1. IT Security Differently
  2. Testing and pentesting, a road to effectiveness
  3. Non-reproducible results with MapleCOMSPS
  4. Why Most Published Research Findings Are False

2016 6

  1. CryptoMiniSat 5.0.1 released — with MIT license
  2. Texas Executed Offenders’ Last Words
  3. CryptoMiniSat 5.0.0 released
  4. Eight Pro Tips on Creating Better Software
  5. Memory layout of clauses in MiniSat
  6. Benchmark randomisation for SAT Comp’16

2015 8

  1. On Testing and Security Engineering
  2. Testing CryptoMiniSat using GoogleTest
  3. CryptoMiniSat: 8000 commits later
  4. STP and CryptoMiniSat in the competitions of 2015
  5. Setting up encrypted mail in Chrome and Gmail
  6. Machine Learning and SAT
  7. Towards CryptoMiniSat 5.0
  8. The past half year of SAT and SMT

2014 12

  1. Faster cleaning of the learnt clause database
  2. TreeLook and transitive reduction
  3. On using less memory for binary clauses in lingeling’s watchlists
  4. CryptoMiniSat 4.2 released
  5. SMT Competition’14 and STP
  6. Multi-threading and startup speed
  7. Final polish of my SAT competition entry
  8. My SAT Competition 2014 entry
  9. Multi-threading
  10. Why it’s hard to eliminate variables
  11. CryptoMiniSat 4 released
  12. Speeding up MiniSat with a one-liner

2013 15

  1. On variable renumbering
  2. A note on learnt clauses
  3. MiniSat in your browser
  4. My SAT solver fuzzing setup
  5. Why CryptoMiniSat 3.3 doesn’t have XORs
  6. Handling disconnected components
  7. CryptoMiniSat 3.3 released
  8. Clause glues are a mystery to me
  9. CryptoMiniSat 3.2.0 released
  10. GCC 4.5.2 at the SAT Competition’13
  11. Certified UNSAT and CryptoMiniSat
  12. A variable elimination improvement
  13. CryptoMinisat 3.1 released
  14. CryptoMiniSat 3.0 released
  15. On benchmark randomization

2012 8

  1. Collecting solver data
  2. My Dell Vostro 3560 review
  3. How to use CryptoMiniSat 2.9 as a library
  4. Visualizing SAT solving
  5. Q-DIMM, an “innovation” by ASUS
  6. On hyper-binary resolution
  7. A nifty way of saving time with OpenCL
  8. AMD’s OpenCL heaven and hell

2011 19

  1. Thoughts on SAT@home
  2. CCC Camp’11
  3. Failed literal probing and UIP
  4. Note to self: higher level autarkies
  5. Learnt clause graphs
  6. Fun facts about SAT solving (part 1)
  7. CryptoMiniSat won two gold medals at SAT Comp’11
  8. Dreaming up a parallel SAT architecture
  9. Understanding Implication Graphs
  10. Presentation at Hackito Ergo Sum
  11. Come to Hackito Ergo Sum’11
  12. Recovering XORs from a CNF
  13. CryptoMiniSat in SAT Competition’11
  14. Visiting Linz
  15. Delayed updates
  16. On the New Watchlist Scheme
  17. CryptoMiniSat 2.9.0 released
  18. Changing the Watchlist Scheme
  19. The variable speed of SAT solving

2010 52

  1. Extended resolution is working!
  2. CCC madness
  3. Distributed SAT solving is fun
  4. Hyper-binary resolution: I was wrong, again
  5. Dependent Literals
  6. Caching
  7. The Cathedral
  8. Implicit binary clauses
  9. Wasting cluster time
  10. CryptoMiniSat 2.7.1 released
  11. Configuration management at IRILL days
  12. Open source software? Free software?
  13. Documenting CryptoMiniSat
  14. Transitive OTF self-subsuming resolution
  15. anf2cnf script released
  16. anf2cnf hell in Sage
  17. Reinventing the wheel
  18. FPGA programming and SAT
  19. Creating a SAT solver from scratch
  20. Truth table to ANF conversion
  21. CryptoMiniSat 2.6.0 released
  22. On-the-fly self-subsuming resolution
  23. Self-subsuming resolution
  24. Asymmetric branching
  25. Propagating faster
  26. Stats on CryptoMiniSat’s development
  27. Winning the SAT Race
  28. The 2010 SAT Conference
  29. ANF to CNF conversion
  30. How to bit-stuff pointers
  31. Propagating binary clauses
  32. Optimisations, take two
  33. The Obvious Child
  34. Why programs fail
  35. Being dumb is part of the deal
  36. I must be dumb
  37. On failed literal probing
  38. Gaussian elimination is released
  39. Parallelisation
  40. Social coding
  41. Blocked clause elimination implies dependent variable removal
  42. CryptoMiniSat v2 finally released
  43. On PrecoSat
  44. Optimisations
  45. Tools that I often use
  46. 216
  47. A great essay on security in the cyberworld
  48. The dates of the SAT Race 2010 have been announced!
  49. On research in general
  50. Why CryptoMiniSat can’t use MATLAB to do Gaussian elimination
  51. Could monomials be handled natively from SAT solvers?
  52. CryptoMiniSat v2

2008 5

  1. Why do I use Linux?
  2. How to unload the sound module
  3. KDE4 composite with intel drivers
  4. Suspend on Dell D430
  5. Synaptics