Let's start with a few definitions:
Our focus in this assignment is on Boolean formulas.
A Boolean formula is constructed
using variables that take on the values True
or
False
and the operators AND (conjunction, denoted by
$\wedge$), OR (disjunction, denoted by $\vee$), and negation (denoted
by $\neg$).
We need a few more definitions:
negation of a variable (a negative literal).
For example, the formula $(x_1 \vee x_3) \wedge (x_2 \vee \neg x_3 \vee x_4) \wedge (\neg x_1 \vee x_2 \vee \neg x_4)$ is in CNF. The formulas we will use in this assignment all have 3 literals per clause.
The satisfiability problem (SAT) is the problem of finding whether there is an assignment of truth values to the variables which satisfies a formula in CNF, i.e. makes the formula evaluate to True. This problem is known to be NP-complete. We'll consider a more general variant of the problem, which is MAXSAT: given a formula in CNF, find an assignment that maximizes the number of satisfied clauses (a clause is satisfied if there is an assignment of truth values for which it evaluates to True). This problem is also NP-complete.
We will encode the instance of MAXSAT
in a file format
described below (see also the 2016 SAT competition webpage).
Here is a (link) to a set of 20 instances of MAXSAT that you are asked to use in this assignment.
The MAXSAT instances have a format demonstrated by the following example:
c
c start with comments
c
c
p cnf 5 3
1 -5 4 0
-1 5 3 0
-3 -4 2 0
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.-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.With that in mind, the above instance of MAXSAT describes the following formula:
$(x_1 \vee \neg x_5 \vee x_4) \wedge (\neg x_1 \vee x_5 \vee x_3) \wedge (\neg x_3 \vee \neg x_4 \vee x_2)$
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.
Your task is to solve the MAXSAT problem with local search strategies.
To do that, write a class called MAXSAT
which is a sub-class
of search.Problem
.
The constructor of your MAXSAT
class should receive a
file name as a parameter and have other methods needed for hill climbing and other methods to work.
import search
class MAXSAT (search.Problem):
def __init__(self, file_name):
"""Construct an instance of MAXSAT by parsing an instance
of MAXSAT represented in the given file
"""
pass
## more methods here.
Your task is to compare the following solution strategies for the MAXSAT problem:
Use the same method for choosing the initial state and neighborhood of a state for all strategies (for GAs you will need crossover and mutation operators in addition). 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. Describe in detail your choice of initial state and neighborhood and the details of your GA crossover and mutation operators. Compute the average quality of the solution and the running time for each strategy, treating instances of 50 variables and 150 variables separately. Explain the difference you observe in performance (how good is the state returned by the algorithm, and how long did each strategy take to run). From your experiments, can you tell if the MAXSAT problem has local maxima? Results should be provided in easy to read tables.
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
.
For timing python code you can go as simple as:
import time
t0 = time.time()
code_block
total = time.time() - t0
Your solution should appear in the following cells:
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.
# your code here
import search
class MAXSAT (search.Problem):
def __init__(self, file_name):
"""Construct an instance of MAXSAT by parsing an instance
of MAXSAT represented in the given file
"""
pass
Show your results and discuss them here.
Answer the questions in the cells reserved for that purpose. 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.
Grading Rubric:
25 pts: Formulation of the MAXSAT problem
50 pts: Correctness of your code for solving the MAXSAT problem
25 pts: Discussion of the results
Grading will be based on the following criteria: