Universal Quantification Demo.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's introduce some new syntax to support modeling with universal quantification (toward expressing problems outside of $NP$). We'll use the a `#theory` declaration to introduce new `&exists` and `&phi` directives. Then we'll provide these directives with semantics by extending the metainterpreter provided with Clingo-5.\n",
    "\n",
    "The new directives will ensure that the `&phi` condition(s) are a necessary *positive* consequence of the configuration of `&exists` condition(s). That is to say, the truth of the `&phi` condition(s) are universally quantified over all conditions not mentioned in the `&exists` directive. If multiple `&phi` conditions are provided (either in one directive with an aggregate or multiple directives), their conjunction is considered. Likewise, the existential conditions are gathered across all `&exists` directives. In either directive, the term appearing before the colon is ignored. The directive `&phi{foo:bar}` will ensure that `bar` is unavoidable.\n",
    "\n",
    "The new directives here have the same semantics as `__level_design(A)` and `__concept` from https://adamsmith.as/papers/fdg2013_shortcuts.pdf (while being more general and compatible with Clingo-5). \n",
    "\n",
    "In the example below, we use a scenario derived from the original puzzle design context. The goal is to generate a puzzle such that the player cannot solve it without practicing some key concept. That is, concept practice should be an unavoidable consequence of solving in any deisgn that are considered valid. Usually, the connection between concept practice and puzzle design is very subtle. Here, we'll simply state that `practice` is present in any `solved` situation tagged with the `valid` property."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting prog.lp\n"
     ]
    }
   ],
   "source": [
    "%%file prog.lp\n",
    "\n",
    "#theory universal_quantification {\n",
    "    &exists/0 : term, directive;\n",
    "    &phi/0 : term, directive;\n",
    "    term {}\n",
    "}.\n",
    "\n",
    "{valid}.    % the designer created a valid puzzle (shortcut-free)\n",
    "{styled}.   % the designer made it look pretty (optional)\n",
    "{solved}.   % the player solved the puzzle\n",
    "{alt}.      % the player used an unanticipated alternate strategy\n",
    "{practice}. % the player practiced the key concept \n",
    "\n",
    ":- not solved.             % only considering solvable scenarios\n",
    "\n",
    "practice :- valid, solved. % the definition of a valid puzzle\n",
    "\n",
    "\n",
    "&exists { level_design_rigor: valid }.\n",
    "&exists { level_design_style: styled }.\n",
    "&phi { key_concept: practice }."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting metaUQ.lp\n"
     ]
    }
   ],
   "source": [
    "%%file metaUQ.lp\n",
    "\n",
    "exists(B) :-\n",
    "    theory_string(S,\"exists\"),\n",
    "    theory_atom(0,S,T),\n",
    "    theory_element_tuple(T,E),\n",
    "    theory_element(E,_,B).\n",
    "\n",
    "phi(B) :-\n",
    "    theory_string(S,\"phi\"),\n",
    "    theory_atom(0,S,T),\n",
    "    theory_element_tuple(T,E),\n",
    "    theory_element(E,_,B).\n",
    "\n",
    ":- phi(B), not conjunction(B).\n",
    "    \n",
    "bot :- exists(B), true(normal(B)), not conjunction(B).\n",
    "bot :- exists(B), fail(normal(B)), conjunction(B).\n",
    "bot :- true(normal(B)):phi(B).\n",
    "\n",
    ":- not bot.\n",
    "    \n",
    "#project conjunction(B):exists(B)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We recycle `meta.lp` and `metaD.lp` from https://github.com/potassco/clingo/tree/master/examples/reify. (The `metaO.lp` file provided is not used here, and I have not tested the case where the original program includes an optimization directive.)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "clingo version 5.2.0\r\n",
      "Reading from - ...\r\n",
      "Solving...\r\n",
      "Answer: 1\r\n",
      "practice solved styled valid\r\n",
      "Answer: 2\r\n",
      "practice solved alt styled valid\r\n",
      "Answer: 3\r\n",
      "practice solved valid\r\n",
      "Answer: 4\r\n",
      "practice solved alt valid\r\n",
      "SATISFIABLE\r\n",
      "\r\n",
      "Models       : 4\r\n",
      "Calls        : 1\r\n",
      "Time         : 0.015s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)\r\n",
      "CPU Time     : 0.015s\r\n"
     ]
    }
   ],
   "source": [
    "!clingo prog.lp --output=reify | clingo - meta.lp metaD.lp metaUQ.lp 0 -W no-atom-undefined"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As expected, there are four solvable designs (each involves `solved`). In each design\n",
    ", the puzzle is `valid`, but the `styled` property of the design and `alt` property of the solution to the puzzle can be varied independently.\n",
    "\n",
    "If we use projected enumeration to represent each puzzle design once (where a puzzle design is captured by the `&exists` conditions), we see only two. The puzzle may be `styled` or not, but variations in the player choices don't count as extra models:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "clingo version 5.2.0\r\n",
      "Reading from - ...\r\n",
      "Solving...\r\n",
      "Answer: 1\r\n",
      "practice solved styled valid\r\n",
      "Answer: 2\r\n",
      "practice solved valid\r\n",
      "SATISFIABLE\r\n",
      "\r\n",
      "Models       : 2\r\n",
      "Calls        : 1\r\n",
      "Time         : 0.015s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)\r\n",
      "CPU Time     : 0.015s\r\n"
     ]
    }
   ],
   "source": [
    "!clingo prog.lp --output=reify | clingo - meta.lp metaD.lp metaUQ.lp 0 -W no-atom-undefined --project"
   ]
  }
 ],
 "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.6.1"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}