Lab05 - SAT solving in Python with Z3

We will be using Z3 programmatically in Python. Consider the following classical logic tautologies:

The Z3 code below (via its convenient Python interface) checks that the formulas above are tautologies by trying to find a satisfying assignment to their negation.

from z3 import *

# create a fresh propositional variable uniquely identified by its name 'p'

p = Bool('p')

# excluded middle

solve(Not(Or(p, Not(p))))

# Pierce's law

q = Bool('q')

solve(Not(Implies(Implies(Implies(p, q), p), p)))

#Other useful connectives:

#Implies, And

Exercise (tautologies)

Prove that the following propositional formula is a classical tautology by checking that its negation is unsatisfiable: inline_formula not implemented.

What about the following Łukasiewicz's formula? inline_formula not implemented.

r = Bool('r')

s = Bool('s')

Example (long conjunctions and disjunctions)

We can conveniently use arrays to represent long conjunctions And and disjunctions Or. For instance the next cell implements the following formula: inline_formula not implemented.

n = 10

x = [Bool('x' + str(k)) for k in range(n)]

phi = And([x[k] for k in range(n)])

print(phi)

solve(phi) # satisfiable

Exercise (The SCS problem)

Let inline_formula not implemented be a finite alphabet. The shortest common superstring problem (SCS) has as input a set of finite strings inline_formula not implemented with inline_formula not implemented and a bound inline_formula not implemented, and asks to determine whether there is a string inline_formula not implemented of length inline_formula not implemented s.t. inline_formula not implemented is a (contiguous) superstring of inline_formula not implemented. The SCS problem is NP-complete.

1. Encode the SCS problem as a SAT problem and use Z3 to solve it.

2. Can you reconstruct a solution inline_formula not implemented from the Z3 model?

# input example

S = ["001010011101", "1001010101011", "101101010101010",

     "10111011001010101010", "10110101011010101010", "10110101101010101010"]

m = len(S)

n = 74 # tight?

# how to declare a list of n variables x0, ..., x(n-1)

x = [ Bool('x' + str(k)) for k in range(n) ]

# Solution for S: 001010011101101011010101010100101010101110110010101010101101010110101010100

# this procedure returns an assignment (as a dictionary) if any exists

def model(phi):

    # create a SAT instance

    s = Solver()

    s.add(phi)

    # return a satisfying assignment

    return s.model() if s.check() == sat else []

phi = And([x[k] for k in range(n)])

solution = model(phi)

print([(var, solution[var]) for var in x])

Exercise (All satisfying assignments)

The Z3 solver returns some satisfying assignment, just in case it exists. How can we use Z3 in order to construct all satisfying assignments? To make this meaningful, if the number of satisfying assignments is inline_formula not implemented, then we want to call Z3 inline_formula not implemented times. Write a Python program that returns all satisfying assignments of a given SAT instance.

p = Bool("p")

q = Bool("q")

r = Bool("r")

phi = Or(And(p, Not(q)), r)

m = model(phi)

print(m[p])

print(m[q])

print(m[r])

# Pro tip 1: can enumerate all variables by looking at the keys of m

# Pro tip 2: if x is a key of m,

# the corresponding Z3 variable can be reconstructed with "Bool(str(x))"

# (it should be just "x", but so is life)

vars = [Bool(str(x)) for x in m]

Exercise (Phase transition)

In this exercise we explore the phenomenon of phase transition for the inline_formula not implemented-SAT problem, where inline_formula not implemented is the size of each clause. Let inline_formula not implemented be the number of variables inline_formula not implemented and let inline_formula not implemented be the number of clauses. A random inline_formula not implemented-SAT instance is obtained by producing each of the inline_formula not implemented clauses according to the following process:

• Extract inline_formula not implemented variables without replacement from inline_formula not implemented and determine independently and uniformly whether each variable appears positively or negatively.

Fix inline_formula not implemented, inline_formula not implemented, and let inline_formula not implemented be the probability that a SAT instance randomly generated as above is satisfiable.

1. For a fixed inline_formula not implemented, compute an estimate inline_formula not implemented by sampling inline_formula not implemented instances as above.

2. Plot the estimates inline_formula not implemented as a function of inline_formula not implemented.

3. What is an "interesting" interval for inline_formula not implemented? Refine the interval above if necessary.

%matplotlib inline

import matplotlib.pyplot as plt

import numpy as np

import random

# number of variables

n = 10

# size of a clause

k = 3

# number of samples per point

N = 100

variables = [Bool('x' + str(i)) for i in range(n)]

# Hints:

# np.random.choice(list) returns a random element from list

# np.random.choice(list, k, replace=False) returns k random elements from list *without replacement*

# np.mean(list) computes the average of the numbers in the list

# plt.plot(list) generates a plot from a list of values

# plt.show() displays the plot

# a simple plot example

list = [x * x for x in range(20)]

plt.plot(list)

plt.show()