Tag Archives: CNF

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

Development, Research, Tools, ,

Ganak (github), our propositional model counter, has won every single model counting competition track for the past two years. Perhaps it’s time to explain how that came about, and what are the ingredients of such a tool. Firstly, a propositional model counter is a tool that counts how many solutions there are to a set of boolean constraints of the form:

a V b
b V -c

This set of constraints has the following possible solutions:

abc
---
000
001
010
011
100
101
110
111

But the ones highlighted in bold are not solutions, because the constraints make them incorrect. So we are left with 8-3=5 solutions. There is one more twist. Sometimes, we are only interested in the solutions over a set of variables, which we will call the sampling set, say “a” and “b”. Then we are only left with the solutions “01x”, “10x”, and “11x”, a total of 3 solutions, where “x” means we don’t care about the value , since it’s not in the sampling set.

The History of the Preprocessor: Arjun

Arjun (github) came about because we saw the B+E tool doing minimisation of the sampling set. Minimising the sampling set is important, because if the sampling set is e.g. only of size 10, then there are at most 2^10 things to count, but if it’s 20, then there are 2^20. It’s possible to minimise the sampling set sometimes: for example when we can prove that e.g. a=b, there is no need to have both “a” and “b” in the sampling set. Tricks like this can significantly lower the complexity of counting solutions. We enhanced B+E, and published this as a paper here.

In the end, it turned out that minimising the sampling set was really only the beginning: we also needed to make the input smaller. The fewer the constraints, and the fewer the number of variables, the easier it is to deal with the formula. This was not new to anyone, but it turns out that this minimisation was hard. Others have tried, too, but my advantage was that I came from the SAT world, with the CryptoMiniSat SAT solver under my belt, so I wrote an entire API (blogpost) for my SAT solver to be used as an input minimiser. This allowed me to try out many heuristics and write code easily, taking advantage of all the datastructures already inside CryptoMiniSat for constraint handling.

The History of the Counter: Ganak

The actual counter, Ganak (github), was something of another story. It started with a hack that my long-time collaborator Kuldeep Meel and I did in 2018, for a long evening and night in Singapore. This lead to the original Ganak paper which essentially added hashing to the system, thereby making it probabilistic, but also use a lot less memory, and thereby faster. I personally haven’t touched that project much, and instead focussed all my energies on the preprocessor, Arjun. I was pretty convinced that if I could make the preprocessor good enough, no matter what Ganak looked like, it would be good enough.

This strategy of focussing on Arjun mostly paid out, we did well in model counting competitions. The counter d4 was the main competitor at the time. Then SharpSAT-TD (paper) by Korhonen and Jarvisalo and came and it blew everything out of the water. That made me look at the Ganak source code first time in about 5 years, and I was appalled. We were putting a donkey, Ganak, on the rocket, Arjun, that I built, and we were doing OK, but looking at SharpSAT-TD, we were clearly racing a donkey against a cheetah. So In the spring of 2023 I sat down one morning and started replacing things I hated about Ganak, which was mostly everything.

Thus, the Ganak we know today was born. This gradual rewriting took about 2-3 years, continued during the summer and then the next spring. The most significant parts of this rewrite were that we cleaned up the code, added extensive fuzzing and debugging capabilities to it, added/adapted a lot of well-known SAT tricks for counting, integrated the tree decomposition (“TD”) system and parts of the preprocessor from SharpSAT-TD, and came up with a way to not only minimise the sampling set, but also the extend it, which can help in certain cases.

Ideas in Ganak and Arjun

We wrote a paper about Ganak (paper here) but to be honest, it only covers a very small ground of what we did. The change to Ganak between the original paper in 2019 to today is about 30’000 lines of code. Obviously, that cannot be explained in detail in just a few pages. Furthermore, the way academic publishing works, it’s not possible to simply list a bunch of ideas that were implemented — you need to explain everything in detail, which cannot be done with 30’000 lines of code. So, below is a bit of an “idea dump” that I have implemented in Ganak, but never published.

I might attempt at publishing some of them some day. Currently, I see little reward for doing so besides citations, and citations are not a great indicator in my view: lcamtuf is one of the best IT security professionals, ever, and has basically no citations. Besides, due to the “publish or perish” system in academia, there is a sea of research papers that most work gets lost in. I believe what matters most is performance and usability. Ganak does pretty well in this regard. It compiles to many platforms: Linux, Mac, both ARM and x86, and even emscripten in your browser. It supports more weight systems than other counters: integers, floats, exact rationals, complex numbers, primes, and multivariate polynomials over the rationals and floats. Ganak also uses less memory than other competing counters, while running faster. Besides, it’s regularly fuzzed and leaks no memory, so its output is rather trustworthy.

Without further ado, here are some ideas never published in Ganak, but which help the system run faster:

  • Using and improving the Oracle SAT Solver Korhonen and Jarvisalo (PDF by the authors). Oracle is a specialised SAT solver that allows one to query with many so-called “assumptions” in the SAT query, i.e. checking if something is satisfiable under conditions such as “a=true, b=false” — but many-many of them. This kind of query is very slow if you use a normal SAT solver, but with Oracle, it’s super-fast. This allows us to remove unneeded constraints, and make the constraints smaller. I improved this tool in a few ways, mostly by integrating a local search solver into it, that can drastically speed it up, by finding a satisfying solution much faster. I have also improved its heuristics, e.g. by using a better LBD heuristic (PDF by authors). I have also improved its solution cache, by employing cache performance tracking, pre-filtering, and cache size limitation. Besides, I added a step-tracking to it so it can be deterministically limited in time.
  • Improved version of tree decomposition originally by Korhonen and Jarvisalo (PDF here). This system computes the tree decomposition of a CNF via Flow-Cutter by Ben Strasser (PDF, code), however, the original system had a few issues. Firstly, it did a clock-limited run of the executable, which was unacceptable to me, as it makes the system non-deterministic: depending on the CPU it will run faster/slower thereby computing different values (it’s a local search algorithm, with many restarts). Also, running separate executables is very fragile. Secondly, and more importantly, it computed the tree decomposition of a CNF and then tried to find its centroid. But… what if the CNF was disjoint? What’s the single centroid of a forest? Slight issue. I fixed this by computing the top-level disjoint components and counting them separately. Although disjoint components sound really like an input issue, and not a counter issue, the problem is that our preprocessing is so strong that it can make a non-disjoint input into a disjoint input, thereby confusing the TD/centroid finding. Ooops.
  • Special-casing some inputs. Because we detect disjoint top-level components, sometimes we end up with CNFs that are very weird, for example, with a sampling set size of 2. These CNFs can only have at most 4 solutions, so counting them via the incredibly complicated d-DNNF system is an overkill, likely to waste a lot of time via the start-up and tear-down. Hence, these CNFs are counted one-by-one via the trivial use of a standard SAT solver.
  • Using CCNR by Shaowei Cai (PDF by authors) for speeding up the Oracle query. It’s a cool local search system, and it works really well. I wish I had fixed up its code because it’s a bit clunky and my colleagues gave me a hard time for it. Not research colleagues, of course. In research, quality of code is irrelevant — remember, only the number of citations matters.
  • Adapting Vivification by Li et al. (PDF paper) to the model counting setting. The original system stops the SAT solver once when the solver restarts, rewrites all the clauses to be shorter when possible, and continues happily every after. This happily ever after is impossible in a model counting setting, because we never restart. Slight issue. What I wrote was basically a nightmare-fuelled 2-week, probably about ~2000 line craziness that rewrites the propagation tree and/or avoids the clause improvement, so that all the invariants of the propagation remain intact while the clauses get shorter. This is kind of like changing the wheels on a car while it’s running. I don’t recommend doing this without extremely thorough fuzzing and debug tooling in place, or you’ll run into a lot of trouble. (By the way, this system not only contracts clauses, but also performs subsumption — if I have built the system, I might as well use it all the way)
  • Using an virtual interface for the Field we are counting over. With this system, the Field we are counting over becomes irrelevant for the counter. Instead, the counter can focus on counting, and the implementation of the interface can focus on the Field-specific operations. This has allowed me to add many-many Fields with very little overhead. The Field parses, prints, and handles the 0, and 1 points, and the + and * operators. This separation of concerns is I think the right way to go. Also, it allows someone to implement their own Field and use it without having to recompile anything.
  • Zero-suppressed Field counting. When counting over a field, there are two special elements one needs to take care of: zero and one. Of this, the zero is quite special, because a+0=a, and a*0=0. So, in Ganak, we don’t initialise the zero field element. Instead, we keep it as a null pointer. When manipulating this pointer, like adding or multiplying, we can simply replace it with a copy of what we add to it, or, when multiplying, keep it a null pointer. This saves space and also reduces the number of pointer dereferences we need to perform.
  • Extensive fuzzing infrastructure by Latour et al (code), with ideas taken from Niemetz at al (PDF here). Ganak and Arjun both have many options that allow the fuzzer to turn off certain parts of the system, or push them to the extreme, thereby exercising parts of them that would otherwise be impossible to reach. The paper I linked to explains how adding the options to the fuzzer, and setting them to all sorts of values, can help the fuzzer reach very hard-to-reach parts of the code, thereby exposing bugs in them easier.
  • Extensive debug infrastructure. Finding issues via fuzzing is only part of the deal, one must also be able to debug them. For this, Ganak has a 4-level debug system where progressively slower self-checking can be turned on so as to find the first place where the bug manifests itself as precisely as possible. The last level of debug checks every single node in the d-DNNF that Ganak builds, and exits out on the first node that the count is incorrect. The debug infrastructure also comes with a verbosity option that prints out full, human readable, structured, coloured logs for each major decision point in the d-DNNF. Overall, just the debug code of Ganak is likely 2-3 thousand lines of code. This may sound excessive, but Ganak can self-check its state at every node, and ensure that there is at least a path forward to counting the correct count, at almost all nodes. Apparently some have attempted to do what we did in our paper on Ganak, but bumped into issues they couldn’t resolve. I can confirm that without the appropriate fuzz and debug infrastructure, it would have been impossible for us to figure the things out we published in that paper.
  • Cache-optimised, lazy component finding. When a decision and propagation happens in the CNF, we must check whether the system has fallen into disjoint components. If so, we can count the components separately, and then multiply their counts — a property of a Field. This greatly helps in doing a lot less work. However, this means we must examine every single variable in the system, and see if it’s connected to the others through clauses at every node — often millions, or even 100s of millions of times during counting. Normally, d-DNNF counters do this by going through all the so-called occurrence list of all variables, recursively, and see if they encounter all variables. The issue with this is that it is extremely expensive, up to 50% of the total runtime, and furthermore, it re-examines parts of the clauses that were not touched by the newly set variables. However, it’s not easy to fix this: doing something very smart to a system that is very fast but dumb can slow down the system, since the smart thing can often take more time to compute than doing the dumb thing fast. So I pulled an old trick out of a hat, one that I learned from a paper by Heule et al.: time stamping. Basically, you keep a time stamp for each data element you touched, and as long as you can decide cheaply that you don’t need to recompute something based on the timestamp, you are good. We keep stamping each variable when its value is changed, and then we know what parts of the clauses need to be re-examined, based on the stamp on the clause and the stamp on the variable. I implemented this in a cache-optimized way, similarly how SharpSAT does it, laying it all out flat in the memory, putting clauses next to each other that will be dereferenced after one another — a trick I learned form MiniSat.
  • Prefetching of watchlists, and using blocked literals. Prefetching of watchlists is one of the very few things in SAT solving that was my idea. Basically, whenever a literal is set, its watchlist will be examined shortly. Hence, we can prefetch the watchslit the moment the literal is assigned, so as to prevent the CPU from stalling when the literal’s watchlist is invariably examined. This prefetching can be extended to the component finding, except there it’s occurrence lists and not watchlists. Secondly, I added blocked literals, another cache-optimising trick, by Chu et al (paper). Blocked literals are widely used by modern SAT solvers. SharpSAT missed it because it was written before this trick was known, so I added it in.
  • Recursive Conflict Clause Minimisation by Sörensson and Biere (paper). This was a trivial lift-and-shift from the MiniSat source code. There’s nothing much to say here other than it’s pretty well-known thing, but was not known at the time of SharpSAT. I believe there is nowadays a much better system by Fleury and Biere that does efficient all-UIP minimisation (paper). If you wanna lift-and-shit that code into Ganak and win the model counting competition, be my guest — all Ganak is always open source and online at all points in time, I have no energy to hide code.
  • Tight monitoring and management of memory usage. One of the first things you will notice with some model counters is that they eat all the RAM you have and then get killed by the kernel for lack of memory. This is unfortunately encouraged by the model counting competition guidelines which give massive amounts of memory, up to 64GB, to use by the counters. However, when you are testing your counter, almost all cluster systems have approx 4GB of memory per core (or less) in their nodes. The cluster I use has 160 cores per node and each node has 768GB of RAM, giving 4.8GB/core. Hence, if I want to test my counter without wasting resources, it should use at most 4.8GB of memory. Since I wanted to win the model counting competition, and for that I needed to test my system a lot, I optimised the system to use about 4.5GB memory at most. This is approx 10x less than what many other counters use. The way I did this is by (1) making sure no memory is leaked, ever, (2) precisely accounting for all memory usage and (3) deleting cache items that are occupying too much memory, ruthlessly. This required a using the valgrind memory leak detector, and a lot of use of valgrind’s massif heap profiler for many different types of inputs. This ensured that Ganak uses only the required amount of memory, and can safely and efficiently run in memory-constrained environments. In fact, Ganak would have won all tracks in both previous model counting competitions with only 1/10th of the allowed memory use (i.e. 6.4GB instead of 64GB).
  • A few more things that I can barely remember. For example, watchlists or clauses(?) were reverse-visited. Binary clauses were in the same watchlists as the normal clauses, but they can use a specialised watchlist and be visited faster. Clauses were removed from the watchlist using the “switch-to-the-end” trick which has been shown to be less efficient than simply overwriting. The original Ganak allocated memory for the component, hashed it, then deallocated the memory, but it could have called the hash in-situ, without the allocation, copy, and de-allocation. The original Ganak also used a hash function that was optimised to hash very large inputs, which made it impossible to compile to emscripten due to the CPU intrinsics used, and besides, it was unnecessary because it only had to hash a few KB at most. So I switched to chibihash64 by nrk.

The above took about 3-4 years of work, on-and-off, since I don’t normally get paid to do research. The total time I worked on Ganak being paid to do it was about 4-5 months. So it was mostly just passion and having some fun. The code at least is not absolutely unreadable, and there are a lot of seatbelts around, about 5-10% of the code is asserts, and there are entire sets of functions written solely to do self-checking, debug reporting, etc.

I will likely not publish any of the above ideas/improvements. Some are, I think, publishable, for example the the vivification, but especially that code is nightmare-inducing to me. The fuzzing and debugging while important to me, as I am interested in tools that work, is hard to publish and not too novel. Memory management again falls into this weird place where it’s not very novel but necessary for usable tools. Supporting many fields is just a basic requirement for a well-functioning system, besides, it’s super-easy to do, if set up right. The rest is just basic copy-paste with minor adjustment. I think the use of CCNR is actually quite fun, but I hardly think it’s worth a paper. It’s shaving 30-40% time off of a very slow-running (but necessary) part of the preprocessor, and I was very happy when I discovered it.

I hope you appreciated this somewhat long list. The code can of course be examined for all of them, and you can lift-and-shift some/all the ideas into other tools and other systems. I left quite a lot of comments, and if you turn on VERBOSE_DEBUG and set verbosity very high (say, “–verb 100”) you should be able to see how all of them work in tandem.

Our tools for solving, counting and sampling

Development, Research, SAT, Tools, , ,

This post is just a bit of a recap of what we have developed over the years as part of our toolset of SAT solvers, counters, and samplers. Many of these tools depend on each other, and have taken greatly from other tools, papers, and ideas. These dependencies are too long to list here, but the list is long, probably starting somewhere around the Greek period, and goes all the way to recent work such as SharpSAT-td or B+E. My personal work stretches back to the beginning of CryptoMiniSat in 2009, and the last addition to our list is Pepin.

Overview

Firstly when I say “we” I loosely refer to the work of my colleagues and myself, often but not always part of the research group lead by Prof Kuldeep Meel. Secondly, almost all these tools depend on CryptoMiniSat, a SAT solver that I have been writing since around 2009. This is because most of these tools use DIMACS CNF as the input format and/or make use of a SAT solver, and CryptoMiniSat is excellent at reading, transforming , and solving CNFs. Thirdly, many of these tools have python interface, some connected to PySAT. Finally, all these tools are maintained by me personally, and all have a static Linux executable as part of their release, but many have a MacOS binary, and some even a Windows binary. All of them build with open source toolchains using open source libraries, and all of them are either MIT licensed or GPL licensed. There are no stale issues in their respective GitHub repositories, and most of them are fuzzed.

CryptoMiniSat

CryptoMiniSat (research paper) our SAT solver that can solve and pre- and inprocess CNFs. It is currently approx 30k+ lines of code, with a large amount of codebase dedicated to CNF transformations, which are also called “inprocessing” steps. These transformations are accessible to the outside via an API that many of the other tools take advantage of. CryptoMiniSat used to be a state-of-the-art SAT solver, and while it’s not too shabby even now, it hasn’t had the chance to shine at a SAT competition since 2020, when it came 3rd place. It’s hard to keep SAT solver competitive, there are many aspects to such an endeavor, but mostly it’s energy and time, some of which I have lately redirected into other projects, see below. Nevertheless, it’s a cornerstone of many of our tools, and e.g. large portions of ApproxMC and Arjun are in fact implemented in CryptoMiniSat, so that improvement in one tool can benefit all other tools.

Arjun

Arjun (research paper) is our tool to make CNFs easier to count with ApproxMC, our approximate counter. Arjun takes a CNF with or without a projection set, and computes a small projection set for it. What this means is that if say the question was: “How many solutions does this CNF has if we only count solutions to be distinct over variables v4, v5, and v6?”, Arjun can compute that in fact it’s sufficient to e.g. compute the solutions over variables v4 and v5, and that will be the same as the solutions over v4, v5, and v6. This can make a huge difference for large CNFs where e.g. the original projection set can be 100k variables, but Arjun can compute a projection set sometimes as small as a few hundred. Hence, Arjun is used as a preprocessor for our model counters ApproxMC and GANAK.

ApproxMC

ApproxMC (research paper) is our probabilistically approximate model counter for CNFs. This means that when e.g. ApproxMC gives a result, it gives it in a form of “The model count is between 0.9*M and 1.1*M, with a probability of 99%, and with a probability of 1%, it can be any value”. Which is very often enough for most cases of counting, and is much easier to compute than an exact count. It counts by basically halfing the solution space K times and then counts the remaining number of solutions. Then, the count is estimated to be 2^(how many times we halved)*(how many solutions remained). This halfing is done using XOR constraints, which CryptoMiniSat is very efficient at. In fact, no other state-of-the-art SAT solver can currently perform XOR reasoning other than CryptoMiniSat.

UniGen

UniGen (research paper) is an approximate probabilistic uniform sample generator for CNFs. Basically, it generates samples that are probabilistically approximately uniform. This can be hepful for example if you want to generate test cases for a problem, and you need the samples to be almost uniform. It uses ApproxMC to first count and then the same idea as ApproxMC to sample: add as many XORs as needed to half the solution space, and then take K random elements from the remaining (small) set of solutions. These will be the samples returned. Notice that UniGen depends on ApproxMC for counting, Arjun for projection minimization, and CryptoMiniSat for the heavy-lifting of solution/UNSAT finding.

GANAK

GANAK (research paper, binary) is our probabilistic exact model counter. In other words, it returns a solution such as “This CNF has 847365 solutions, with a probability of 99.99%, and with 0.01% probability, any other value”. GANAK is based on SharpSAT and some parts of SharpSAT-td and GPMC. In its currently released form, it is in its infancy, and while usable, it needs e.g. Arjun to be ran on the CNF before, and while competitive, its ease-of-use could be improved. Vast improvements are in the works, though, and hopefully things will be better for the next Model Counting Competition.

CMSGen

CMSGen (research paper) is our fast, weighted, uniform-like sampler, which means it tries to give uniform samples the best it can, but it provides no guarantees for its correctness. While it provides no guarantees, it is surprisingly good at generating uniform samples. While these samples cannot be trusted in scenarios where the samples must be uniform, they are very effective in scenarios where a less-than-uniform sample will only degrade the performance of a system. For example, they are great at refining machine learning models, where the samples are taken uniformly at random from the area of input where the ML model performs poorly, to further train (i.e. refine) the model on inputs where it is performing poorly. Here, if the sample is not uniform, it will only slow down the learning, but not make it incorrect. However, generating provably uniform samples in such scenarios may be prohibitively expensive. CMSGen is derived from CryptoMiniSat, but does not import it as a library.

Bosphorus

Bosphorus (research paper) is our ANF solver, where ANF stands for Algebraic Normal Form. It’s a format used widely in cryptography to describe constraints over a finite field via multivariate polynomials over a the field of GF(2). Essentially, it’s equations such as “a XOR b XOR (b AND c) XOR true = false” where a,b,c are booleans. These allow some problems to be expressed in a very compact way and solving them can often be tantamount to breaking a cryptographic primitive such as a symmetric cipher. Bosphorus takes such a set of polynomials as input and either tries to simplify them via a set of inprocessing steps and SAT solving, and/or tries to solve them via translation to a SAT problem. It can output an equivalent CNF, too, that can e.g. be counted via GANAK, which will give the count of solutions to the original ANF. In this sense, Bosphorus is a bridge from ANF into our set of CNF tools above, allowing cryptographers to make use of the wide array of tools we have developed for solving, counting, and sampling CNFs.

Pepin

Pepin (research paper) is our probabilistically approximate DNF counter. DNF is basically the reverse of CNF — it’s trivial to ascertain if there is a solution, but it’s very hard to know if all solutions are present. However, it is actually extremely fast to probabilistically approximate how many solutions a DNF has. Pepin does exactly that. It’s one of the very few tools we have that doesn’t depend on CryptoMiniSat, as it deals with DNFs, and not CNFs. It basically blows all other such approximate counters out of the water, and of course its speed is basically incomparable to that of exact counters. If you need to count a DNF formula, and you don’t need an exact result, Pepin is a great tool of choice.

Conclusions

My personal philosophy has been that if a tool is not easily accessible (e.g. having to email the authors) and has no support, it essentially doesn’t exist. Hence, I try my best to keep the tools I feel responsible for accessible and well-supported. In fact, this runs so deep, that e.g. CryptoMiniSat uses the symmetry breaking tool BreakID, and so I made that tool into a robust library, which is now being packaged by Fedora, because it’s needed by CryptoMiniSat. In other words, I am pulling other people’s tools into the “maintained and supported” list of projects that I work with, because I want to make use of them (e.g. BreakID now builds on Linux, MacOS, and Windows). I did the same with e.g. the Louvain Community library, which had a few oddities/issues I wanted to fix.

Another oddity of mine is that I try my best to make our tools make sense to the user, work as intended, give meaningful (error) messages, and good help pages. For example, none of the tools I develop call subprocesses that make it hard to stop a computation, and none use a random number seed that can lead to reproducibility issues. While I am aware that working tools are sometimes less respected than a highly cited research paper, and so in some sense I am investing my time in a slightly suboptimal way, I still feel obliged to make sure the tax money spent on my academic salary gives something tangible back to the people who pay for it.

On benchmark randomization

Research, SAT, , ,

As many of you have heard, the SAT Competition for this year has been announced. You can send in your benchmarks between the 12th and the 22nd of April, so get started. I have a bunch of benchmarks I have already submitted about 2 years ago, still waiting for any reply from those organizers — but the organizers are different this year, so fingers crossed.

What I want to talk about today is benchmark randomization. This is a very-very touchy topic. However, I fear that it’s touchy for the wrong reasons, and so I think it’s important to talk about it in detail.

What is benchmark randomization?

Benchmark randomization is when a benchmark that is submitted is shuffled around a bit. There are many ways to shuffle a problem, and I will discuss this in a bit, but the point is that the problem at hand that is described by the benchmark CNF should not be changed, or changed only in a very-very minor way, such that everyone agrees that it doesn’t affect the core problem itself as described by the CNF.

Why do we need shuffling?

We need shuffling because simply put, there aren’t enough good benchmarks and so the benchmarks of yesteryear (and the year before, and before, and…) re-appear often. This would be OK if SAT solvers couldn’t be tuned to solving specific problems faster. Note that I am not suggesting that SAT solvers are intentionally manipulated to solve specific problems faster by unscrupulous researchers. Instead, the following happens.

Unintentional random seed improvements

Researchers test the performance of their SAT solvers on specific instances and then tune their solvers, testing the performance again and again on the same instances to check if they have improved performance. Logically this is the best way to test and improve performance: use the same well-defined test-set all the time for meaningful comparison. Since the researcher wants to use the instances that he/she thinks is the current use-case of SAT solvers, he naturally uses the instances of SAT competitions, since those are representative. I did and still do the same.

So, researchers add their idea to a SAT solver, and test. If the idea is not improving things then some change is made and tested again. Since modern CDCL SAT solvers behave quite randomly, and since any change in the source code changes the behaviour quite significantly, a small change in the source code (tuning of a parameter, for example) will change the behaviour. And since the set of problems tested on is fixed, there is a chance that more problems will be solved. If more are solved, the researcher might correctly interpret this as a general improvement, not specific to the problem set. However, it may very well be generic, it is also specific.

The above suggests that the randomness of the SAT solver is completely unintentionally tuned to specific problems — a subset of which will appear next year in the competition.

Easy fixes

Since there aren’t enough benchmark problems, and in particular some benchmark types are rare, I suggest to fix the unintentional tuning of solvers to specific problems by changing the benchmarks in minor ways. Here is a list, with an explanation why I think it’s OK to perform the manipulation:

  1. Propagate variables. Unitary clauses are often part of benchmarks. Propagating some of these, some recursively, gives quite a bit of problem space variation. Propagation is performed by every CDCL SAT solver, and I think many would be  surprised if it didn’t help SAT solvers that worked differently than  current SAT solvers. Agreeing on performing partial propagation is something that shouldn’t be too difficult.
  2. Renumber variables. For some variable X that is not used (or is fixed to a value that has been propagated), every variable that is higher than X is decremented by one, and the CNF header is fixed to reflect this change.  Such a minor renumbering may be approved by every researcher as something that doesn’t change the problem or its structure. Note that if  partial propagation is performed there should be quite a number of variables that can be removed. Renumbering some, but not others is a way to shuffle the problem. A more radical way of renumbering variables would be to completely shuffle them, however that would change the way the problem is described in quite a radical way, so some would correctly object and it’s not necessary anyway.
  3. Replace equivalent literals. Perform strongly connected component analysis and replace equivalent literals. This has been shown to significantly improve performance and I have never seen a case where it doesn’t. Since equivalent literal replacement can be performed with a lot of freedom, this is quite a bit of shuffling space. For example, if v1=v2=v3, then any of the v1, v2, v3 can be the one that replaces the rest in the CNF. Picking one randomly is a way to shuffle the instance

There are other ways of shuffling, but either they change the instance too much (e.g. blocked clause removal), or can be undone quite easily (e.g. shuffling the order of the clauses). In fact, (3) is already quite a touchy issue I think, but with (1) and (2) all could agree on. Neither requires the order of the literals or the order of the clauses to change — some clauses (e.g. unitary ones) and literals (some of those that are set) would be removed, but that’s all. The problem remains essentially unchanged such that most probably even the original problem author would easily recognize it. However, it would be different from a SAT solver point of view: these changes would change the random seed of the solver, forcing the solver to behave in a way that is less tuned to this specific problem instance.

Conclusion

SAT solvers are currently tuned too much to specific instances. This is not intentional by the researchers, however it still affects the results. To obtain better, less biased results we should shuffle the problem instances we have. Above, I suggested three ways to shuffle the instances in such a way that most would agree they don’t disturb or change the complexity of the underlying problem described by the instance. I hope that some of these suggestions will be employed, if not this year then for next year’s SAT competition such that we could reach better, more meaningful results.

anf2cnf script released

SAT, , ,

I have finally managed to fix the script that converts ANF problems to CNF format in the Sage math system. The original script was having some problems that I blogged about. The new script has corrected most of the shortcomings of the original script, as well as added some textual help for the user.

For instance, the equations

sage: print two_polynoms
[x0*x1 + 1, x0*x1 + x1]

that last time required 13 clauses and 4 variables in CNF, now look like this:

sage: print anf2cnf.cnf(two_polynoms)
p cnf 3 6
c ------------------------------
c Next definition: x0*x1 + 1
3 0
c ------------------------------
c Next definition: x0*x1 + x1
3 -2 0
-3 2 0
c ------------------------------
c Next definition: monomial x0*x1
1 -3 0
2 -3 0
3 -1 -2 0

which is 1 variable and 7 clauses shorter than the original, not to mention the visually cleaner look and human-parseable output. The new script is available here. Hopefully, some of my enhancements included in the Grain-of-Salt package will be included in this script. The problem is mainly that Grain-of-Salt uses radically different data structures, and is written in a different programming language, so porting is not trivial.

anf2cnf hell in Sage

SAT, ,

There is an ANF (Algebraic Normal Form) to CNF (Conjunctive Normal Form) converter by Martin Albrecht in Sage. Essentially, it performs the ANF to CNF conversion that I have described previously in this blog entry. Me, as unsuspecting as anyone else, have been using this for a couple of days now. It seemed to do its job. However, today, I wanted to backport some of my ideas to this converter. And then it hit me.

Let me illustrate with a short example why I think something is wrong with this converter. We will try to encode that variable 0 and variable 1 cannot both be TRUE. This is as simple as saying x0*x1 = 0 in plain old math. In Sage this is done like this:

sage: B = BooleanPolynomialRing(10,'x')
sage: load anf2cnf.py
sage: anf2cnf = ANFSatSolver(B)
sage: polynom = B.gen(0)*B.gen(1)
sage: print polynom
x0*x1

So far, so good. Let’s try to make a CNF out of this:

sage: print anf2cnf.cnf([polynom])
p cnf 4 6
2 -4 0
3 -4 0
4 -2 -3 0
1 0
4 1 0
-4 -1 0

Oooops. Why do we need 6 clauses to describe this? It can be described with exactly one:

p cnf 2 1
-1 -2

This lonely clause simply bans the solution 1 = TRUE, 2 = TRUE, which was our original aim.

Let me just mention one more thing about this converter: it repeats definitions. For example:

sage: print two_polynoms
[x1*x2 + 1, x1*x2 + x1]
sage:  print anf2cnf.cnf(two_polynoms)
p cnf 4 13
2 -4 0
3 -4 0
4 -2 -3 0
1 0
4 0
2 -4 0
3 -4 0
4 -2 -3 0
1 0
4 2 1 0
-4 -2 1 0
-4 2 -1 0
4 -2 -1 0

Notice that clause 2 -4 0 and the two following it have been repeated twice, as well as the clause setting 1 to TRUE.

I have been trying to get around these problems lately. When ready, the new script will be made available, along with some HOWTO. It will have some minor shortcomings, but already, the number of clauses in problem descriptions have dramatically dropped. For example, originally, the description of an example problem in CNF contained 221’612 clauses. After minor corrections, the same can now be described with only 122’042 clauses. This of course means faster solving, cleaner and even human-readable CNF output, etc. Fingers are crossed for an early release ;)