Requiring the AND of two bit vectors two have at most k true values

[jplauri]

Suppose we have two bit vectors (always of the same length). We'd like to express that the bitwise AND of the two contains at most k true values. Is there a neat way of doing this via PySAT?

So for instance, suppose we had two vectors consisting of the variables [1,2,3] and [4,5,6]. If k was equal to 1, we'd be fine if the variables took Boolean values such that they were [0,1,1] and [0,0,1] since now the third position is the only position where both vectors have a 1. On the other hand, if the vectors were [0,1,1] and [1,1,1] this would not be OK, since the 2nd and 3rd position have a true value after the AND.

I suppose that in theory, one solution is to have three new variables to correspond to the ANDs of the individual bits and then requiring these three bits to have at most k values true. But then again I'm not so sure how to really express this.

[alexeyignatiev]

PySAT gives you a way to model your problems on the CNF level, which is quite low. It would be great to have a submodule with the most popular modeling use cases, like bit vectors. But that requires a significant time investment...

You can still create your own model to work with bit vectors. Here is a simplistic example assumed to be in file bvect.py:

from pysat.formula import CNF, IDPool

class BitVect():
    def __init__(self, variables, pool):
        self.vars = variables[:]
        self.pool = pool
        self.cnf = CNF()

        if self.vars:
            topv = max(abs(l) for l in self.vars)
            if topv > self.pool.top:
                self.pool.occupy(self.pool.top, topv)

    def __getitem__(self, key):
        return self.vars[key]

    def __setitem__(self, key, value):
        self.vars[key] = value

    def __delitem(self, key):
        del self.vars[key]

    def __and__(self, other):
        res = BitVect([], self.pool)
        for x, y in zip(self.vars, other.vars):
            t = res.pool.id('AND({0}, {1})'.format(x, y))
            res.vars.append(t)
            res.cnf.append([-t, x])
            res.cnf.append([-t, y])
            res.cnf.append([t, -x, -y])
        return res

    def __or__(self, other):
        res = BitVect([], self.pool)
        for x, y in zip(self.vars, other.vars):
            t = res.pool.id('OR({0}, {1})'.format(x, y))
            res.vars.append(t)
            res.cnf.append([-t, x, y])
            res.cnf.append([t, -x])
            res.cnf.append([t, -y])
        return res

It is not ideal and looks quite bulky even though it is very simple in terms of capabilities. But it gives you an idea of how you can do that yourself. Now, you can play with it:

>>> from pysat.card import *
>>> from pysat.formula import CNF, IDPool
>>> from pysat.solvers import Solver
>>> from bvect import BitVect
>>>
>>> pool = IDPool()
>>> v1 = BitVect([1, 2, 3], pool)
>>> v2 = BitVect([4, 5, 6], pool)
>>>
>>> v1.vars
[1, 2, 3]
>>> v2.vars
[4, 5, 6]
>>>
>>> v3 = v1 & v2
>>> v3.vars
[7, 8, 9]
>>> v3.cnf.clauses
[[-7, 1], [-7, 4], [7, -1, -4], [-8, 2], [-8, 5], [8, -2, -5], [-9, 3], [-9, 6], [9, -3, -6]]
>>>
>>> am1 = CardEnc.atmost(v3.vars, bound=1, vpool=pool, encoding=EncType.pairwise)
>>> am1.clauses
[[-7, -8], [-7, -9], [-8, -9]]
>>>
>>> formula = CNF()
>>> formula.extend(v1.cnf)
>>> formula.extend(v2.cnf)
>>> formula.extend(v3.cnf)
>>> formula.extend(am1)
>>>
>>> with Solver(name='m22', bootstrap_with=formula) as s:
...     print(s.solve(assumptions=[-1, 2, 3, -4, -5, 6]))
...     print(s.solve(assumptions=[-1, 2, 3, 4, 5, 6]))
...
True
False

[jplauri]

Great, thank you very much! I will give this a try.

Incidentally, I also noticed pySMT for SMT - I've known about SMT but never really played around much with any solvers. Perhaps if one's problem is so heavily involving bit vectors, SMT might also be worth a try. Probably depends on the instance specifics though which one is faster, i.e., experimentation is required as usual :-)

[alexeyignatiev]

Well, if you really have to deal with bitvector arithmetic a lot, you should consider using SMT, e.g. PySMT, indeed. Some SMT solvers do bitblasting, i.e. automatically translate the high-level operations on bitvectors into propositional logic, and then call a SAT solver.

[alexeyignatiev]

Since this is not really an issue of PySAT, I am closing it now.