Problem Solving via Satisfiability

Transcription

1 Problem Solving via Satisfiability 오학주 고려대학교정보대학컴퓨터학과 January 20, 2018

2 두가지소프트웨어기반분야 알고리즘및계산복잡도 소프트웨어로문제를해결하는방법에대한탐구 자료구조, 알고리즘, 계산이론, etc 형식논리및프로그래밍언어 소프트웨어를손쉽게잘만드는방법에대한탐구 프로그래밍언어, 컴파일러, 전산논리, etc

3 예: 퀵 정렬 (Quick Sort) Tony Hoare가 고안한 평균복잡도 O(N log N)의 정렬 알고리즘: 1. 리스트가 비었으면 그대로 리턴한다. 2. 리스트에서 원소(피봇)를 하나 고른다. 3. 피봇 앞에는 피봇보다 값이 작은 모든 원소들을 모으고, 피봇 뒤에는 피봇보다 값이 큰 모든 원소들을 모은다: 피봇보다 작은 원소들(L1 ) + 피봇 + 피봇보다 큰 원소들(L2 ) 4. 두 리스트 L1 과 L2 에 대해서 재귀적으로 위 과정을 반복한다.

4 프로그래밍 언어가 생각의 틀을 결정

5 프로그래밍언어가생각의틀을결정 qsort: stmfd sp!, {r4, r6, Save r4 and r6 for caller mov r6, r6 <- right qsort_tailcall_entry: sub r7, r6, If right - left <= 1 (already sorted), cmp r7, #1 ldmlefd sp!, {r4, r6, Return, restoring r4 and r6 ldr r7, [r0, r1, asl r7 <- a[left], gets pivot element add r2, r1, l <- left + 1 mov r4, r <- right partition_loop: ldr r3, [r0, r2, asl r3 <- a[l] cmp r3, If a[l] <= pivot_element, addle r2, r2, increment l, and ble continue to next iteration. sub r4, r4, Otherwise, decrement r, ldr r5, [r0, r4, asl and swap a[l] and a[r]. str r5, [r0, r2, asl #2] str r3, [r0, r4, asl #2] partition_test: cmp r2, If l < r, blt continue iterating. partition_finish: sub r2, r2, Decrement l ldr r3, [r0, r2, asl Swap a[l] and pivot

6 프로그래밍언어가생각의틀을결정 void swap(int* a, int* b) { int t = *a; *a = *b; *b = t; } int partition (int arr[], int low, int high) { int pivot = arr[high]; int i = (low - 1); } for (int j = low; j <= high- 1; j++) { if (arr[j] <= pivot) { i++; swap(&arr[i], &arr[j]); } } swap(&arr[i + 1], &arr[high]); return (i + 1); void quicksort(int arr[], int low, int high) { if (low < high) { int pi = partition(arr, low, high); quicksort(arr, low, pi - 1); quicksort(arr, pi + 1, high); } }

7 프로그래밍언어가생각의틀을결정 quicksort [] = [] quicksort (x:xs) = quicksort ys ++ [x] ++ quicksort zs where ys = [a a <- xs, a <=x] zs = [b b <- xs, b > x] cf) 1. 리스트가비었으면그대로리턴한다. 2. 리스트에서원소 ( 피봇 ) 를하나고른다. 3. 피봇앞에는피봇보다값이작은모든원소들을모으고, 피봇뒤에는피봇보다값이큰모든원소들을모은다 : 피봇보다작은원소들 (L 1 ) + 피봇 + 피봇보다큰원소들 (L 2 ) 4. 두리스트 L 1 과 L 2 에대해서재귀적으로위과정을반복한다.

8 소프트웨어자동디버깅기술 소프트웨어오류자동탐지및수정

9 소프트웨어검증기술 : 0 l u < a sorted(a, l, : rv i.l i u a[i] = e bool BinarySearch (int a[], int l, int u, int e) { if (l > u) return false; else { int m := (l + u) div 2; if (a[m] = e) return true; else if (a[m] < e) return BinarySearch (a, m + 1, u, e) else return BinarySearch (a, l, m 1, e) } }

10 자동프로그래밍기술 의도로부터소프트웨어를자동합성

11 기본기 : Logic An introduction to formal logic and satisfiability Propositional logic and satisfiability Problem solving via satisfiability First-order logic and satisfiability

12 Proposition and Satisfiability 명제 : 참또는거짓인문장, 비가온다 (P) 날이흐리다 (Q) 비가오지않는다 ( P) 비가오고날이흐리다 (P Q) 비가오거나날이흐리다 (P Q) 비가오면날이흐리다 (P Q) Satisfiability: 주어진명제가참이될수있는지여부, P Q P P P P P Q

13 Syntax of Propositional Logic Atom: basic elements truth symbols ( false ) and ( true ) propositional variables P, Q, R,... Literal: an atom α or its negation α. Formula: a literal or the application of a logical connective to formulas: F negation ( not ) F 1 F 2 conjunction ( and ) F 1 F 2 disjunction ( or ) F 1 F 2 implication ( implies ) F 1 F 2 iff ( if and only if )

14 Semantics of Propositional Logic The meaning of a PL formula is either true or false. It is defined with an interpretation that assigns truth values to propositional variables. For example, under I : {P true, Q false}, the formula F : P Q P Q evaluates to true. Under I : {P true, Q true}, F evaluates to false. We write I F if F evaluates to true under I. satisfying interpretation We write I F if F evaluates to false under I. falsifying interpretation

15 Semantics of Propositional Logic 귀납적으로정의 (inductive definition): I, I, for any I I P iff I [P] = true I P iff I [P] = false I F iff I F I F 1 F 2 iff I F 1 and I F 2 I F 1 F 2 iff I F 1 or I F 2 I F 1 F 2 iff I F 1 or I F 2 I F 1 F 2 iff (I F 1 and I F 2 ) or (I F 1 and I F 2 )

16 Example 1 Consider the formula F : P Q P Q and the interpretation I : {P true, Q false} The truth value of F is computed as follows: 1. I P since I [P] = true 2. I Q since I [Q] = false 3. I Q by 2 and semantics of 4. I P Q by 2 and semantics of 5. I P Q by 1 and semantics of 6. I F by 4 and semantics of

17 Example 2 What is the truth value of (P Q) (Q R) under I = {P false, Q true, R true}?

18 Satisfiability and Validity A formula F is satisfiable iff there exists an interpretation I such that I F. Otherwise, F is unsatisfiable. A formula F is valid iff for all interpretations I, I F. Otherwise, F is invalid. Satisfiability and validity are dual: F is valid iff F is unsatisfiable Thus, we can check satisfiability by deciding validity, and vice versa. The first known NP-complete problem. No efficient algorithm exists (for all instances). Every decision problem in the NP class can be reduced to the boolean satisfiability problem.

19 Examples Determine satisfiability and validity of the formulas: F 1 : P Q P Q F 2 : P Q P Q F 3 : P Q P Q F 4 : P Q (Q P)

20 Deciding Satisfiability and Validity Two approaches to show F is valid: Truth table method (exhaustive search). Semantic argument method (deduction).

21 Truth Table Method F : P Q P Q Thus, F is valid. P Q P Q Q P Q F Truth table method is brute-force and impractical. Also, it is not applicable to logic where domain is infinite (e.g., first-order logic).

22 Semantic Argument Method ( 귀류법 ) Semantic argument method is essentially a proof by contradiction, and is applicable to logics with infinite domain. Main idea: Assume F is not valid: there exists some falsifying interpretation I such that I F. Apply proof rules. If we derive a contradiction in every case of the proof, then F is valid. If there is some branch where we cannot derive (after applying all proof rules), then F is not valid.

23 Proof Rules for Propositional Logic I F I F I F G I F, I G I F G I F I G I F G I F I G I F G I F G I F G I F I F I F I F I I F G I F I G I F G I F, I G I F G I F, I G I F G I F G I F G

24 Example 1 To prove that the formula F : P Q P Q is valid, assume that it is invalid and derive a contradiction: 1. I P Q P Q assumption 2. I P Q by 1 and semantics of 3. I P Q by 1 and semantics of 4. I P by 2 and semantics of 5. I P by 3 and semantics of 6. I 4 and 5 are contradictory

25 Example 2 To prove that the formula F : (P Q) (Q R) (P R) is valid, assume that it is invalid and derive a contradiction: 1. I F assumption 2. I (P Q) (Q R) by 1 and semantics of 3. I P R by 1 and semantics of 4. I P by 3 and semantics of 5. I R by 3 and semantics of 6. I P Q 2 and semantics of 7. I Q R 2 and semantics of Two cases consider from 6: 1. I P: contradiction with I Q: two cases to consider from 7: 2.1 I Q: contradiction 2.2 I R: contradiction with 5.

26 Equivalence and Implication Two formulas F 1 and F 2 are equivalent F 1 F 2 iff F 1 F 2 is valid, i.e., for all interpretations I, I F 1 F 2. Formula F 1 implies formula F 2 F 1 = F 2 iff F 1 F 2 is valid, i.e., for all interpretations I, I F 1 F 2. Note F 1 F 2 and F 1 = F 2 are assertions, not formulas. We can check equivalence and implication by checking satisfiability. How?

27 Examples P P P Q P Q R ( R P) = P

28 Normal Forms A normal form of formulas is a syntactic restriction such that for every formula of the logic, there is an equivalent formula in the normal form. Three useful normal forms in logic: Negation Normal Form (NNF) Disjunctive Normal Form (DNF) Conjunctive Normal Form (CNF)

29 Negation Normal Form (NNF) NNF requires that,, and are the only connectives (i.e., no and ) and that negations appear only in literals. P Q (R S) P (P Q) P Q Transforming a formula F to equivalent formula F in NNF can be done by repeatedly applying the following equivalences: F 1 F 1 (F 1 F 2 ) F 1 F 2 (F 1 F 2 ) F 1 F 2 F 1 F 2 F 1 F 2 F 1 F 2 (F 1 F 2 ) (F 2 F 1 )

30 Disjunctive Normal Form (DNF) A formula is in disjunctive normal form (DNF) if it is a disjunction of conjunctive clauses (conjunctions of literals): i To convert a formula F into an equivalent formula in DNF, transform F into NNF and then distribute conjunctions over disjunctions: j (F 1 F 2 ) F 3 (F 1 F 3 ) (F 2 F 3 ) F 1 (F 2 F 3 ) (F 1 F 2 ) (F 1 F 3 ) l i,j

31 Example To convert F : (Q 1 Q 2 ) ( R 1 R 2 ) into DNF, first transform it into NNF: F : (Q 1 Q 2 ) (R 1 R 2 ) then apply distributivity: F : (Q 1 (R 1 R 2 )) (Q 2 (R 1 R 2 )) and then: F : (Q 1 R 1 ) (Q 1 R 2 ) (Q 2 R 1 ) (Q 2 R 2 ))

32 Conjunctive Normal Form (CNF) A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses (i.e. conjunctions of disjunctions of literals): i To convert a formula F into an equivalent formula in DNF, transform F into NNF and distribute disjunctions over conjunctions: j (F 1 F 2 ) F 3 (F 1 F 3 ) (F 2 F 3 ) F 1 (F 2 F 3 ) (F 1 F 2 ) (F 1 F 3 ) l i,j

33 Example To convert F : (Q 1 Q 2 ) ( R 1 R 2 ) into CNF, transform F into NNF: F : (Q 1 Q 2 ) (R 1 R 2 ) Then apply distributivity: F : (Q 1 R 1 R 2 ) (Q 2 R 1 R 2 )

34 Decision Procedures (Satisfiability Solvers) A decision procedure decides whether F is satisfiable after some finite steps of computation. Approaches for deciding satisfiability: Search: exhaustively search through all possible assignments Deduction: deduce facts from known facts by iteratively applying proof rules Combination: Modern SAT solvers combine search and deduction in an effective way

35 Exhaustive Search The recursive algorithm for deciding satisfiability: let rec SAT F = if F = then true else if F = then false else let P = Choose(vars(F )) in (SAT F {P }) (SAT F {P }) When applying F {P } and F {P }, the resulting formulas should be simplified using equivalences on PL. F F F F F F F F F F F F F F...

36 Example 1 F : (P Q) P Q Choose variable P and F {P } : ( Q) Q which simplifies to F 1 : Q Q F 1 {Q } : F 1 {Q } : Recurse on the other branch for P in F : F {P } : ( Q) Q which simplifies to. All branches end without finding a satisfying assignment.

37 Example 2 F : (P Q) P Choose P and recurse on the first case: which is equivalent to. Try the other case: which is equivalent to. F {P } : ( Q) T F {P } : ( Q) Arbitrarily assigning a value to Q produces the satisfying interpretation: I : {P false, Q true}.

38 DPLL Applicable only to CNF formulas. The Davis-Putnam-Logemann-Loveland algorithm (DPLL) combines the enumerative search and a restricted form of deduction, called unit resolution. If a set of clauses contains a unit clause l, we can simplify the other clauses as follows: Every clause (other than the unit clause itself) containing l is removed, In every clause that contains l this literal is deleted. The process of applying this resolution as much as possible is called Boolean constraint propagation (BCP).

39 BCP Example (a b) ( a c) ( c d) a Apply unit resolution for a produces c ( c d) a. Applying unit resolution for c produces c d a The result is equivalent to the original formula.

40 DPLL DPLL is similar to SAT, except that it begins by applying BCP: let rec DPLL F = let F = BCP(F ) in if F = then true else if F = then false else let P = Choose(vars(F )) in (DPLL F {P }) (DPLL F {P })

41 Practical SAT Solvers Over the past decades, significant effort has been devoted to improving SAT solvers. As the result, modern SAT solvers are extremely scalable for practical instances.

42 Z3 A state-of-the-art SAT/SMT solver: Supported theories: Propositional Logic Theory of Equality Uninterpreted Functions Arithmetic Arrays Bit-vectors,... References Z3 Guide Z3 API in Python http: //ericpony.github.io/z3py-tutorial/guide-examples.htm

43 Example F 1 : P Q P Q F 2 : P Q P Q F 3 : (P Q) (Q R) (P Q) 1 from z3 import 2 p = Bool ( P ) 3 q = Bool ( Q ) 4 r = Bool ( R ) 5 f 1 = I m p l i e s ( And ( p, q ), Or ( p, q ) ) 6 f 2 = I m p l i e s ( Or ( p, q ), And ( p, q ) ) 7 f 3 = I m p l i e s ( And ( I m p l i e s ( p, q ), I m p l i e s ( q, r ) ), I m p l i e s ( p, q ) ) 8 p r o v e ( f 1 ) 9 p r o v e ( f 2 ) 10 p r o v e ( f 3 ) $ python test.py proved counterexample [Q = True, P = False] proved

44 Example 1 from z3 import 2 3 p = Bool ( P ) 4 q = Bool ( Q ) 5 r = Bool ( R ) 6 7 f 1 = I m p l i e s ( And ( p, q ), Or ( p, q ) ) 8 f 2 = I m p l i e s ( Or ( p, q ), And ( p, q ) ) 9 10 s = S o l v e r ( ) 11 s. add ( Not ( f 1 ) ) 12 p r i n t s. check ( ) s = S o l v e r ( ) 15 s. add ( Not ( f 2 ) ) 16 p r i n t s. check ( ) unsat sat

45 Arithmetic 1 from z3 import 2 3 x = I n t ( x ) 4 y = I n t ( y ) 5 s o l v e ( x > 2, y < 10, x + 2 y == 7) 6 7 x = Real ( x ) 8 y = Real ( y ) 9 s o l v e ( x 2 + y 2 > 3, x 3 + y < 5) $ python test.py [y = 0, x = 7] [x = 1/8, y = 2]

46 BitVectors 1 x = BitVec ( x, 32) 2 y = BitVec ( y, 32) 3 4 s o l v e ( x & y == y ) 5 s o l v e ( x >> 2 == 3) 6 s o l v e ( x << 2 == 3) 7 s o l v e ( x << 2 == 24) [y = , x = 0] [x = 12] no solution [x = 6]

47 Uninterpreted Functions 1 x = I n t ( x ) 2 y = I n t ( y ) 3 f = F u n c t i o n ( f, I n t S o r t ( ), I n t S o r t ( ) ) 4 5 s = S o l v e r ( ) 6 s. add ( f ( f ( x ) ) == x, f ( x ) == y, x!= y ) 7 8 p r i n t s. check ( ) 9 10 m = s. model ( ) 11 p r i n t m p r i n t f ( f ( x ) ) =, m. e v a l u a t e ( f ( f ( x ) ) ) 14 p r i n t f ( x ) =, m. e v a l u a t e ( f ( x ) ) sat [x = 0, y = 1, f = [0 -> 1, 1 -> 0, else -> 1]] f(f(x)) = 0 f(x) = 1

48 Constraint Generation with List Comprehension 1 X = [ I n t ( x%s % i ) f o r i i n range ( 5 ) ] 2 Y = [ I n t ( y%s % i ) f o r i i n range ( 5 ) ] 3 p r i n t X, Y 4 X plus Y = [ X[ i ] + Y[ i ] f o r i i n range ( 5 ) ] 5 X gt Y = [ X[ i ] > Y[ i ] f o r i i n range ( 5 ) ] 6 p r i n t X plus Y 7 p r i n t X gt Y 8 a = And ( X gt Y ) 9 p r i n t a 10 s o l v e ( a ) [x0, x1, x2, x3, x4] [y0, y1, y2, y3, y4] [x0 + y0, x1 + y1, x2 + y2, x3 + y3, x4 + y4] [x0 > y0, x1 > y1, x2 > y2, x3 > y3, x4 > y4] And(x0 > y0, x1 > y1, x2 > y2, x3 > y3, x4 > y4) [y4 = 0, x4 = 1, y3 = 0, x3 = 1, y2 = 0, x2 = 1, y1 = 0, x1 = 1, y0 = 0, x0 = 1]

49 Problem 1: Program Equivalence Consider the two code fragments. if (!a&&!b) then h else if (!a) then g else f if (a) then f else if (b) then g else h The latter might have been generated from an optimizing compiler. We would like to prove that the two programs are equivalent.

50 Encoding in Propositional Logic The if-then-else construct can be replaced by a PL formula as follows: if x then y else z (x y) ( x z) The problem of checking the equivalence is to check the validity of the formula: F : ( a b) h ( a b) ( a g a f ) a f a (b g b h) If F is unsatisfiable, the two expressions are equivalent.

51 In Python 1 from z3 import 2 3 a = Bool ( a ) 4 b = Bool ( b ) 5 f = Bool ( f ) 6 g = Bool ( g ) 7 h = Bool ( h ) 8 9 f 1 = Or ( And ( And ( Not ( a ), Not ( b ) ), h ), And ( Not ( And ( Not ( a ), Not ( b ) ) ), ( Or ( And ( Not ( a ), g ), And ( a, f ) ) ) ) ) 10 f 2 = Or ( And ( a, f ), And ( Not ( a ), Or ( And ( b, g ), And ( Not ( b ), h ) ) ) ) s o l v e ( Not ( f 1==f 2 ) ) $ python equiv.py no solution

52 Problem 2: Seat Assignment Consider three persons A, B, and C who need to be seated in a row. There are three constraints: A does not want to sit next to C A does not want to sit in the leftmost chair B does not want to sit to the right of C We would like to check if there is a seat assignment for the three persons that satisfies the above constraints.

53 Encoding in Propositional Logic To encode the problem, let X ij be boolean variables such that X ij person i seats in chair j We need to encode two types of constraints. Valid assignments: Every person is seated Every seat is occupied i j j i X ij X ij One person per seat (X ij = X ik ) k j i,j

54 Encoding in Propositional Logic Problem constraints: A does not want to sit next to C: (X 00 = X 21) (X 01 = ( X 20 X 22)) (X 02 = X 21) A does not want to sit in the leftmost chair X 00 B does not want to sit to the right of C (X 20 = X 11 ) (X 21 = X 12 )

55 In Python 1 from z3 import 2 3 X = [ [ Bool ( x %s %s % ( i +1, j +1) ) f o r j i n range ( 3 ) ] f o r i i n range ( 3 ) ] 4 5 # e v e r y p e r s o n i s s e a t e d 6 v a l c 1 = [ ] 7 f o r i i n range ( 3 ) : 8 c = F a l s e 9 f o r j i n range ( 3 ) : 10 c = Or ( c, X[ i ] [ j ] ) 11 v a l c 1. append ( c ) # e v e r y s e a t i s o c c u p i e d 14 v a l c 2 = [ ] 15 f o r j i n range ( 3 ) : 16 c = F a l s e 17 f o r i i n range ( 3 ) : 18 c = Or ( c, X[ i ] [ j ] ) 19 v a l c 2. append ( c )

56 In Python 1 # one p e r s o n p e r s e a t 2 v a l c 3 = [ ] 3 f o r i i n range ( 3 ) : 4 f o r j i n range ( 3 ) : 5 c = True 6 f o r k i n range ( 3 ) : 7 i f k <> j : 8 c = And ( c, X[ i ] [ k ] == F a l s e ) 9 v a l c 3. append ( I m p l i e s (X[ i ] [ j ] == True, c ) ) v a l i d = v a l c 1 + v a l c 2 + v a l c # A does not want to s i t n e x t to C 14 c1 = [ I m p l i e s (X [ 0 ] [ 0 ] == True, X [ 2 ] [ 1 ] == F a l s e ), 15 I m p l i e s (X [ 0 ] [ 1 ] == True, And (X [ 2 ] [ 0 ] == F a l s e, X [ 2 ] [ 2 ] == F a l s e ) ), 16 I m p l i e s (X [ 0 ] [ 2 ] == True, X [ 2 ] [ 1 ] == F a l s e ) ]

57 In Python 1 # A does not want to s i t i n the l e f t c h a i r 2 c2 = [X [ 0 ] [ 0 ] == F a l s e ] 3 4 # B does not want to s i t to the r i g h t o f C 5 c3 = [ I m p l i e s (X [ 2 ] [ 0 ] == True, X [ 1 ] [ 1 ] == F a l s e ), 6 I m p l i e s (X [ 2 ] [ 1 ] == True, X [ 1 ] [ 2 ] == F a l s e ) ] 7 8 c = c1 + c2 + c3 9 s o l v e ( v a l i d + c ) $ python equiv.py no solution

58 Problem 3: Radio Station Let S = {s 1,..., s n } be a set of radio stations, each of which has to be allocated one of k transmission frequencies, for some k < n. Two stations that are too close to each other cannot have the same frequency. The set of pairs having this constraint is denoted by E. Find a frequency assignment.

59 Encoding in Propositional Logic X ij station i is assigned frequency j Every station is assigned at least one frequency: Every station is assigned not more than one frequency: Close stations are not assigned the same frequency:

60 Problem 4: Sudoku Insert the numbers in the 9 9 board so that each row, column, and 3 3 boxes must contain digits 1 through 9 exactly once.

61 Encoding in SMT formulas X ij : number in position (i, j), for i, j [0, 8] Each cell contains a value in {1,..., 9}: X ij 9 i=0 j=0 Each row contains a digit at most once: (j k = X ij X ik ) i=0 j=0 k=0 Each column contains a digit at most once: (i k = X ij X kj ) j=0 i=0 k=0

62 Encoding in SMT formulas Each 3 3 square contains a digit at most once: ( (i i j j ) = i 0 =0 j 0 =0 i=0 j=0 i =0 j =0 i=0 j=0 X 3i0 +i,3j 0 +j X 3i0 +i,3j 0 +j ) Board configuration (stored in B, where 0 means empty): 8 8 (B[i][j] 0 = B[i][j] = X ij )

63 Python Implementation 1 from z3 import 2 X = [ [ I n t ( x %s %s % ( i +1, j +1) ) f o r j i n range ( 9 ) ] f o r i i n range ( 9 ) ] 3 4 # each c e l l c o n t a i n s a v a l u e i n { 1,..., 9 } 5 c e l l s c = [ ] 6 f o r i i n range ( 9 ) : 7 f o r j i n range ( 9 ) : 8 c e l l s c. append ( And (1 <= X[ i ] [ j ], X[ i ] [ j ] <= 9) ) 9 10 # each row c o n t a i n s a d i g i t at most once 11 r o w s c = [ ] 12 f o r i i n range ( 9 ) : 13 f o r j i n range ( 9 ) : 14 f o r k i n range ( 9 ) : 15 r o w s c. append ( I m p l i e s ( j <>k, X[ i ] [ j ]<>X[ i ] [ k ] ) )

64 Python Implementation 1 # each column c o n t a i n s a d i g i t at most once 2 c o l s c = [ ] 3 f o r j i n range ( 9 ) : 4 f o r i i n range ( 9 ) : 5 f o r k i n range ( 9 ) : 6 c o l s c. append ( I m p l i e s ( i <>k, X[ i ] [ j ]<>X[ k ] [ j ] ) ) 7 8 # each 3 x3 s q u a r e c o n t a i n s a d i g i t at most once 9 s q c = [ ] 10 f o r i 0 i n range ( 3 ) : 11 f o r j 0 i n range ( 3 ) : 12 f o r i i n range ( 3 ) : 13 f o r j i n range ( 3 ) : 14 f o r i 2 i n range ( 3 ) : 15 f o r j 2 i n range ( 3 ) : 16 s q c. append ( I m p l i e s ( Or ( i <>i2, j <>j 2 ), X[ 3 i 0+i ] [ 3 j 0+j ] <> X[ 3 i 0+i 2 ] [ 3 j 0+j 2 ] ) ) c = c e l l s c + r o w s c +c o l s c + s q c

65 Python Implementation 1 i n s t a n c e = ( ( 0, 8, 2, 0, 0, 5, 0, 0, 0 ), 2 ( 0, 0, 0, 6, 0, 0, 2, 0, 0 ), 3 ( 6, 0, 0, 0, 0, 1, 0, 0, 0 ), 4 ( 5, 0, 0, 0, 0, 0, 0, 0, 0 ), 5 ( 0, 0, 0, 4, 0, 2, 0, 0, 0 ), 6 ( 0, 0, 0, 0, 0, 0, 0, 0, 6 ), 7 ( 0, 0, 0, 8, 0, 0, 0, 0, 5 ), 8 ( 0, 0, 8, 0, 0, 9, 0, 0, 0 ), 9 ( 0, 0, 0, 5, 0, 0, 4, 3, 0 ) ) 10 i n s t a n c e c = [ I f ( i n s t a n c e [ i ] [ j ] == 0, 11 True, X[ i ] [ j ] == i n s t a n c e [ i ] [ j ] ) 12 f o r i i n range ( 9 ) f o r j i n range ( 9 ) ] 13 s = S o l v e r ( ) 14 s. add ( sudoku c + i n s t a n c e c ) 15 i f s. check ( ) == s a t : 16 m = s. model ( ) 17 r = [ [ m. e v a l u a t e (X[ i ] [ j ] ) f o r j i n range ( 9 ) ] 18 f o r i i n range ( 9 ) ] 19 p r i n t m a t r i x ( r ) 20 e l s e : 21 p r i n t f a i l e d to s o l v e

66 Python Implementation $ python sudoku.py [[3, 8, 2, 9, 7, 5, 1, 6, 4], [1, 7, 5, 6, 8, 4, 2, 9, 3], [6, 9, 4, 2, 3, 1, 8, 5, 7], [5, 2, 7, 1, 6, 8, 3, 4, 9], [9, 3, 6, 4, 5, 2, 7, 8, 1], [8, 4, 1, 7, 9, 3, 5, 2, 6], [4, 1, 3, 8, 2, 6, 9, 7, 5], [7, 5, 8, 3, 4, 9, 6, 1, 2], [2, 6, 9, 5, 1, 7, 4, 3, 8]]

67 Problem 5: Eight Queens The eight queens puzzle is the problem of placing eight chess queens on an 8x8 chessboard so that no two queens attack each other. Thus, a solution requires that no two queens share the same row, column, or diagonal.

68 Encoding Define boolean variables Q i as follows: Q i : the column position of the queen in row i Each queen is in a column {1,..., 8}: 8 1 Q i Q i 8 i=1 No queens share the same column: 8 8 (i j = Q i Q j ) i=1 j=1 i=1 j=1 No queens share the same diagonal: 8 i (i j = Q i Q j i j Q i Q j j i)

69 In Python 1 from z3 import 2 3 d e f p r i n t b o a r d ( r ) : 4 f o r i i n range ( 8 ) : 5 f o r j i n range ( 8 ) : 6 i f r [ i ] == j +1: 7 p r i n t 1, 8 e l s e : 9 p r i n t 0, 10 p r i n t Q = [ I n t ( Q %i % ( i +1) ) f o r i i n range ( 8 ) ] v a l c = [ And (1 <= Q[ i ], Q[ i ] <= 8) 15 f o r i i n range ( 8 ) ] 16 c o l c = [ I m p l i e s ( i <> j, Q[ i ] <> Q[ j ] ) 17 f o r i i n range ( 8 ) f o r j i n range ( 8 ) ] 18 d i a g c = [ I m p l i e s ( i <> j, 19 And (Q[ i ] Q[ j ]!= i j, 20 Q[ i ] Q[ j ]!= j i ) ) 21 f o r i i n range ( 8 ) f o r j i n range ( i ) ]

70 In Python 1 s = S o l v e r ( ) 2 s. add ( v a l c + c o l c + d i a g c ) 3 r e s = s. check ( ) 4 i f r e s == s a t : 5 m = s. model ( ) 6 r = [ m. e v a l u a t e (Q[ i ] ) f o r i i n range ( 8 ) ] 7 p r i n t b o a r d ( r ) 8 p r i n t $ python queens.py

71 실습문제 1 대칭인해를서로다른해로생각할때 8- 퀸문제는총 92 개의해를가진다. 예를들어, 아래상태도해중하나이다 z3 를이용하여 92 개의모든해를출력하는프로그램을작성하시오.

72 실습문제 1 실행시키면다음과같이모든해와함께찾은개수를출력한다 Number of solutions : 92

73 실습문제 2 다음과같은이차원행렬을생각하자 A B C D E F 각가로줄 (A, B,..., F ) 은집합 X = {1, 2,..., 7} 의부분집합을의미한다. 예를들어, A 는집합 {1, 4, 7} 을의미한다. 집합 X 의모든원소를포함하되각원소가하나의가로줄에속하게되는가로줄의집합을찾는프로그램을작성하시오. 예를들어, 위예제의경우 {B, D, F } 가정답이며, {B, D, E} 또는 {A, E} 등은답이아니다.

74 연습문제 입출력포맷은다음과같다. 다음과같은텍스트파일을입력으로받는다 : 가로줄의집합을다음과같이출력한다 : 답이없으면 No solution 을출력한다.

75 First-Order Logic An extension of propositional logic with predicates, functions, and quantifiers. John likes all sports. x.sports(x) likes(john, x) John does not like some sports. x.sports(x) likes(john, x) Every mother is older than her children. x.older(mother(x), x) The length of one side of a triangle is less than the sum of the lengths of the other two sides. x, y, z.triangle(x, y, z) length(x) < length(y) + length(z)

76 Exercises John only likes sports. Fermat s Last Theorem. (a, b,c가양의정수이고, n이 3 이상의정수일때, 항상 a n + b n c n 이다.) Given: integer, >,, +, x n

77 Terms While formulas in PL evaluate to true or false, terms in FOL evaluate to values other than truth values such as integers. Basic terms are variables (x, y,... ) and constants (a, b,... ). Composite terms include n-ary functions applied to n terms, i.e., f (t 1,..., t n ), where t i s are terms. A constant can be viewed as a 0-ary function. Examples: f (a), a unary function f applied to a constant g(x, b), a binary function g applied to a variable x and a constant b f (g(x, f (b)))

78 Predicates The propositional variables of PL are generalized to predicates in FOL, denoted p, q, r,.... An n-ary predicate takes n terms as arguments. A FOL propositional variable is a 0-ary predicate, denoted P, Q, R,.... Examples: P, a propositional variable (or 0-ary predicate) p(f (x), g(x, f (x))), a binary predicate applied to two terms

79 Syntax of First-Order Logic Atom: basic elements truth symbols ( false ) and ( true ) n-ary predicates applied to n terms Literal: an atom α or its negation α. Formula: a literal or the application of a logical connective (boolean connective) to formulas, or the application of a quantifier to a formula. F p(t 1,..., t n ) atom F negation ( not ) F 1 F 2 conjunction ( and ) F 1 F 2 disjunction ( or ) F 1 F 2 implication ( implies ) F 1 F 2 iff ( if and only if ) x.f [x] existential quantification x.f [x] universal quantification

80 Interpretation A FOL interpretation I : (D I, α I ) is a pair of a domain and an assignment. D I is a nonempty set of values such as integers, reals, etc. α I maps variables, constant, functions, and predicate symbols to elements, functions, and predicates over D I. each variable x is assigned a value from D I each n-ary function symbol f is assigned an n-ary function f I : DI n D I. each n-ary predicate symbol p is assigned an n-ary predicate p I : DI n {true, false}. Example: F : x + y > z y > z x Note +,, > are just symbols: p(f (x, y), z) p(y, g(z, x)). Domain: D I = Z = {..., 1, 0, 1,...} Assignment: α I = {+ + Z, Z, > > Z, x 13, y 42, z 1,...}

81 Semantics of First-Order Logic Given an interpretation I : (D I, α I ), I F or I F. I, I, I p(t 1,..., t n ) iff α I [p(t 1,..., t n )] = true I F iff I F I F 1 F 2 iff I F 1 and I F 2 I F 1 F 2 iff I F 1 or I F 2 I F 1 F 2 iff I F 1 or I F 2 I F 1 F 2 iff (I F 1 and I F 2 ) or (I F 1 and I F 2 ) I x.f iff for all v D I, I {x v} F I x.f iff there exists v D I, I {x v} F where J : I {x v} denotes an x-variant of I : D J = D I α J [y] = α I [y] for all constant, free variable, function, and predicate symbols y, except that α J (x) = v.

82 Example F : x.f (x) = g(x) Consider the interpretation I : (D : {v 1, v 2 }, α I ): α I : {f (v 1 ) v 1, f (v 2 ) v 2, g(v 1 ) v 2, g(v 2 ) v 1 } Compute the truth value of F under I as follows: 1. I {x v} f (x) = g(x) for v D 2. I x.f (x) = g(x) since v D is arbitrary

83 Satisfiability and Validity Suppose F is a closed FOL formula (no free variables). A formula F is satisfiable iff there exists an interpretation I such that I F. A formula F is valid iff for all interpretations I, I F. Duality still holds: F is valid F is unsatisfiable. Satisfiability for first-order logic is undecidable.

84 Examples Determine satisfiability and validity: x.x + 0 = 1 F : ( x.p(x)) ( x. p(x)) F : ( x.p(x, x)) ( x. y.p(x, y))

85 First-Order Theories In practice, we are not interested in pure logical validity (i.e. valid in all interpretations) of FOL formulas but in validity in a specific class of interpretations. E.g. x.x + 0 = 1 First-order logic is rather a general framework for building a specific, restricted logic, which provides a generic syntax and building blocks for defining the restrictions, called theories. First-order theories useful for reasoning about programs: Equality Integers, rationals, and reals Lists, arrays Pointers Bit-vectors...

86 Summary Propositional logic and satisfiability First-order logic and satisfiability Problem-solving as satisfiability Applications to programming systems