{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Assignment 3\n", "\n", "### Solving the MAXSAT problem with local search algorithms\n", "\n" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Let's start with a few definitions: \n", "\n", "Our focus in this assignment is on **Boolean formulas**.\n", "A Boolean formula is constructed\n", "using **variables** that take on the values `True` or\n", "`False` and the operators AND (conjunction, denoted by\n", "$\\wedge$), OR (disjunction, denoted by $\\vee$), and negation (denoted\n", "by $\\neg$). \n", "\n", "We need a few more definitions:\n", "* A **literal** is either a variable (a positive literal), or the\n", "negation of a variable (a negative literal). \n", "* A **clause** is a disjunction of literals or a single literal.\n", "* A formula is in **conjunctive normal form** (CNF) if it is a conjunction of clauses or a single clause.\n", "\n", "For example, the formula $(x_1 \\vee x_3) \\wedge (x_2 \\vee \\neg x_3\n", "\\vee x_4) \\wedge (\\neg x_1 \\vee x_2 \\vee \\neg x_4)$ is in CNF.\n", "The formulas we will use in this assignment all have 3 literals per\n", "clause.\n", "\n", "The **satisfiability problem (SAT)** is the problem of finding whether there is\n", "an assignment of truth values to the variables which satisfies a\n", "formula in CNF, i.e. makes the formula evaluate to True.\n", "This problem is known to be NP-complete.\n", "We'll consider a more general variant of the problem, which is [MAXSAT](https://en.wikipedia.org/wiki/Maximum_satisfiability_problem): given a formula in CNF, find an\n", "assignment that maximizes the number of satisfied clauses (a clause is\n", "satisfied if there is an assignment of truth values for which it\n", "evaluates to True).\n", "This problem is also NP-complete.\n" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "We will encode the instance of `MAXSAT` in a file format \n", "described below (see also the [2016 SAT competition webpage](http://maxsat.ia.udl.cat/requirements/)).\n", "Here is a ([link](https://www.cs.colostate.edu/~cs440/fall19/assignments/maxsat.tgz)) to a set of 20 instances of MAXSAT that you are asked to use in this assignment.\n", "\n", "The MAXSAT instances have a format demonstrated by the following example:\n", "\n", "```\n", "c\n", "c start with comments\n", "c\n", "c \n", "p cnf 5 3\n", "1 -5 4 0\n", "-1 5 3 0\n", "-3 -4 2 0\n", "```\n", "\n", "* The file will start with comments, that is lines begining with the character c.\n", "* Right after the comments, there is the line `p cnf nbvar nbclauses` indicating that the instance is in CNF format; `nbvar` is the number of variables appearing in the file; `nbclauses` is the number of clauses contained in the file.\n", "* Then the clauses follow. Each clause is a sequence of distinct non-null numbers between `-nbvar` and `nbvar` ending with a 0 (the 0 does not refer to any variable); it cannot contain the opposite literals i and -i simultaneously. A positive number denotes the corresponding variable. A negative number denotes the negation of the corresponding variable.\n", "\n", "With that in mind, the above instance of MAXSAT describes the following formula:\n", "\n", "$(x_1 \\vee \\neg x_5 \\vee x_4) \\wedge (\\neg x_1 \\vee x_5\n", "\\vee x_3) \\wedge (\\neg x_3 \\vee \\neg x_4 \\vee x_2)$ \n", "\n", "For this formula, there is an assignment of truth values that satisfies all the clauses, so the MAXSAT value for this instance of the problem is 3.\n", "\n", "Your task is to solve the MAXSAT problem with local search strategies.\n", "To do that, write a class called `MAXSAT` which is a sub-class\n", "of `search.Problem`. \n", "The constructor of your `MAXSAT` class should receive a\n", "file name as a parameter and have other methods needed for hill climbing and other methods to work." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "```python\n", "import search\n", "class MAXSAT (search.Problem):\n", " def __init__(self, file_name):\n", " \"\"\"Construct an instance of MAXSAT by parsing an instance\n", " of MAXSAT represented in the given file\n", " \"\"\"\n", " pass\n", " ## more methods here.\n", "```" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Evaluating solution strategies for MAXSAT\n", "\n", "Your task is to compare the following solution strategies for the MAXSAT problem:\n", "\n", "* Hill climbing.\n", "* Hill climbing with random restarts (use 20 restarts).\n", "* Genetic algorithms.\n", "* Simulated annealing.\n", "\n", "Use the same method for choosing the initial state and neighborhood of\n", "a state for all strategies (for GAs you will need crossover and\n", "mutation operators in addition).\n", "To compare the search strategies run each of these solvers on the provided instances of MAXSAT and compute the average value of the solutions and their running time.\n", "Describe in detail your choice of initial state and neighborhood and\n", "the details of your GA crossover and mutation operators.\n", "Compute the average quality of the solution and the running time for each strategy, treating instances of 50 variables and 150 variables separately.\n", "Explain the difference you observe in performance (how good is the state returned by the algorithm, and how long did\n", "each strategy take to run).\n", "From your experiments, can you tell if the MAXSAT problem has local maxima?\n", "Results should be provided in easy to read tables." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "In designing your code, consult the examples shown in class on how to solve problems such as Eight Queens and TSP. You may use the implementations provided in `search.py`.\n", "\n", "For timing python code you can go as simple as:\n", "\n", "```Python\n", "import time\n", "t0 = time.time()\n", "code_block\n", "total = time.time() - t0\n", "```\n", "\n", "Your solution should appear in the following cells:" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "*Describe your approach to formulating the MAXSAT problem, how each of the methods will be used to address it. Your description should include the specification of the cost function, state, neighborhood, and mutation/crossover operators for the GA*." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "# your code here\n", "\n", "import search\n", "class MAXSAT (search.Problem):\n", " def __init__(self, file_name):\n", " \"\"\"Construct an instance of MAXSAT by parsing an instance\n", " of MAXSAT represented in the given file\n", " \"\"\"\n", " pass" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "*Show your results and discuss them here.*" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Submission\n", "\n", "Answer the questions in the cells reserved for that purpose.\n", "Submit your report as a Jupyter notebook via Canvas. Running the notebook should generate all the results in your notebook. Leave the output of your notebook intact so we don't have to run it to see the results.\n", "\n", "## Grading\n", "\n", "Grading Rubric:\n", "\n", "```\n", "25 pts: Formulation of the MAXSAT problem\n", "50 pts: Correctness of your code for solving the MAXSAT problem\n", "25 pts: Discussion of the results\n", "```\n", "\n", "Grading will be based on the following criteria:\n", "* Correct behavior of the required code\n", "* Overall readability and organization of the notebook\n", "* Effort in making interesting observations where requested.\n", "* Conciseness. Points may be taken off if the notebook is overly long." ] } ], "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.5.5" } }, "nbformat": 4, "nbformat_minor": 2 }