{
  "cells": [
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "%matplotlib inline"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "\n# Half-SAT problem\n\n\nThe Half-SAT problem can be defined as:\n\n\\begin{align}\\text{HALF-SAT} = \\{ \\varphi \\mid \\varphi \\text{ is a formula which is satisfied by half of all assignments }\\}\\end{align}\n\nOr, in other words, considering a CNF formula with $2n$ variables, an there's a satisfying assignment in which $n$ variables are ``True`` and $n$ variables are ``False``.\nThe Half-SAT problem is known to be `NP-Hard <https://en.wikipedia.org/wiki/NP-hardness>`_, so it cannot be solved in polynomial time.\nIn these situations the Particle Swarm Algorithm can sometimes reach optimal results in an feasible amount of time\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "import random\nfrom psopt import Combination\n\n\ndef generate_cnf(n_vars, clauses, k=3, seed=None):\n    \"\"\"\n    This function generates a random CNF formula for the Half-SAT problem\n\n    Args:\n        n_vars (int): the number of variables in the formula\n\n        clauses (int): the number of clauses that compose the formula\n\n        k (int, optional): the number of variables in each clause. Defaults to 3\n\n        seed (int, optional): Seed the function generator\n\n    Returns:\n        cnf (callable): a function in CNF for the Half-SAT problem\n    \"\"\"\n    # seed value for testing purposes\n    random.seed(seed)\n    # start expression\n    cnf = str()\n    # iterate clauses\n    for _ in range(clauses):\n        clause = str()\n        # get variables\n        variables = random.sample(list(range(n_vars)), n_vars)[:k]\n        # build clause\n        clause += random.choice([\"\", \"not \"]) + \"x[{}]\".format(variables.pop(0))\n        while len(variables) > 0:\n            clause += \" or {}x[{}]\".format(\n                random.choice([\"\", \"not \"]), variables.pop(0)\n            )\n        cnf += \"({}) and \".format(clause)\n    # quick-fix for pattern that does not affect the result\n    cnf += str(1)\n    return lambda x: eval(cnf), cnf\n\n\ndef main():\n    # define objective function: SAT in CNF\n    n_var = 30\n    fn, desc = generate_cnf(n_var, 20, seed=0)\n\n    def obj_func(x):\n        return fn([1 if i in x else 0 for i in range(n_var)])\n\n    # instantiate the optimizer\n    opt = Combination(obj_func, list(range(n_var)), metrics=\"hamming\")\n\n    # define a threshold of acceptance\n    threshold = 1\n\n    # Uncomment line below to display the objective function\n    # print(\"Objective function: \\n{}\".format(desc)\n\n    # maximize HALF-SAT\n    # (half of the number of variables are one and the rest is zero)\n    opt.maximize(selection_size=n_var // 2, verbose=1, threshold=threshold, seed=0)\n\n\nif __name__ == \"__main__\":\n    main()"
      ]
    }
  ],
  "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.7.3"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 0
}