A more compact encoding of the full adder

[martin-cs]

In http://www.kroening.com/papers/vmcai2016.pdf we give a more compact encoding of the full adder (Fig 3.c, page 6):

{cin,¬s,¬cout}
{a,¬s,¬cout}
{b,¬s,¬cout}
{a,b,cin,¬s}
{¬a,¬b,¬cin,s}
{¬cin,s,cout}
{¬a,s,cout} 
{¬b,s,cout}
{¬a,¬b,cout}
{¬a,¬cin,cout}
{¬b,¬cin,cout}
{a,b,¬cout}
{a,cin,¬cout}
{b,cin,¬cout}

we found it improved performance. It would be great to know if it helps your usecases.

[petersn]

Got it, thanks so much for the reference!

I believe this is the full adder that is currently automatically synthesized by the current heuristics I'm using. For example, if one writes:

import autosat

@autosat.sat
def full_adder(a, b, cin):
    r = a + b + cin
    s = r & 1
    cout = r >> 1
    return s, cout

inst = autosat.Instance()
a, b, cin, s, cout = inst.new_vars(5)
full_adder(a, b, cin, outs=[s, cout])
for clause in inst.clauses:
    print("{" + ",".join(
        ("¬" if lit < 0 else "") + ["a", "b", "cin", "s", "cout"][abs(lit) - 1]
        for lit in clause
    ) + "}")

then one will get:

{a,b,¬cout}
{¬a,¬b,cout}
{cin,¬s,¬cout}
{¬cin,s,cout}
{a,cin,¬cout}
{¬a,¬cin,cout}
{b,cin,¬cout}
{¬b,¬cin,cout}
{a,¬s,¬cout}
{¬a,s,cout}
{b,¬s,¬cout}
{¬b,s,cout}
{a,b,cin,¬s}
{¬a,¬b,¬cin,s}

I compared this to your thing by hand by sorting them, and they appear to be identical. So it looks like I'm already producing your adders.

Your paper looks very useful, I'd like to take a closer look. From skimming algorithms 1 and 2 from your paper I'd assume what I'm doing is too naive and is inferior in more complicated cases (what I'm doing is definitely simpler than what you show), even if it's equivalent for the full adder example. Do you have any other relations you'd recommend I try as test cases? Presumably I should just be implementing your algorithms instead, once I understand them.

Thanks again for the reference, this is exactly the sort of content I'm looking for for fleshing out this library.

[martin-cs]

It's great that you are already using it!

The algorithms we have are intended to be design-time rather than part of bit-blasting (although you could). I would use them to improve small sbox encodings or places where the circuit contains diamonds. The complexity is pretty high so they are only really suitable for small components.

Our implementation is available here:

https://github.com/sat-group/genpce

which might save you a little time.

Note that propagation completeness is not the whole story on encoding performance. Auxiliary variables that allow better generalisation are also a factor but we didn't ever get a formalisation we were happy with for exploring this.

[petersn]

Okay, super cool, thanks for the link.

What's the approximate complexity of what you're doing? My current algorithm is:

We would like to implement a relation on n bits. Let a "state" refer to a configuration of said n bits. We will think of our relation as being a set of allowed states. Call a clause "admissible" if it rules out no allowed states. Call a clause "useful" if it rules out at least one disallowed state, and call it increasingly useful if it rules out more disallowed states.

My heuristic: Start with the empty implementation. Then repeatedly greedily add the next most useful admissible clause (as in, ruling out the greatest number of invalid states without ruling out any valid states), until we run out of clauses to add of a given length; we then advance to the next possible clause length. Eventually all invalid states are ruled out, and we're done.

As pseudocode:

implementation = []
states_to_rule_out = [ all states disallowed by the relation ]
for each clause size 0, 1, 2, ...:
    while true:
        candidates_list = a list of admissible clauses of the current size
                          that are useful for states_to_rule_out
        if candidates_list is empty:
            break
        selected_clause = the clause in candidates_list that rules out
                          the maximum number of states in states_to_rule_out
        implementation.append(selected_clause)
        filter states_to_rule_out down excluding any states ruled out by selected_clause
    if states_to_rule_out is empty:
        return implementation

This algorithm seems to run very quickly for "typical" relations on at most 16ish bits, and starts to really take quite a while on typical relations around 18 or so bits, at which point it can take tens of minutes (therefore this library applies a bunch of caching).

If you don't mind me asking, approximately what sorts of running times were you seeing with genpce for what sorts of sizes?

[martin-cs]

Aside from the results table in the paper I don't have any particularly accurate numbers. I recall the 44->8 multiplication taking a while and the 55->10 multiplication being computationally prohibitive.

I think your algorithm is broadly speaking in the same vein. IIRC the run-time is exponential.

[petersn]

Okay, cool. Do you happen to have the results of the 4 bit x 4 bit -> 8 bit multiplication handy? I'm super curious how far off from a careful implementation my greedy heuristic gets.

For reference:

@autosat.sat
def mult(x0, x1, x2, x3, y0, y1, y2, y3):
    x = 1*x0 + 2*x1 + 4*x2 + 8*x3
    y = 1*y0 + 2*y1 + 4*y2 + 8*y3
    r = x * y 
    return [(r >> i) & 1 for i in range(8)]

takes 3.3 seconds to implement on my machine, and produces an implementation with:
Clauses of length 2: 4
Clauses of length 3: 13
Clauses of length 4: 73
Clauses of length 5: 108
Clauses of length 6: 38

If it's a hassle to pull up what you were generating, no worries, I can just play with genpce myself, this is already extremely helpful.

[martin-cs]

I /think/ it is this:

https://github.com/sat-group/genpce/blob/master/circuits/genpce/cvc-mult4_4.cnf

but it is possible that I have misremembered. That directory contains the generated encodings.

[martin-cs]

Ah, actually, that might be 4*4->4 (i.e. modulo multiply).

[petersn]

Ack, sorry for the four year delay in responding. For 4*4->4 multiplication I see:

Clauses of length 2: 2
Clauses of length 3: 5
Clauses of length 4: 16
Clauses of length 5: 29
Clauses of length 6: 27
Clauses of length 7: 13
Clauses of length 8: 3

That's a total of 95 clauses, but the thing you linked has 670 clauses. I'm curious what the differences are!

[martin-cs]

Off the top of my head, I don't know. It has been some while since I last worked on this. If I were guessing I would say it was something to do with the use of intermediate variables. The original (reference) encoding we used had 97 clauses but 36 variables (i.e. 8 input, 4 output and 24 intermediate). As the optimal encoding is computed just using input and output variables it will miss out some of the compression that is possible using intermediate variables. I notice that there are some clear patterns and repeated subclauses in the optimal encoding so it is likely possible to compact it using new variables (computing these was always on our TODO list but never got TODONE!).

If this kind of thing is still of interest / entertainment / use to you, we have a paper at SMT'25 this year on compact encodings for polynomials over bit-vectors.