Problem 1: Modeling A nondeterministic finite automaton (NFA) is given by a 5-tuple (Q,8,8,1,F), where: . Q is a finite set of states is a finite alphabet .8:Qxx 2Q is a transition function ICQ is a set of initial states FCQ is a set of final (accepting) states An NFA accepts a finite word (or, a char sequence) w = [Co,...,Cn), where c E E, if and only if there is a sequence of states 90,...,In, with qi E Q, such that: 4o EI For all i E {1,...,n}, qi 8(li-1, W;) In EF 1-1 Given an NFA M = (1,5,8,1,F) and a fixed input string w, describe how to construct a propositional formula that is satisfiable if and only if M accepts w. Hint Consider defining propositional variables that correspond to the initial states, final states, transition function, and alphabet symbols in w. Then think about "unwinding" the NFA on w. Do you need to define additional variables? How can you encode the fact that w is accepted? 1-2 Demonstrate your encoding on the NFA shown in Figure 1. Q = {90, 91, 92, 93} = {0,1} 8 = {(90,0) 90 (90,1) 90, (90,0) 01, (90,1) H 92 (91,0) - 93, (22,1) 93, (93,0) + 93, (93,1) H+ 93} I = {90} F = {93} Figure 1: An NFA