Instructor: Ashutosh Gupta

(1)

cbna CS228 Logic for Computer Science 2021 Instructor: Ashutosh Gupta IITB, India 1

CS228 Logic for Computer Science 2021

Lecture 13: Encoding into reasoning problems

Instructor: Ashutosh Gupta

IITB, India

Compile date: 2021-02-04

(2)

Topic 13.1

Z3 solver

(3)

Solver basic interface

I Input : formula I Output: sat/unsat

If satisfiable, we may ask for a satisfying assignment.

Exercise 13.1

What can we ask from a solver in case of unsatisfiability?

(4)

Z3: SMT solver

I Written in C++

I Provides API in C++ and Python

I We will initially use python interface for quick ramp up

I Later classes we will switch to C++ interface

(5)

Installing Z3 (Ubuntu-18.04)

$ sudo apt-get install z3

Not tested on 20.04

(6)

Locally Installing a version of Z3 (Linux)

Let us install z3-4.7.1 . You may choose another version.

I Download

https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1-x64-ubuntu-16.04.zip

I Unzip the file in some folder. Say

/path/z3-4.7.1-x64-ubuntu-16.04/

I Update the following environment variables

$ export LD_LIBRARY_PATH= $ LD_LIBRARY_PATH:/path/z3-4.7.1-x64-ubuntu-16.04/bin

$ export PYTHONPATH= $ PYTHONPATH:/path/z3-4.7.1-x64-ubuntu-16.04/bin/python I After the setup the following call should throw no error

$ python3 /path/z3-4.7.1-x64-ubuntu-16.04/bin/python/example.py

(7)

Topic 13.2

Using solver

(8)

Steps of using Z3 via python interface

f r o m z3 i m p o r t * # l o a d z3 l i b r a r y

p1 = B o o l ( " p1 ") # d e c l a r e a B o o l e a n v a r i a b l e p2 = B o o l ( " p2 ")

phi = Or ( p1 , p2 ) # c o n s t r u c t the f o r m u l a p r i n t ( phi ) # p r i n t i n g the f o r m u l a s = S o l v e r () # a l l o c a t e s o l v e r

s . add ( phi ) # add f o r m u l a to the s o l v e r r = s . c h e c k () # c h e c k s a t i s f i a b i l i t y

if r == sat : p r i n t ( " sat ") e l s e :

p r i n t ( " u n s a t " ) # s a v e the s c r i p t t e s t . py

# run \ $ p y t h o n 3 t e s t . py

(9)

Get a model

r = s . c h e c k () if r == sat :

m = s . m o d e l () # r e a d m o d e l p r i n t ( m ) # p r i n t m o d e l e l s e :

p r i n t ( " u n s a t " )

Exercise 13.2

What happens if we run m = s.model() in the unsat case?

(10)

Solve and print model

f r o m z3 i m p o r t *

# p a c k a g i n g s o l v i n g and m o d e l p r i n t i n g def s o l v e ( phi ):

s = S o l v e r () s . add ( phi ) r = s . c h e c k () if r == sat :

m = s . m o d e l () p r i n t ( m )

e l s e :

p r i n t (" u n s a t " )

# we w i l l use t h i s f u n c t i o n in l a t e r s l i d e s

(11)

Pointer and variable

There is a distinction between the Python variable name and the propositional variable it holds.

f r o m z3 i m p o r t * # l o a d z3 l i b r a r y

x = B o o l (" y " ) # c r e a t e s P r o p o s i t i o n a l v a r i a b l e y

z = x # p y t h o n p o i n t e r z a l s o h o l d s v a r i a b l e y

(12)

Exercise: encoding Boolean circuit

Exercise 13.3

Using Z3, find the input values of A, B, and C such that output D is 1.

A B

C

D

We know you can do it! Please do not shout the answer. Please make computer find it.

(13)

Topic 13.3

Solver engineering

(14)

Design of solvers: context vs. solver

Any complex software usually has a context object.

The context consists of a formula store containing the constructed formulas.

Z3 Python interface instantiates a default context. Therefore, we do not see it explicitly.

A Solver is a solving instance. There can be multiple solvers in a context.

The Solver solves only the added formula.

(15)

Formula handling

a = B o o l ( ’ a ’) b = B o o l ( ’ b ’) ab = And ( a , b )

# a c c e s s i n g sub - f o r m u l a s p r i n t ( ab . arg ( 0 ) )

p r i n t ( ab . arg ( 1 ) )

# a c c e s s i n g the s y m b o l at the h e a d a b _ d e c l = ab . d e c l ()

n a m e = a b _ d e c l . n a m e () if n a m e == " and " :

p r i n t ( " F o u n d an And ")

(16)

Topic 13.4

Problems

(17)

Exercise : Python programming

Exercise 13.4

Write a Python program that generates a random graph in a file edges.txt for n nodes and m edges, which are given as command line options.

Please store edges in edges.txt as the following sequence of tuples 10,12

30,50 ....

Exercise 13.5

Write a program that reads a directed graph from edges.txt and finds the number of strongly connected components in the graph

Exercise 13.6

Write a program that reads a directed graph from edges.txt and finds the cliques of size k,

which is given as a command line option.

(18)

Proving theorems

Exercise 13.7

Prove/disprove the following theorems using a solver

I Sky is blue. Space is black. Therefore sky and space are blue or black.

I Hammer and chainsaw are professional tools. Professional tools and vehicles are rugged.

Therefore, hammers are rugged.

(19)

Write a function: find positive variables

Exercise 13.8

Find the set of Boolean variables that occur only positively in a propositional logic formula.

An occurrence of a variable is positive if there are even number of negations from the occurrence to the root of the formula.