Bit blasting gives answers that do not live up to the constraints

Question

I am using z3 to do bit blasting. I then solve the problem in a SAT solver, and do reverse bit blasting in order to find out what value the varibles take. However, I find that the solutions I get after doing reverse bit balsting do not live up to the constraints. As z3 does not save which values corrospond to what in the bit blasted reslult, I have used a piece of code from How can I access the variable mapping used when bit-blasting? to do that. I suspect that the problem might be here, as I get more varibles and constraints when using a bitmap than when I don't do it.

I have the following code:

x1 = BitVec('x1', 2)
x2 = BitVec('x2', 2)

g = Goal()

bitmap = {}
for i in range(2):
    bitmap[(x1,i)] = Bool('x1'+str(i))
    mask = BitVecSort(2).cast(math.pow(2,i))
    g.add(bitmap[(x1,i)] == ((x1 & mask) == mask))
    bitmap[(x2,i)] = Bool('x2'+str(i))
    mask = BitVecSort(2).cast(math.pow(2,i))
    g.add(bitmap[(x2,i)] == ((x2 & mask) == mask))

g.add(x1 + x2 == 3)

t = Then('simplify', 'bit-blast', 'tseitin-cnf')
subgoal = t(g)

For which I get the following solutions (x1 = 2, x2 =2), (x1 = 0, x2 = 0), (x1 = 1, x2 = 1) and (x1 = 3, x2 = 3). For different constraints I get different solutions(x1 and x2 and not always the same), but they don't live up to the constraints.

score 0 · Answer 1 · answered Feb 20 '23 at 16:05

There's nothing wrong with this encoding, and while it's hard to decipher the tseitin output from z3, I'd assume it's correct as well.

What you haven't shown us is the output of this "other" SAT solver, and more importantly, how you translate that back to z3. I suspect the bug is in there somewhere. But without seeing that code, it's impossible to answer your question. But as a guide, I'd look at the code that translates back the SAT output to your z3py variables. What code are you using for that purpose?

score 0 · Answer 2 · answered Feb 21 '23 at 07:38

I am using a SAT solver called "SPUR" that takes DIMACS format. It then outputs a row for each solution, that consists of 0 and 1's so the first number represent varible 1 and so on. I translate it to DIMACS like this:

var_count = 1
constraint_count=0
varibles_number = {}
varibles_var = {}
negation = False
dimacs_format = [[]]
for c in subgoal[0]:
    constraint_count += 1
    dimacs_format.append([])
    for i in range(c.num_args()):
        #Save varible names in dictonary
        if(is_app_of(c.arg(i),Z3_OP_NOT)):
            var = simplify(Not(c.arg(i)))
            negation = True
        else:
            var = c.arg(i)
        if(var not in varibles_var):
            varibles_var[var] = var_count
            varibles_number[var_count] = var
            var_count += 1
        if(negation == True):
            dimacs_format[constraint_count].append(-varibles_var[var])
        else:
            dimacs_format[constraint_count].append(varibles_var[var])
        negation = False
    if(c.num_args() == 0):
        var = c
        if(var not in varibles_var):
            varibles_var[var] = var_count
            varibles_number[var_count] = var
            var_count += 1
        dimacs_format[constraint_count].append(varibles_var[var])
    
    dimacs_format[constraint_count].append(0)


n_varibles = len(varibles_var)
n_constraints = len(dimacs_format)-1
s = "p cnf " + str(n_varibles) + " " + str(n_constraints)
dimacs_format[0].append(s)

I then solve it in SPUR

#Number of solutions
n = 4
#Number of variables
m = n_varibles

samples = np.zeros((n,m))

file = "../samples_file.txt"
counter = 0
with open(file , 'r') as f:
    i = 0
    for line in f:
        if ((line[0]).isdigit()):
            n_ = int(line.split(',')[0])
            sampel2 = line.split(',')[1]
            sampel = sampel2.split('\n')[0]
            samples[i]=list(map(int, sampel))
            i += 1

varible_values = {}
for i in range(m):
    varible_values[str(varibles_number[i+1])] = samples[:,i]

x1 = varible_values['x10']+2*varible_values['x11'] 
x2 = varible_values['x20']+2*varible_values['x21']

You'll have to debug this code; look at the produced CNF; convince yourself that it captures the z3's output faithfully, and then check the translation. Unfortunately, there isn't much here we can help you with, aside from debugging your whole code. Stack-overflow works the best when you have very specific questions, instead of large-swaths of code to debug. See if you can spot the issue and can ask a specific question if you're unable to debug. Best of luck! — alias, Feb 21 '23 at 09:09

Bit blasting gives answers that do not live up to the constraints

2 Answers2