\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=blue,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}
\usepackage{amsmath}
\usepackage{stmaryrd}   % for the tval symbol
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{trees}
\newcommand{\fn}[1]{\mathrm{#1}}
\newcommand{\append}{\mathbin{+\mkern-10mu+}}
\newcommand{\cons}{\mathbin{::}}
\newcommand{\tval}[1]{\llbracket #1 \rrbracket}
\newcommand{\liff}{\leftrightarrow}
% If you don't have the stmaryrd package, the following substitute will do.
%\newcommand{\tval}[1]{[\![ #1 ]\!]}

\pagestyle{fancy}
\fancyhf{}
\renewcommand{\headrulewidth}{0pt}

\lhead{\sf Logic and Mechanized Reasoning}
\rhead{\sf Fall 2021}


\begin{document}

\bigskip

\begin{center}
{\Large Assignment 7}

\medskip

due 6pm Thursday, October 21, 2021
\end{center}

\medskip

\thispagestyle{fancy}

\subsection*{Problem 1 (18 points)}

The game Number Mind is a variant of the well known game Master Mind by Project Euler.\footnote{\url{https://projecteuler.net/problem=185}}
Instead of colored pegs, you have to guess a secret sequence of digits.
After each guess you are only told in how many places you have guessed the
correct digit. So, if the sequence was {\tt 1234} and you guessed {\tt 2036},
you would be told that you have one correct digit; however, you would {\bf not} be told
that you also have another digit in the wrong place.

\medskip

\noindent
For instance, given the following guesses for a 5-digit secret sequence,

\begin{verbatim}
    90342 ;2 correct
    70794 ;0 correct
    39458 ;2 correct
    34109 ;1 correct
    51545 ;2 correct
    12531 ;1 correct
\end{verbatim}

\noindent
The correct sequence {\tt 39542} is unique.

\bigskip

\noindent
Based on the following guesses,
\begin{verbatim}
    5616185650518293 ;2 correct
    3847439647293047 ;1 correct
    5855462940810587 ;3 correct
    9742855507068353 ;3 correct
    4296849643607543 ;3 correct
    3174248439465858 ;1 correct
    4513559094146117 ;2 correct
    7890971548908067 ;3 correct
    8157356344118483 ;1 correct
    2615250744386899 ;2 correct
    8690095851526254 ;3 correct
    6375711915077050 ;1 correct
    6913859173121360 ;1 correct
    6442889055042768 ;2 correct
    2321386104303845 ;0 correct
    2326509471271448 ;2 correct
    5251583379644322 ;2 correct
    1748270476758276 ;3 correct
    4895722652190306 ;1 correct
    3041631117224635 ;3 correct
    1841236454324589 ;3 correct
    2659862637316867 ;2 correct
\end{verbatim}
the goal of the assignment is to find the unique 16-digit secret sequence.

\newpage

\noindent
A) (6 points) Write in Lean a function that takes as input a {\tt List Lit} and a natural number $k$
and returns a propositional formula of Lean data type {\tt CnfForm} that is satisfiable if and 
only if exactly $k$ literals of list are satisfied. (Hint: The easiest way to encode that
exactly $k$ literals are true is by splitting it in at-least $k$ are true and at-most $k$ are true. No auxiliary propositional variables are required.)  

\medskip

\noindent
B) (5 points) Write a Lean program that can solve Number Mind puzzles. The input is a list of 
exactly-$k$ constraints with a constraint being a list of literals and a number $k$. The meaning
of a constraint is that exactly $k$ of the literals are true. The program should 
return a formula of Lean data type {\tt CnfForm} that is satisfiable if and only if 
all constraints are satisfied. Note that Number Mind puzzles require i) constraints enforcing how many
digits are correct {\bf and} ii) constraints enforcing that for each position exactly $1$ digit can be
present in a solution. 


\medskip

\noindent
C) (3 points) Run the program to solve the Number Mind puzzle shown above with 16 digits
using the CaDiCaL interface. Transform the solution into a sequence of digits. 

\medskip

\noindent
D) (4 points) The solution of the Number Mind puzzle shown above is claimed to be unique. 
Show that this claim is correct. Please explain your approach, implement it, and solve it. 
(Hint: showing uniqueness cannot be done using a single propositional formula. 
You will need to construct an additional, but closely related, formula of the one solved in C).

\end{document}