# 2
#
import numpy, numpy.random, pylab, random
#
# Graphics for animating solution process
import DynamicNetwork
import imp
imp.reload(DynamicNetwork)
#
# Use to control whether you animate your solution
# Set to False if you want to run quickly
GRAPHICS = True
#
# We first generate some "real-world" logical satisfiability problems
# that emerge from graph coloring. This is mostly to give a feeling for
# what SAT problems are, and to give a couple of examples where we
# know the answer, to be used to debug our algorithms.
#
def MakeSATFrom3Colorability(colorGraphDict):
"""Transform a 3-colorability problem into a SAT exercise.
Assume that the graph to be colored is a dictionary, with
keys labeling the nodes of the graph, and lists of neighbors
as edges for each node. We assume an undirected graph, so if
A has B in its list of neighbors, so B has A in its list.
Assume colorGraphDict gives the neighbors of each edge:
['A'] = ['B', 'C', 'D']
Given an N-node graph, make up a 3N-variable SAT problem
where node A has three logical variables A_red, A_green, and A_blue.
#
Let's do this systematically.
(1) Define three dictionaries red, green, and blue, by iterating
over the nodes ("for node in colorGraphDict");
for the nth node [counting from zero] red=3*n+1, green=3*n+2,
and blue=3*n+3. (We'll use the negatives of these variables to denote
the logical statement that the node is not colored that color:
not-red = -(3*n+1), etc.)
Each clause is a list of at most three integers (minus for "not"), so
[6, -7, 3] says "node 2 is blue or node 3 is not red or node 1 is blue".
Of course, that example will not show up in a classic 3-coloring problem
-- examples of more typical clauses are:
[1, 2, 3] -- "node 1 is red or blue or green"
[-1, -4] -- "either node 1 is not red or node 2 is not red" whcih is easier
to understand as "node 1 and node 2 are not both red"
[-1,-2] -- "node 1 is not both red and blue"
(2) Then generate the clauses, appending to an empty list
For each node,
Append a clause saying that the node is colored at least one color
Append three clauses saying that the node is not colored two colors
For each edge (say between A and B), if B>A (to avoid double counting)
append three clauses saying that
A and B are not colored the same color
(3) Return the clauses
"""
pass
#
def MakeMapsFromProblemSet():
"""Generate, by hand, the two maps in the Graph Coloring figure
in the Satisfactory Map Coloring exercise, as dictionaries:
leftGraph={}
leftGraph['A']=['B','C','D'],
...
return leftGraph, rightGraph
"""
pass
#
# We also want to generate random kSAT problems
#
def MakeRandom_kSATClauses(nVars, nClauses, k=3):
"""
MakeRandom_kSATClauses(nVars, nClauses, k) generates a random k-SAT
instance with nvariables and nClauses.
We recommend using numpy.random.randint, making an array of shape
(nClauses,k) of integers in the range [1,nVars], and multiplying it
by an array filled with +-1 (found by making an array of 0's and 1's,
doubling it and subtracting one).
Our clauses are lists and not arrays (because lists can have variable
numbers of entries, mixing 2SAT and 3SAT, for example), so convert
the result to a list using clauses.tolist(), where clauses is the
name of your clause array. [array.tolist() is a method to convert
a numpy array to a Python list]
"""
pass
#
# -------------------------------------------------------------------
#
class DPSATSolverBase:
"""
SATSolverBase implements a Davis-Putnam algorithm for finding solutions
to logical satisfiability problems stated in conjuctive normal form.
#
This is a "base class", or virtual class: it does not implement
one key method (TrySet), but awaits two different implementations
(SlowDPSATSolver and FasterDPSATSolver) in classes derived from
SATSolverBase.
"""
def __init__(self, clauseList=None):
"""
Constructs a SATSolverBase given a set of input clauses.
It needs to create and store the following data members:
#
self.clauseList: the list of input clauses, each one consisting of
a list of variables and negations of variables (stored as a list
of signed integers)
#
self.vars: a list of the variables. This internal list will be
used also to determine the order in which the variables are
tried (given tentative values). Shuffling or reordering this
list will be an important diagnostic and optimization tool.
Until we start the fancy methods, be sure to sort this list
(self.vars.sort()) after it is assembled from the
clauses, so that your algorithm will set variables in the same
order as the graphics program lays them out.
#
self.varStatus: a dictionary mapping variables to boolean
values True or False, or None if variable is (so far) unset
#
self.nodeClauses: a dictionary mapping a variable
to the indices of the clauses including that variable and maps
its negation to those for clauses including the negation of that
variable. Specifically, if clauseList[i]=[n,-m,p] then
nodeClauses[n]=[..., i, ...] contains i, as should nodeClauses[-m]
and nodeClauses[p].
#
self.clauseStatus: a dictionary identifying
whether the clause is not determined (None), or if it is True
give the current state of the variables. (If a clause
is False, for this algorithm, we immediately backtrack.)
#
if GRAPHICS is set to True, create
self.dynnet: an instance of a DynamicNetwork graphics window
for animating solver progress
(self.dynnet = DynamicNetwork.DynamicNetwork())
"""
self.clauseList = clauseList
pass
def SelectNextVariableToTry(self):
"""Gives next variable (index entry into list vars) for DP algorithm
to try setting. Initially we explore the simple algorithm of
just setting them in order: later we'll select them in MOMS order"""
# return self.SelectNextVariableSimple()
return self.SelectNextVariableMOMS()
def SelectNextVariableSimple(self):
"""
Search through self.vars for the first unset variable
(the index for which varStatus[vars[varIndex]] is None). If all are
set (we're done!) return None; otherwise return varIndex.
"""
pass
def SelectNextVariableMOMS(self):
"""
Select one of the MOMS literals (Most Occurences in unresolved
clauses of Minimial Size) at random. Also, if there are no
unresolved clauses, return None to signal that a SAT solution
has been found.
"Size" refers to the number of unset variables in the clause.
Usually the minimal size will be two. (`Length one' literals will
be reduced by FasterDPSATSolver.TrySet).
(1) Assemble a list MSVars of the unset variables in unresolved clauses
of minimal size:
Set k=1; # the Fast solver can start at k=2, but the Slow one
# needs to start at k=1
while no unresolved clauses of length k exist:
Loop over clauses,
if the clause is not True (resolved)
build a list of unset variables in the clause
if that list has k variables,
note that length k clauses exist
extend the list of MSVars
If no unresolved clauses exist, return None
Increment k
(2) Find the number of times each variable is contained in MSVars,
and the maximum number
(3) Collect the list of MOMS variables represented most often
(4) Use random.choice to return random choice among MOMS variables
"""
pass
def Solve(self):
"""Solve() returns True if the clauses are satisfiable (SAT)
and False if UNSAT, along with the number of tries required
to find a solution. Solve() also leaves "self" in a solved
state if it found one.
#
Solve works by
(0) initializing numTries = 0
(1) selecting a literal litNext to try setting next. If all
variables are set, declare victory: return True and numTries(=0)
(2) loop over literal in [litNext, -litNext]
calling TrySet on that literal, incrementing numTries
If TrySet returns True, Solve recursively calls itself,
and supplements numTries.
If this recursive call returns true, Solve declares
victory and returns True and numTries
Otherwise, unwind: set the status of the variables in varsSet
and clauses in clausesSet to None
(3) return False, numTries
Also, if GRAPHICS==True, call Display() after each call to
TrySet or Solve.
"""
pass
def TrySet(self, literal):
"""Tries to set one literal to True, with various ramifications
setting other variables depending on implementation. Returns
status (True or False), a list varsSet of variables that have been
set, and a list clausesSetTrue of clauses that have been newly set
to True.
#
TrySet is undefined in the base class: SlowDPSATSolver and
FasterDPSATSolver will implement it as subclasses of SATSolverBase.
"""
pass
def Display(self):
"""Display() displays the current status of the DPSATSolver by
calling self.dynnet.displayFromLists with the following data:
#
nodelist: the list of variables
edgelist: the list of edges between variables which occur in
clauses that have not been satisfied
nodecolors: a dictionary mapping (positive) variable ids to colors
clear = True: otherwise it won't redraw when edges are removed
"""
self.dynnet.displayFromLists(self.vars, self.GetUnresolvedEdges(),
self.GetNodeColors(), clear=True)
def GetUnresolvedEdges(self):
"""GetUnresolvedEdges() (used in Display) returns a list of all
pairs of variables that are unset, and are involved in a clause
which is not yet resolved;
start with an empty list of unresolved edges,
for each clauseIndex, clause in enumerate(clauseList)
if the clause status is not set
for each literal in the clause
if the variable is unset
for each second literal in the clause
if the second variable is > first variable and is unset
append to unresolved"""
pass
def GetNodeColors(self):
"""GetNodeColors() returns a dictionary of colors for Display:
green (0,255,0) if variable is True, red (255,0,0)
if False, and white (255,255,255) if unset"""
pass
"""You'll want to implement and test SlowDPSATSolver and Display
on your colorability problems and some kSAT examples at this point, and
then PlotSATFrac. Probably then you'll be motivated to improve on your
algorithm using FasterDPSATSolver. At that point, you'll want to
start implementing these further class member functions."""
def ShuffleVariableOrder(self):
"""ShuffleVariableOrder() resets and then
randomly shuffles the var_order list,
using the random.shuffle method: used for diagnosis on
FasterDPSATSolver"""
pass
def Reset(self):
"""Reset() sets each variable value to None and each element of
clause_true to None. Used especially when repeated runs are needed,
as in using ShuffleVariableOrder."""
pass
def SetVariableOrderFromFrequency(self):
"""SetVariableOrderFromFrequency() sorts the vars list
by the frequency with which each variable (or its negation)
occurs in the clauses, in order of decreasing frequency"""
pass
def Verify(self):
"""
Verify() returns True if the current settings of the variables
satisfy all the SAT clauses; otherwise returns False. Used especially
in debugging.
"""
pass
#
class SlowDPSATSolver (DPSATSolverBase):
def TrySet(self, literal):
"""Try setting one literal true.
(1) Sets self.varStatus[var] to True or False,
where var = abs(literal) and the sign of the literal is
positive for True and negative for False.
Set varsSet=[var] and initialize clausesSet to [].
(2) Then tests each clause involving -literal:
if it is not already set True,
if all of its literals have variables that are set,
(so the clause must be False)
return False, varsSet=[var], and clausesSet = []
(3) Then, for each clause involving the literal, if the clause
is unset, add the clause index to clausesSet and set the
clause status to True.
Return True, varsSet, and clausesSet"""
pass
#
class FasterDPSATSolver (DPSATSolverBase):
def TrySet(self, literal):
"""Improves on SlowDPSATSolver, by looking for a `length one'
clause where all but one literal is set wrong, and using
TrySet recursively to set that last literal true.
"""
pass
#
# -------------------------------------------------------------------
#
# Various SAT analyses and tests
#
# -------------------------------------------------------------------
#
def SATFrac(nVars, nClauses, nRuns, k=3, Solver=FasterDPSATSolver):
"""SATFrac(nVars, nClauses, nRuns, k=3, Solver=FasterDPSATSolver)
calculates the fraction satisfiable and the times taken for
nRuns of a kSAT problem with nVars and nClauses, using the solver algorithm.
Returns mean and standard deviation for SATFrac and time, and the list
of times.
#
It sets GRAPHICS to False (after declaring it global).
It sets up variables 'SATTot' to store the total numer of satisfiable
problems, 'times' a list to store the number of tries taken by the
algorithm, 'timeTot' for the total time, and 'time2Tot' for the
total squared time. [Remember that the variance
var=(t2Tot-tTot^2/N)/(N-1) and thus the standard deviation of
the mean sig=sqrt(var/N)].
It then loops over nRuns
makes clauses
instantiates solver
finds SAT, time for solution
(option, verify solution: useful for debugging new solvers)
increments SATTot, timeTot, time2Tot, and appends to times
finds SATFrac and timeAv
if nRuns==1 returns them
finds variance, sigma for the mean for SAT, time
(note SAT2Tot = SATTot: why?)
returns SATFrac, SATFracSigmaMean, timeAv, timeSigmaMean
"""
pass
#
def PlotSATFrac(nVars, nRuns, k=3,
ClausesOverVars=numpy.arange(0.5, 8.0, 0.5),
Solver=FasterDPSATSolver):
"""
PlotSATFrac(nVars, nRuns, k=3, ClausesOverVars=arange(0.5, 8.0, 0.5),
Solver=FasterDPSATSolver)
collects data from SATFrac for a variety of nClauses, and
makes three plots versus the ratio clauses/variables: one with the mean
and standard deviation of SATFrac, one of mean and sigma for times,
and one of the distribution of times found at that ratio.
Use pylab.errorbar to draw the first two plots, and assemble two long
lists of ratios and times for the last plot. Use pylab.figure(n) to
switch to plot #n.
"""
pass
#
def TimeTails(SATInstance, nRuns=10, showPlot=True):
"""TimeTails(SATInstance, nRuns=10, showPlot=True)
computes and returns the times for nRuns runs of a SAT instance
shuffling the order of the variable list vars (and hence the order
in which they are attempted by the DP algorithm) and resetting the
instance in between. GRAPHICS is turned off.
Optionally, a pylab.hist plot of the histogram can be generated and shown.
See pylab.hist and pylab.histogram
"""
pass
#
def NTimeTails(nInst, nRuns, nVars=10, nClauses=40, k=3, plot=True,
Solver=FasterDPSATSolver):
"""NTimeTails(nInst, nRuns, nVars, nClauses, plot=True,
Solver=FasterDPSATSolver) computes the runtimes for nRuns runs each
of nInst SAT instances (k-SAT with nVars variables and nClauses clauses),
returning a list of the runtime (number of flips) of each run. Optionally,
a pylab plot of the histogram can be generated and shown.
see pylab.hist and pylab.histogram
"""
pass
#
def LogLogHist(seq, nBins=10):
"""LogLogHist(seq, nBins=10) makes a log-log histogram (with nBins bins)
of a sequence of numbers contained in seq. Bin widths are sized
exponentially (i.e., uniformly in logs) and bin counts are normalized
by bin width."""
pass
#
def TimeSlowFast(nInst, nRuns, nVars, nClauses):
"""TimeSlowFast(nInst, nRuns, nVars, nClauses) compares the runtimes
of the Slow and Faster DPSATSolvers.
"""
pass
#
def TestSAT(nVars, nClauses, k, with_graphics = True,
Solver=FasterDPSATSolver):
"""
TestSAT(nVars, nClauses, k, with_graphics=True,
Solver=FasterDPSATSolver) generates a single instance of k-SAT
with nVars variables and nClauses clauses, and solves it using the
specified solver class. If with_graphics is True, then a graphics
window showing progress of the algorithm is shown. The status of
the solution (i.e., True=SAT or False=UNSAT), along with the number
of variable flips, is returned.
"""
pass
#
# Copyright (C) Cornell University
# All rights reserved.
# Apache License, Version 2.0