Q:

ASP simple program

In the following Program:
ide_drive       :- hard_drive, not scsi_drive. 
scsi_drive      :- hard_drive, not ide_drive. 
scsi_controller :- scsi_drive. 
hard_drive. 

The stable models are:
M1 = {hard_drive, ide_drive}
M2 = {hard_drive, scsi_drive, scsi_controller}

An stable model tells which atoms are true. 

Why M1 and M2 are stable models of the given program? 

A:

Let's call the variables $A,B,C,D$. So we are given
$$
\begin{align*}
A &\leftrightarrow D \land \lnot B \\
B &\leftrightarrow D \land \lnot A \\
C &\leftrightarrow B \\
D &
\end{align*}
$$
So $D$ must be true.  Also, $C = B$. The program simplifies to $A \leftrightarrow \lnot B$. So exactly one of $A,B$ is true.  If $A$ is true then $B,C$ are false, and conversely, if $A$ is false then $B,C$ are true.  So the "stable models" are
$$
\{A,D\}, \quad \{B,C,D\}. 
$$

