# Propagating binary clauses

Binary clauses are somewhat special. They are clauses that look like:

`-v1 or v20 = true`
`-v1 or v21 = true`

which basically mean: if `v1` is TRUE, then both `v20` and `v21` must be TRUE. We put these clauses into a special datastructure, that looks like this:

`watchlist[-v1] = v20,v21, ...`

This makes us all very happy, since this datastructure is very simple: just literals (negated or non-negated variables) one after the other, in a very trivial list. This makes the whole thing very compact, and very efficient.

The problem with such a list is that when `v1` is indeed set to TRUE, then when we set the variables (e.g. `v20,v21`), we must record what set these variables to their new values. What usually is done is to simply record the pointer to the clause that does this. However, in the above datastructure, there are no clause pointers. The datastructure for GLUCOSE contained these pointers. I have lately been experimenting with removing these pointers. The tricky part is to update the conflict generation routine that examines the clauses and decisions that lead to a conflict. This routine must now automatically recognise that these binary clauses are special, and they are only 2-long: one part of them is the variable that got set, and the other part is the variable that set it. These two informations are available: `watchlist[-v1] ` immediately tells us that literal `-v1` set the variable, and the variable that got set is always known.

Armed with this logic, one would think that moving towards this all-new no-clause-pointers heaven is the way to go. However, apparently, this might not be so. This is quite astonishing, given that doing things without pointers should mean less cache-misses (since pointers are less likely to be resolved during conflict analysis). I consistently get worse speeds, though. I am guessing that the problem lies with the datastructure I use to store the information stating what lead to the setting of the variable. I use a very simple struct:

```struct WhatLeadHere {
bool wasPointer;
union{Clause* pointer; Lit lit;};
};```

where `wasPointer` is TRUE if a non-binary clause lead here (and we store the pointer), and FALSE if it was a binary clause (and we store the other literal). The union takes care of the rest: `pointer` is valid when `wasPointer` is TRUE and `lit` is valid when `wasPointer` is FALSE.

What is apparent in this datastructure is the following: we now store a 32/64 bit pointer plus we store a boolean. Right, so 42/72 bits of data? No. Data alignment in C++ means, that this datastructure will be aligned according to its largest member, so it will be aligned to 32/64-bit boundaries: this datastructure takes 128/64 bits to store on 32 and 64 bit architectures, respectively. Oops, we just doubled our demand of data writes!

There are some remedies, of course. We can simply pack:

```#pragma pack(push)
#pragma pack(1)