Solving Tabular relations

Question

In scenario : Input table with columns "Name", "Value"

Each column is represented as Enum sorts for z3 (Valid possible values of a column is known)
A combination (Name, Value) is represented as a DataType
Valid combination : if it appears in table

The following sample code always returns unsat. I can model same using uninterpreted sort and functions, however would like to know why the following with DataType isnt working.

import z3 as z3

symbol_dict = {}

def create_enum_sort(name, elts):
    global symbol_dict
    z3_sort, z3_elts = z3.EnumSort(name, elts)
    for e in z3_elts:
        symbol_dict[str(e)] = e
    return z3_sort


# Universe of Enum values for columns to take
Values = ['1', '2', '3', '4', '5']
Names = ['A1', 'A2', 'B1', 'B2', 'C5']

VTYPE = create_enum_sort('VTYPE', Values)
NTYPE = create_enum_sort('NTYPE', Names)

# Valid combinations (Table relation)
dct = {'A2': '2',
       'A1': '1',
       'B1': '1',
       'B2': '2',
       'C5': '5'}

# Record type consisting of Name, Value
comb = z3.Datatype('Comb')
comb.declare('cons', \
           ('value', VTYPE), \
           ('name', NTYPE) \
           )
COMB = comb.create()

# Constraint to valid combinations
constraints = []
e1 = z3.Const('e1', COMB)
for key, value in dct.items():
    constraints.append(z3.ForAll([e1], 
            z3.Implies(COMB.name(e1) == symbol_dict[key], COMB.value(e1) == symbol_dict[value])))
    

# Basic check 
solver = z3.Solver()
solver.add(constraints)

xvar = z3.Const('xvar', COMB)

solver.set(unsat_core=True)
print(solver.assertions())    
res = solver.check()
print(res)
if res == z3.sat:
    model = solver.model()
    print('Model:', model)

alias alias · Accepted Answer · 2021-12-30T18:19:54

Your query is unsat because data-types in SMTLib are freely generated. If you look at the output of your program, you'll see:

ForAll(e1, Implies(name(e1) == A2, value(e1) == 2))

amongst other constraints. This constraint by itself isn't satisfiable. Why? Because it says for all Comb values, if the name field is A2, then it's value field must be 2. Clearly that's not true: A freely generated data-type contains all those values; i.e., it also contains the value name = A2 and value = 1. This is why you're getting unsat. (Note what your assertion is saying: FOR ALL values of Comb, it needs to satisfy the constraint. This is clearly not true.)

Of course, what you wanted to say was not that all Comb values satisfy this constraint! You meant there's a particular Comb that has these properties. The way to write that is as follows. I'm only including the part that modifies the constraints variable; everything prior can stay the same:

constraints = []
e1 = z3.Const('e1', COMB)
for key, value in dct.items():
    constraints.append(z3.Implies(COMB.name(e1) == symbol_dict[key], COMB.value(e1) == symbol_dict[value]))

solver = z3.Solver()
solver.add(z3.Or(constraints))

solver.set(unsat_core=True)
res = solver.check()
print(res)
if res == z3.sat:
    model = solver.model()
    print('Model:', model.evaluate(e1, model_completion=True))

This prints:

sat
Model: cons(1, A1)

giving you one possible interpretation for the value of e1.

Note that I had to use the evaluate method of the model to get this printed. Simply printing the model returns an empty list; which can be surprising. I'm not entirely sure why z3 doesn't assign a value for it in the standard-mode. Model-construction has its own quirks. I suspect if you have other constraints on e1 you wouldn't need to do so. If this turns out to be a hurdle, feel free to post a new question demonstrating the issue.

Solving Tabular relations

1 Answers