1. A binary adder is shown in Figure 1. The adder, on test inputs may be showing unintended results. Actually, the input values are: A = 1, B = 0, C = 1; and the output values are: D = 0 E = 0.
(a) Construct a weak-failure model of the circuit using PROPOSITIONAL LOGIC, that is a model that allows for faulty components. Explain each formula and its role in the model.
(b) You want to obtain minimal conflicts, that is, sets of components that cannot be all simultaneously working well at the light of the observation. (Minimality means in this case that no proper subset of a conflict is a conflict.)
Explain your methodology based on automated reasoning a` la Prover9 for obtaining such conflicts, in particular, how you make sure they are minimal.
(c) Use Prover9 to obtain all possible minimal conflicts. Show the main ingredients of the input file, with an explanation. Do the same with the output file, interpreting and explaining the results.
(d) Assume that a second test is performed (in addition to the first one). Now the values are: A = 1, B = 1, C = 1, and D = 0, E = 0. Now, using both sets of observations, find minimal conflicts through new Prover9 input, run and output.
Explain how and with what results you used the new informa- tion. Analyze the results in comparison with the previous diagnoses.