sat_preprocessing

sat_preprocessing.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "#\n",
    "# For this problem, we would like you to implement pre-processing\n",
    "# rules for SAT. We're going to use the same format as in the problem\n",
    "# set for Unit 2 to represent Boolean Formulas (in conjunctive normal\n",
    "# form):\n",
    "#\n",
    "# The number of variables will be given as an integer num_variables\n",
    "# (all variables are consecutively numbered from 1 to (num_variables)\n",
    "#\n",
    "# The clauses will be represented as a list of lists called\n",
    "# \"clauses\". The \"outer list\" contains all clauses, each inner list is\n",
    "# a clause. The variable x_i is represented as i if it appears without\n",
    "# a not, otherwise it is represented as -i\n",
    "#\n",
    "# For example, the Boolean Formula (x1 or x2 or not(x3)) and (x2 or\n",
    "# not(x4)) and (not(x1) or x3 or x4) would translate into\n",
    "#\n",
    "# num_variables = 4\n",
    "#\n",
    "# clauses = [[1,2,-3],[2,-4],[-1,3,4]]\n",
    "#\n",
    "# For this exercise, please write a function that, when given a\n",
    "# Boolean Formula in the above format, performs the following data\n",
    "# reduction rules and outputs the resulting set of clauses:\n",
    "#\n",
    "# 1) If any clause consists of a single variable, set the variable so\n",
    "# that this clause is satisfied\n",
    "#\n",
    "# 2) If a variable appears just once (and it hasn't been set, see\n",
    "# below), set it so that the respective clause is satisfied\n",
    "#\n",
    "# 3) Remove all clauses that have become satisfied\n",
    "#\n",
    "# 4) Remove all variables that evaluate to 'FALSE' (i.e., all variables x\n",
    "# that are set to FALSE and all variables not(x) where x is set to TRUE).\n",
    "# If this results in an empty clause, then the input formula has no satisfying\n",
    "# assignment and the function should return the Boolean formula [[1,-1]]\n",
    "#\n",
    "# The challenging part is implementing Rule 2, for your function must\n",
    "# perform the data reductions exhaustively, that is, until they can no\n",
    "# further be applied: After rules 2, 3 and 4 have been applied, there\n",
    "# might be other clauses for which rule 2 now becomes applicable (you\n",
    "# will have to be careful if a variable that now appears once has\n",
    "# already been set earlier - if not, then Rule 2 may apply, otherwise\n",
    "# it doesn't).\n",
    "#\n",
    "# Remember that pre-processing cannot change the satisfiablity. If\n",
    "# a SAT problem is satisfiable, the output of the pre-processing also\n",
    "# needs to be satisfiable.\n",
    "#\n",
    "# If through the pre-processing steps you are able to determine that a\n",
    "# SAT problem is satisfiable then return []. Likewise, if you\n",
    "# determine that it is unsatisfiable then return [[1,-1]]. Otherwise,\n",
    "# return the remaining clauses.\n",
    "\n",
    "def sat_preprocessing(num_variables, clauses):\n",
    "    # YOUR CODE HERE\n",
    "\n",
    "\n",
    "def test():\n",
    "    assert [] == sat_preprocessing(1, [[1]])\n",
    "    assert [[1,-1]] == sat_preprocessing(1, [[1], [-1]])\n",
    "    assert [] == sat_preprocessing(4, [[4], [-3, -1], [3, -4, 2, 1], [1, -3, 4],\n",
    "                                         [-1, -3, -4, 2], [4, 3, 1, 2], [4, 3],\n",
    "                                         [1, 3, -4], [3, -4, 1], [-1]])\n",
    "    assert [[1,-1]] == sat_preprocessing(5, [[4, -2], [-1, -2], [1], [-4],\n",
    "                                         [5, 1, 4, -2, 3], [-1, 2, 3, 5],\n",
    "                                         [-3, -1], [-4], [4, -1, 2]])\n",
    "    ans = [[5, 6, 2, 4], [3, 5, 2, 4], [-5, 2, 3], [-3, 2, -5, 6, -4]]\n",
    "    assert ans == sat_preprocessing(6, [[-5, 3, 2, 6, 1], [5, 6, 2, 4],\n",
    "                                        [3, 5, 2, -1, 4], [1], [2, 1, 4, 3, 6],\n",
    "                                        [-1, -5, 2, 3], [-3, 2, -5, 6, -4]])"
   ]
  }
 ],
 "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.4.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}