{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# **Exercise 03. Count aggregates.**\n",
    "\n",
    "You may want to watch this [video](http://www.youtube.com/watch?v=e0zd-caqjOM&t=13m15s),\n",
    "where we explain sum aggregates in answer set programming.\n",
    "\n",
    "The video does not explain count aggregates, but they are very similar to sum aggregates.\n",
    "They also define a set, \n",
    "but they simply count the number of tuples in that set\n",
    "(instead of adding the first element of every tuple of that set)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### **1**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "c(5) d(2) e(3)\n",
      "SATISFIABLE\n"
     ]
    }
   ],
   "source": [
    "%%clingo -V0 0\n",
    "a(1,1). a(1,2). a(2,1). a(2,2). a(2,3).\n",
    "b(1,1).                 b(2,2).         b(3,3).\n",
    "\n",
    "% c(S) if S is the cardinality of the set\n",
    "%         of all tuples X,Y such that a(X,Y) belongs to the answer set.\n",
    "%         In this case the set is { 1,1; 1,2; 2,1; 2,2; 2,3 } and S is 5.\n",
    "c(S) :- S = #count{ X,Y : a(X,Y) }.\n",
    "            \n",
    "% d(S) if S is the cardinality of the set\n",
    "%         of all tuples X such that a(X,Y) belongs to the answer set.\n",
    "%         In this case the set is { 1; 2 } and S is 2.\n",
    "d(S) :- S = #count{   X : a(X,Y) }.\n",
    "\n",
    "% e(S) if S is the cardinality of the set\n",
    "%         of all tuples Y such that a(X,Y) belongs to the answer set.\n",
    "%         In this case the set is { 1; 2; 3 } and S is 3.\n",
    "e(S) :- S = #count{   Y : a(X,Y) }.\n",
    "\n",
    "#show c/1. #show d/1. #show e/1."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo -V0 0\n",
    "a(1,1). a(1,2).         a(2,2). a(2,3).\n",
    "b(1,1).                                 b(3,3).\n",
    "\n",
    "c(S) :- S = #count{ X,Y : a(X,Y) }.\n",
    "d(S) :- S = #count{   X : a(X,Y) }.\n",
    "e(S) :- S = #count{   Y : a(X,Y) }.\n",
    "\n",
    "#show c/1. #show d/1. #show e/1."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### **2**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "c(6) d(6) e(8) f(8)\n",
      "SATISFIABLE\n"
     ]
    }
   ],
   "source": [
    "%%clingo -V0 0\n",
    "a(1,1). a(1,2). a(2,1). a(2,2). a(2,3).\n",
    "b(1,1).                 b(2,2).         b(3,3).\n",
    "\n",
    "% c(S) if S is the cardinality of the set\n",
    "%         of all tuples X,Y such that a(X,Y) belongs to the answer set, and\n",
    "%            all tuples X,Y such that b(X,Y) belongs to the answer set.\n",
    "%         In this case the set is { 1,1; 1,2; 2,1; 2,2; 2,3; 3,3 } and S is 6.\n",
    "c(S) :- S = #count{   X,Y : a(X,Y);      X,Y : b(X,Y) }.\n",
    "    \n",
    "% d(S) if S is the cardinality of the set\n",
    "%         of all tuples X,Y such that a(X,Y) belongs to the answer set, and\n",
    "%            all tuples Z,W such that b(Z,W) belongs to the answer set.\n",
    "%         In this case the set is { 1,1; 1,2; 2,1; 2,2; 2,3; 3,3 } and S is 6.\n",
    "d(S) :- S = #count{   X,Y : a(X,Y);      Z,W : b(Z,W) }.\n",
    "\n",
    "% e(S) if S is the cardinality of the set\n",
    "%         of all tuples X,Y,1 such that a(X,Y) belongs to the answer set, and\n",
    "%            all tuples X,Y,2 such that b(X,Y) belongs to the answer set.\n",
    "%         In this case the set is { 1,1,1; 1,2,1; 2,1,1; 2,2,1; 2,3,1; 1,1,2; 2,2,2; 3,3,2 } and S is 8.\n",
    "e(S) :- S = #count{ X,Y,1 : a(X,Y);    X,Y,2 : b(X,Y) }. \n",
    "\n",
    "% f(S) if S is the cardinality of the set\n",
    "%         of all tuples X,Y   such that a(X,Y) belongs to the answer set, and\n",
    "%            all tuples X,Y,2 such that b(Z,W) belongs to the answer set.\n",
    "%         In this case the set is { 1,1; 1,2; 2,1; 2,2; 2,3; 1,1,2; 2,2,2; 3,3,2 } and S is 8.\n",
    "f(S) :- S = #count{   X,Y : a(X,Y);    X,Y,2 : b(X,Y) }. \n",
    " \n",
    "#show c/1. #show d/1. #show e/1. #show f/1. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo -V0 0\n",
    "a(1,1). a(1,2).         a(2,2). a(2,3).\n",
    "b(1,1).                                 b(3,3).\n",
    "\n",
    "c(S) :- S = #count{   X,Y : a(X,Y);      X,Y : b(X,Y) }.\n",
    "d(S) :- S = #count{   X,Y : a(X,Y);      Z,W : b(Z,W) }.\n",
    "e(S) :- S = #count{ X,Y,1 : a(X,Y);    X,Y,2 : b(X,Y) }. \n",
    "f(S) :- S = #count{   X,Y : a(X,Y);    X,Y,2 : b(X,Y) }. \n",
    " \n",
    "#show c/1. #show d/1. #show e/1. #show f/1. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### **3**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "d(1,2) d(2,3) e(1,3) e(2,4)\n",
      "SATISFIABLE\n"
     ]
    }
   ],
   "source": [
    "%%clingo -V0 0\n",
    "a(1,1). a(1,2). a(2,1). a(2,2). a(2,3).\n",
    "b(1,1).                 b(2,2).         b(3,3).\n",
    "c(1).           c(2).\n",
    "    \n",
    "% d(X,S) if c(X) and S is the cardinality of the set\n",
    "%           of all tuples Y such that a(X,Y) belongs to the answer set, and\n",
    "%              all tuples Z such that b(X,Z) belongs to the answer set.\n",
    "%           In this case when X is 1 the set is { 1; 2    } and S is 2, and\n",
    "%                        when X is 2 the set is { 1; 2; 3 } and S is 3.\n",
    "d(X,S) :- c(X), S = #count{   Y : a(X,Y);        Z : b(X,Z) }.\n",
    "\n",
    "% e(X,S) if c(X) and C is the cardinality of the set\n",
    "%           of all tuples Y,a such that a(X,Y) belongs to the answer set, and\n",
    "%              all tuples Z,b such that b(X,Z) belongs to the answer set.\n",
    "%           In this case when X is 1 the set is { 1,a; 2,a; 1,b      } and S is 3, and\n",
    "%                        when X is 2 the set is { 1,a; 2,a; 2,a; 2,b } and S is 4.\n",
    "e(X,S) :- c(X), S = #count{ Y,a : a(X,Y);      Z,b : b(X,Z) }.\n",
    "\n",
    "#show d/2. #show e/2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo -V0 0\n",
    "a(1,1). a(1,2).         a(2,2). a(2,3).\n",
    "b(1,1).                                 b(3,3).\n",
    "c(1).             c(2).\n",
    "\n",
    "d(X,S) :- c(X), S = #count{   Y : a(X,Y);        Z : b(X,Z) }.\n",
    "e(X,S) :- c(X), S = #count{ Y,a : a(X,Y);      Z,b : b(X,Z) }.\n",
    "\n",
    "#show d/2. #show e/2."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### **4**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "a(2)\n",
      "a(1)\n",
      "SATISFIABLE\n"
     ]
    }
   ],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..2).\n",
    "{ a(X) : n(X) }.\n",
    ":- 2 #count{ X : a(X) }.\n",
    "#show a/1."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..3).\n",
    "{ a(X) : n(X) }.\n",
    ":- 2 #count{ X : a(X) }.\n",
    "#show a/1."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### **5**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "a(1,2)\n",
      "a(2,1)\n",
      "a(2,2)\n",
      "a(1,1)\n",
      "SATISFIABLE\n"
     ]
    }
   ],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..2).\n",
    "{ a(X,Y) : n(X), n(Y) }.\n",
    ":- 2 #count{ X,Y : a(X,Y) }.\n",
    "#show a/2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..2).\n",
    "{ a(X,Y) : n(X), n(Y) }.\n",
    ":- 2 #count{ X : a(X,Y) }.\n",
    "#show a/2."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This time we have another exercise for the same example."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..2).\n",
    "{ a(X,Y) : n(X), n(Y) }.\n",
    ":- 2 #count{ Y : a(X,Y) }.\n",
    "#show a/2."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### **6**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "a(2,2) b(2,2)\n",
      "a(1,2) b(1,2)\n",
      "a(2,1) b(2,1)\n",
      "a(1,1) b(1,1)\n",
      "SATISFIABLE\n"
     ]
    }
   ],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..2).\n",
    "1 { a(X,Y) : n(X), n(Y) } 1.\n",
    "1 { b(X,Y) : n(X), n(Y) } 1.\n",
    ":- 2 #count{ X,Y : a(X,Y);   Z,W : b(Z,W) }.\n",
    "#show a/2. #show b/2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..2).\n",
    "1 { a(X,Y) : n(X), n(Y) } 1.\n",
    "1 { b(X,Y) : n(X), n(Y) } 1.\n",
    ":- 2 #count{ X,Y,a : a(X,Y);   Z,W,b : b(Z,W) }.\n",
    "#show a/2. #show b/2."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### **7**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "b(1,1) a(1,2) ok(1)\n",
      "a(1,1) b(1,2) ok(1)\n",
      "b(2,1) a(2,2) ok(2)\n",
      "a(2,1) b(2,2) ok(2)\n",
      "SATISFIABLE\n"
     ]
    }
   ],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..2).\n",
    "1 { a(X,Y) : n(X), n(Y) } 1.\n",
    "1 { b(X,Y) : n(X), n(Y) } 1.\n",
    "ok(X) :- 2 #count{ Y : a(X,Y);   Z : b(X,Z) }, n(X).\n",
    ":- not ok(1), not ok(2).\n",
    "#show a/2. #show b/2. #show ok/1."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo -V0 0\n",
    "n(1..2).\n",
    "1 { a(X,Y) : n(X), n(Y) } 1.\n",
    "1 { b(X,Y) : n(X), n(Y) } 1.\n",
    "ok(X) :- 2 #count{ Y,first : a(X,Y);   Z,second : b(X,Z) }, n(X).\n",
    ":- not ok(1), not ok(2).\n",
    "#show a/2. #show b/2. #show ok/1."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.1"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}