{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### SAT Solving to Software Verification: Part 1"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this post, we'll look at how to teach computers to solve puzzles. Specifically, we'll look at a simple puzzle that can be expressed as a boolean constraint satisfaction problem, and we'll write a simple constraint solver (a SAT solver) and mention how our algorithm, when augmented with a few optimizations, is used in modern SAT solvers. The only requisite knowledge is a basic understanding of algorithms and the ability to read Haskell code.\n",
"\n",
"In future posts, we'll extend our puzzle solving abilities beyond boolean constratint satisfaction by writing an SMT solver; after that, we'll look at how these puzzle solving algorithms can be used for software verification.\n",
"\n",
"This is an exported [IHaskell](http://www.github.com/gibiansky/IHaskell) notebook, and you can download the [original](/blog/verification/writing-a-sat-solver/data/Writing-a-SAT-Solver.ipynb) to play around with the code."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Boolean Constraint Satisfaction\n",
"\n",
"Let's start by jumping in with an example of a constraint satisfaction problem. Suppose that you need to go grocery shopping, and need to visit three stores: Costco, Home Depot, and Walmart. Costco is open in the morning and evening, Home Depot is open in the evening only, and Walmart is open in the morning only. You can only be in one place at a time, and shopping at a given store takes up the entire morning or evening. Can you go to all three stores in a day?\n",
"\n",
"To a human, it is intuitively obvious that the answer is no. Since Home Depot and Walmart offer us only one time option (evening and morning, respectively), then we have to go there at those times. However, this leaves no time for a Costco trip, so it's evident that this \"puzzle\" has no solution.\n",
"\n",
"Now suppose instead of three stores, you were given three thousand (each with its own schedule), and instead of two times, you were given all the hours of a day? At this point, the problem becomes intractable for a human. Luckily, though, cruching numbers and analyzing thousands of different options are what computers excel at.\n",
"\n",
"So, how would you encode the above problem in a way that a computer could understand?\n",
"\n",
"Computers are built upon boolean algebra, operating on true and false values. Thus, a natural way to encode our problem is to try to rewrite it as an expression involving boolean variables, which can either be true or false. For example, using the example of three stores and two times, let's make six variables:\n",
"\n",
"- $C_e$: Whether we go to Costco in the evening.\n",
"- $C_m$: Whether we go to Costco in the morning.\n",
"- $H_e$: Whether we go to Home Depot in the evening.\n",
"- $H_m$: Whether we go to Home Depot in the morning.\n",
"- $W_e$: Whether we go to Walmart in the evening.\n",
"- $W_m$: Whether we go to Walmart in the morning.\n",
"\n",
"Each of these variables if true (or 1) if we visit the store at the corresponding time, and false otherwise. Next, we form some constraints on these variables, and express them in a unified form we could feed to a computer.\n",
"\n",
"First, we know that we can only be in one place at a given time. For example, if we are at Costco in the morning (that is, $C_m = 1$), then we cannot be at Home Depot or Walmart in the morning (and thus $H_m = W_m = 0$). Using $\\wedge$ for \"and\", $\\vee$ for \"or\", and $\\overline{A}$ to indicate \"not $A$\", we can express that constraint as $C_m \\wedge \\overline{H_m} \\wedge \\overline{W_m}$. Note that this constraint *assumes* that $C_m = 1$; $C_m$ must be true in order to satisfy that constraint.\n",
"\n",
"Of course, we know that at a given time, we could go to Costco, Home Depot, *or* Walmart, so $C_m$ doesn't have to be true. Thus, the constraint that we only go to one place in the evening can be represented as\n",
"\n",
"$$(C_e \\wedge \\overline{H_e} \\wedge \\overline{W_e}) \\vee (\\overline{C_e} \\wedge {H_e} \\wedge \\overline{W_e}) \\vee (\\overline{C_e} \\wedge \\overline{H_e} \\wedge {W_e})$$\n",
"\n",
"Similarly, the constraint that we only go to one place in the morning is\n",
"\n",
"$$(C_m \\wedge \\overline{H_m} \\wedge \\overline{W_m}) \\vee (\\overline{C_m} \\wedge {H_m} \\wedge \\overline{W_m}) \\vee (\\overline{C_m} \\wedge \\overline{H_m} \\wedge {W_m})$$\n",
"\n",
"Next, we need a constraint that we go to Costco in either the morning or evening, which we can represent as $C_m \\vee C_e$: either we go to Costco in the morning, or in the evening. We have similar constraints for Walmart and Home Depot, yielding the following constraint to represent that we must go to each store:\n",
"\n",
"$$(C_m \\vee C_e) \\wedge (H_m \\vee H_e) \\wedge (M_m \\vee M_e)$$\n",
"\n",
"Thus, the full set of constraints for our problem is\n",
"\n",
"$$\\begin{align*}\n",
"(C_m \\vee C_e) \\wedge (H_m \\vee H_e) \\wedge (M_m \\vee M_e) &\\wedge\\\\\n",
"(C_m \\wedge \\overline{H_m} \\wedge \\overline{W_m}) \\vee (\\overline{C_m} \\wedge {H_m} \\wedge \\overline{W_m}) \\vee (\\overline{C_m} \\wedge \\overline{H_m} \\wedge {W_m}) &\\wedge\\\\\n",
"(C_e \\wedge \\overline{H_e} \\wedge \\overline{W_e}) \\vee (\\overline{C_e} \\wedge {H_e} \\wedge \\overline{W_e}) \\vee (\\overline{C_e} \\wedge \\overline{H_e} \\wedge {W_e}) &\n",
"\\end{align*}$$\n",
"\n",
"To find out whether we can complete our shopping trip, we must find a set of true or false values for all our boolean variables such that the constraints are **satisfied**. This type of problem is known as the [boolean satisfiability problem](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem), often abbreviated to just \"SAT\". A program that finds solutions to these problems is known as a SAT solver."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## SAT Solving\n",
"\n",
"Let's write a simple SAT solver in Haskell. Once we have a simple solver, we'll discuss heuristics for speeding up solving.\n",
"\n",
"Let's start by defining a data type to store our constraints:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"data Expr = Var Char\n",
" | And Expr Expr\n",
" | Or Expr Expr\n",
" | Not Expr\n",
" | Const Bool\n",
" deriving (Show, Eq)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Note the `Var Char` constructor: in this simple expression data type, we use `Char` to represent variables. We also allow for `Const` constructors to represent concrete true or false values; this is particularly useful for intermediate computations.\n",
"\n",
"The most basic algorithm for SAT solving is a backtracking search. This search has the following steps:\n",
"\n",
"1. Find a variable in the constraint expression that *hasn't* been assigned (a free variable).\n",
"2. Guess a value for this free variable.\n",
"3. Replace all occurrences of the free variable with the guessed value.\n",
"4. Simplify the expression. If the expression simplifies to true (one), then the values we've assigned work, and any variables that are unassigned do not matter. If the expression simplifies to false (zero), then undo the last assignment, and assign the opposite value.\n",
"\n",
"First, we implement step 1: finding free variables with `freeVariable :: Expr -> Maybe Char`. Since not all expressions have a free variables, we return a `Maybe` value, and we can use `<|>` from the `Alternative` typeclass to choose the first `Just` we encounter."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"import Control.Applicative ((<|>))\n",
"\n",
"-- Return the first free variable in the boolean expression.\n",
"-- If there are no free variables (it is Const), return Nothing.\n",
"freeVariable :: Expr -> Maybe Char\n",
"freeVariable (Const _) = Nothing\n",
"freeVariable (Var v) = Just v\n",
"freeVariable (Not e) = freeVariable e \n",
"freeVariable (Or x y) = freeVariable x <|> freeVariable y\n",
"freeVariable (And x y) = freeVariable x <|> freeVariable y"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Next, implement step 2: replacing free variables with a constant true or false guess value. At this point, we introduce `Const` constructors into our expression tree, replacing the appropriate `Var` constructors with them."
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"-- Guess a value for a variable. This replaces all\n",
"-- the appropriate Var constructors with a Const constructor.\n",
"guessVariable :: Char -> Bool -> Expr -> Expr\n",
"guessVariable var val e =\n",
" case e of \n",
" Var v -> if v == var\n",
" then Const val\n",
" else Var v\n",
" Not e -> Not (guess e)\n",
" Or x y -> Or (guess x) (guess y)\n",
" And x y -> And (guess x) (guess y)\n",
" Const b -> Const b\n",
" where\n",
" guess = guessVariable var val"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now that we've introduced `Const` constructors, our expression is no longer simplified. For example, we can now have expressions such as $x \\wedge 0$ or $y \\vee 1$, which should be simplified down to 0 and 1, respectively.\n",
"\n",
"Thus, we introduce `simplify`, which returns either a `Const` constructor or a simplified expression; if the result is not a `Const` constructor, it guarantees that there are no `Const` constructors in the `Expr` tree further down. (Note that we could encode this invariant in the type system! The best way to do this is left as an exercise to the reader.)"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"simplify :: Expr -> Expr\n",
"simplify (Const b) = Const b\n",
"simplify (Var v) = Var v\n",
"simplify (Not e) =\n",
" case simplify e of\n",
" Const b -> Const (not b)\n",
" e -> Not e\n",
"simplify (Or x y) =\n",
" -- Get rid of False values, which are irrelevant.\n",
" let es = filter (/= Const False) [simplify x, simplify y]\n",
" in\n",
" -- If True is in a branch, the entire expression is True.\n",
" if Const True `elem` es\n",
" then Const True\n",
" else\n",
" case es of\n",
" -- If all the values were False, this 'or' is unsatisfied.\n",
" [] -> Const False\n",
" [e] -> e\n",
" [e1, e2] -> Or e1 e2\n",
"-- Dual to the simplify (Or x y) definition.\n",
"simplify (And x y) =\n",
" let es = filter (/= Const True) [simplify x, simplify y]\n",
" in\n",
" if Const False `elem` es\n",
" then Const False\n",
" else\n",
" case es of\n",
" [] -> Const True\n",
" [e] -> e\n",
" [e1, e2] -> And e1 e2"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We now have all the building blocks of the backtracking algorithm described above. We can implement it as a depth first search, using recursion for backtracking:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"-- Extract the boolean from the Const constructor.\n",
"unConst :: Expr -> Bool\n",
"unConst (Const b) = b\n",
"unConst _ = error \"Not Const\"\n",
"\n",
"satisfiable :: Expr -> Bool\n",
"satisfiable expr =\n",
" case freeVariable expr of\n",
" Nothing -> unConst expr\n",
" Just v ->\n",
" -- We have a variable to guess.\n",
" -- Construct the two guesses.\n",
" -- Return whether either one of them works.\n",
" let trueGuess = simplify (guessVariable v True expr)\n",
" falseGuess = simplify (guessVariable v False expr)\n",
" in satisfiable trueGuess || satisfiable falseGuess"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can test this backtracking search on a few trivial examples:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"(True,False)"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"(satisfiable (Const True), satisfiable (Const False))"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"satisfiable $ And (Var 'x') (Not (Var 'x'))"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"satisfiable $ Or (Var 'x') (Not (Var 'x'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Solving Our Puzzle"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can also use this to solve our earlier puzzle. For generality, we'll write the code to solve this puzzle for any set of stores and times, but only define a small number of them:"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"-- Stores we need to go to.\n",
"data Store = Walmart | HomeDepot | Costco deriving (Show, Eq)\n",
"\n",
"-- Times the stores could be open.\n",
"data Time = Morning | Evening deriving (Show, Eq)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now that we have a data type to represent stores and times, let's encode (as a function) when each store is available. In a real application, this would be fetched from a database, or some other information source:"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"-- Times each store is open.\n",
"availability :: Store -> [Time]\n",
"availability Walmart = [Morning]\n",
"availability HomeDepot = [Evening]\n",
"availability Costco = [Morning, Evening]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Finally, create a set of constraints to satisfy. We'll first have to encode the variables ($C_m$, $C_e$, $H_m$, and so on) in our expression format, after which we can encode all our constraints:"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"-- A variable to represent visiting a store at a time.\n",
"variable :: Store -> Time -> Expr\n",
"variable Walmart Morning = Var 'a'\n",
"variable Walmart Evening = Var 'b'\n",
"variable HomeDepot Morning = Var 'c'\n",
"variable HomeDepot Evening = Var 'd'\n",
"variable Costco Morning = Var 'e'\n",
"variable Costco Evening = Var 'f'\n",
"\n",
"-- Create a constraint requiring us to visit a given store\n",
"-- on *one* of the provided times. In our puzzle, the provided\n",
"-- times are all the available ones.\n",
"visitConstraint :: [Time] -> Store -> Expr\n",
"visitConstraint times store =\n",
" foldl1 Or $ map (variable store) times\n",
"\n",
"-- A constraint requiring us to visit all the stores.\n",
"visitAllConstraint :: [Store] -> [Time] -> Expr\n",
"visitAllConstraint stores times =\n",
" foldl1 And $ map (visitConstraint times) stores\n",
"\n",
"-- mapMaybe :: (a -> Maybe b) -> [a] -> [b]\n",
"-- Apply a function and keep all the Just results.\n",
"import Data.Maybe (mapMaybe)\n",
"\n",
"-- Generate a constraint enforcing the fact that\n",
"-- we only visit stores when they are available.\n",
"storeConstraint :: [Time] -> Store -> Expr\n",
"storeConstraint allTimes store =\n",
" case mapMaybe timeConstraint allTimes of\n",
" [] -> Const True -- We can go to this store any time.\n",
" cs -> foldl1 And cs\n",
" where\n",
" -- Return Nothing is we can visit the store\n",
" -- at the time. Otherwise return a constraint\n",
" -- that must be satisfied which ensures that the\n",
" -- store is not visited at this time.\n",
" timeConstraint :: Time -> Maybe Expr\n",
" timeConstraint time\n",
" | time `elem` availability store = Nothing\n",
" | otherwise = Just (Not (variable store time))\n",
" \n",
"-- (\\\\) is set difference on lists.\n",
"import Data.List ((\\\\))\n",
"\n",
"-- Constraints for each time, indicating that we cannot\n",
"-- be in multiple places during one time.\n",
"timeConstraint :: [Store] -> Time -> Expr\n",
"timeConstraint allStores time =\n",
" foldl1 Or $ map chooseStore allStores\n",
" where\n",
" -- Generate a constraint requiring us to be in a given store at a time,\n",
" -- and no other stores at that same time.\n",
" chooseStore store =\n",
" And (variable store time) \n",
" (foldl1 And (map (Not . flip variable time) (allStores \\\\ [store])))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"With our main logic written we now formulate our full set of constraints:"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"And (And (And (And (And (And (And (Or (Var 'a') (Var 'b')) (Or (Var 'c') (Var 'd'))) (Or (Var 'e') (Var 'f'))) (Not (Var 'b'))) (Not (Var 'c'))) (Const True)) (Or (Or (And (Var 'a') (And (Not (Var 'c')) (Not (Var 'e')))) (And (Var 'c') (And (Not (Var 'a')) (Not (Var 'e'))))) (And (Var 'e') (And (Not (Var 'a')) (Not (Var 'c')))))) (Or (Or (And (Var 'b') (And (Not (Var 'd')) (Not (Var 'f')))) (And (Var 'd') (And (Not (Var 'b')) (Not (Var 'f'))))) (And (Var 'f') (And (Not (Var 'b')) (Not (Var 'd')))))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"-- All available stores and times in the puzzle.\n",
"stores = [Walmart, HomeDepot, Costco]\n",
"times = [Morning, Evening]\n",
"\n",
"constraints :: Expr\n",
"constraints =\n",
" foldl1 And $\n",
" [visitAllConstraint stores times] ++\n",
" map (storeConstraint times) stores ++\n",
" map (timeConstraint stores) times\n",
"\n",
"-- Look at the expression tree\n",
"-- It's quite huge!\n",
"constraints"
]
},
{
"cell_type": "markdown",
"metadata": {
"collapsed": true
},
"source": [
"Can this be satisfied? As our human intuition immediately told us, no, it cannot:"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"satisfiable constraints"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"But now we know how to derive that result algorithmically, with a very simple SAT solver!"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Improving our Algorithm\n",
"\n",
"Our simple backtracking algorithm, while it works, can be pretty slow. It's a brute-force solution to the problem: we simply search through all possible assignments of values to variables, and check whether any of them work. At worst, when given an expression with $N$ variables in it, backtracking search has to check $2^N$ different assignments; this happens if every single assignment is initially guessed incorrectly.\n",
"\n",
"Surprisingly enough, it's possible that asymptotically better algorithms don't exist, as some subsets of SAT ([3-SAT](http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#3-satisfiability)) are known to be NP-complete. The formal definition of NP-completeness involves a bit of math and complexity theory. Roughly speaking, NP problems are those that we can check but not necessarily solve in polynomial time, and NP-complete problems are problems that, if we could solve them in polynomial time, we could solve any NP problem in polynomial time. Computer scientists currently do not know if P is equal to NP; that is, whether all NP problems can be solved in polynomial times. Most people believe that that isn't the case, and that NP-complete problems *cannot* be solved efficiently (in polynomial time). Since 3-SAT is NP-complete, this means that it probably can't be solved in polynomial time, and so quite possibly the exponential asymptotics of backtracking search are the best we can do.\n",
"\n",
"However, even if asymptotically better algorithms cannot exist, that doesn't mean we can't have algorithms that are better in practice. One such algorithm, known as the DPLL Algorithm (named after it's creators, unabbreviated as the Davis–Putnam–Logemann–Loveland algorithm), is effectively a set of heuristics that optimize our simple backtracking search. Although the DPLL algorithm was invented decades ago (in the 60s), many modern SAT solvers still use DPLL as their base, adding many algorithmic tricks, data structures, and low-level optimizations to achieve high performance.\n",
"\n",
"### Conjunctive Normal Form (CNF)\n",
"\n",
"The DPLL algorithm, unlike our backtracking search, requires that the input expressions be of a particular form, known as conjunctive normal form, or CNF. An expression is in CNF if it consists of conjunction of clauses, each of which is a disjunction of literals. In other words, we have a set of clauses; each clause consists of variables and negated variables which are all or-ed together; all the clauses are then and-ed together. For example, the expressions $A \\wedge B \\wedge (C \\vee \\overline A)$ and $(A \\vee B) \\wedge \\overline A$ are in conjunctive normal form (CNF), but the expressions $\\overline{\\overline{A}} \\vee B$ and $\\overline{A \\vee B}$ are not.\n",
"\n",
"It may seem at first that an algorithm that *only* works on such a restricted set of expressions is useless. Our backtracking search works on *any* bolean expression! What's the point of DPLL if it requires something in CNF?\n",
"\n",
"It turns out that any boolean expression can be *converted* to CNF fairly efficiently. If we apply [De Morgan's laws](http://en.wikipedia.org/wiki/De_Morgan%27s_laws) and distribute \"or\"s over \"ands\" repeatedly, we eventually get an expression in CNF. Once we have our expression in CNF, we can feed it to DPLL.\n",
"\n",
"De Morgan's laws allow you to distribute negations over conjunctions (ands) and disjunctions (ors):\n",
"- $\\overline{A \\wedge B} = \\overline{A} \\vee \\overline{B}$.\n",
"- $\\overline{A \\vee B} = \\overline{A} \\wedge \\overline{B}$.\n",
"Applying this repeatedly ensures that the only things inside a negation are literals like $A$ or $B$, and not compound expressions, like $A \\wedge B$.\n",
"\n",
"Distributing disjunctions over conjunctions allows you to float the conjunctions to the outer layer, which we require for CNF:\n",
"$$A \\vee (X \\wedge Y) = (A \\vee X) \\wedge (A \\vee Y)$$\n",
"\n",
"Before discussing DPLL, let's go ahead and implement that conversion. We begin by two helper functions: one which tries to apply De Morgan's laws, and one which tries to distribute an or over an and:"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"-- Get rid of negations on everything but\n",
"-- literals by applying De Morgan's laws\n",
"-- and removing double negations.\n",
"fixNegations :: Expr -> Expr\n",
"fixNegations expr =\n",
" case expr of\n",
" -- Remove double negatives\n",
" Not (Not x) -> fixNegations x\n",
" \n",
" -- De Morgan's laws\n",
" Not (And x y) -> Or (fixNegations $ Not x) (fixNegations $ Not y)\n",
" Not (Or x y) -> And (fixNegations $ Not x) (fixNegations $ Not y)\n",
" \n",
" -- Deal with constants.\n",
" Not (Const b) -> Const (not b)\n",
" \n",
" -- Recurse on sub-terms.\n",
" Not x -> Not (fixNegations x)\n",
" And x y -> And (fixNegations x) (fixNegations y)\n",
" Or x y -> Or (fixNegations x) (fixNegations y)\n",
" x -> x\n",
" \n",
"-- Attempt to distribute Or over And.\n",
"-- For example, A or (B and C) becomes (A or B) and (A or C).\n",
"distribute :: Expr -> Expr\n",
"distribute expr =\n",
" case expr of\n",
" -- Distribute over and in either position.\n",
" Or x (And y z) ->\n",
" And (Or (distribute x) (distribute y))\n",
" (Or (distribute x) (distribute z))\n",
" Or (And y z) x -> \n",
" And (Or (distribute x) (distribute y))\n",
" (Or (distribute x) (distribute z))\n",
" \n",
" -- Recurse on sub-terms.\n",
" Or x y -> Or (distribute x) (distribute y)\n",
" And x y -> And (distribute x) (distribute y)\n",
" Not x -> Not (distribute x)\n",
" x -> x"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Using these two helpers, we can now convert any expression to CNF by applying the two helpers repeatedly. As soon as they stop changing anything, we should have converged to CNF.\n",
"\n",
"In this implementation, we check this by comparing the result against the input, which requires traversing the entire tree an extra time. We could do this much more efficiently by returning whether or not the expression was modified, but we will not here, for the sake of clarity:"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"-- Convert an expression to CNF.\n",
"-- This guarantees that the output is CNF.\n",
"cnf :: Expr -> Expr\n",
"cnf expr =\n",
" if updated == expr\n",
" then expr\n",
" else cnf updated\n",
" \n",
" where\n",
" updated = distribute (fixNegations expr)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This can produce quite huge results. For example, take a look at the expression $A \\vee \\overline{B \\wedge (A \\vee C)}$ when converted to CNF:"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"And (Or (Var 'a') (Or (Not (Var 'b')) (Not (Var 'a')))) (Or (Var 'a') (Or (Not (Var 'b')) (Not (Var 'c'))))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"cnf $ Or (Var 'a') (Not (And (Var 'b') (Or (Var 'a') (Var 'c'))))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The result is a rather length $(A \\vee \\overline{B} \\vee \\overline{A}) \\wedge (A \\vee \\overline{B} \\vee \\overline{C})$, which is indeed in CNF."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### The DPLL Algorithm\n",
"\n",
"The DPLL algorithm adds two shortcuts to our backtracking search, and these two shortcuts require that the input be in CNF.\n",
"\n",
"First of all, in includes a **literal elimination** step. If some literal (like $A$) is seen in only one polarity (that is, it is always $A$ or $\\overline{A}$), we can immediately determine the truth value of that literal. If it is in positive polarity, it must be true, and if it is only in negative polarity, it must be false. For example, in the expression $(A \\vee B) \\wedge (A \\vee \\overline{C})$, we can immediately assign true to $A$, since $A$ occurs in positive polarity only.\n",
"\n",
"Second, it includes a **unit propagation** step. If there exists a clause in the top-level conjunction that consists of only one literal, we can immediately assign a value to that literal. For example, in the expression $A \\wedge (B \\vee \\overline{A})$, we immediately know that $A$ must be true, since it occurs alone.\n",
"\n",
"#### Literal Elimination\n",
"To demonstrate, let's implement incredibliy simple variants of these two steps. We'll start with literal elimination, in which we build a list of all literals and then check whether each one occurs in only one polarity:"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"import Data.Set (Set)\n",
"import qualified Data.Set as Set\n",
"\n",
"-- Get all the literals in an expression.\n",
"literals :: Expr -> Set Char\n",
"literals (Var v) = Set.singleton v\n",
"literals (Not e) = literals e\n",
"literals (And x y) = Set.union (literals x) (literals y)\n",
"literals (Or x y) = Set.union (literals x) (literals y)\n",
"literals _ = Set.empty\n",
"\n",
"-- Literal polarity. Positive means the literal\n",
"-- is never negated; negative means it always is.\n",
"data Polarity = Positive | Negative | Mixed deriving (Show, Eq)\n",
"\n",
"-- Determine whether a literal has a polarity.\n",
"-- Return Nothing if the literal doesn't appear in the expression.\n",
"literalPolarity :: Expr -> Char -> Maybe Polarity\n",
"\n",
"-- Literal in positive polarity\n",
"literalPolarity (Var v) v'\n",
" | v == v' = Just Positive\n",
" | otherwise = Nothing \n",
"-- Literal in negative polarity\n",
"literalPolarity (Not (Var v)) v'\n",
" | v == v' = Just Negative\n",
" | otherwise = Nothing\n",
"\n",
"-- Combine polarities of sub expressions\n",
"literalPolarity e v =\n",
" case e of\n",
" And x y -> combinePolarities [x, y]\n",
" Or x y -> combinePolarities [x, y]\n",
" Not x -> error $ \"Not in CNF: negation of a non-literal: \" ++ show x\n",
" Const _ -> Nothing\n",
" where\n",
" combinePolarities es =\n",
" let polarities = mapMaybe (flip literalPolarity v) es\n",
" in case polarities of\n",
" [] -> Nothing\n",
" ps -> if all (== Positive) ps\n",
" then Just Positive\n",
" else if all (== Negative) ps\n",
" then Just Negative\n",
" else Just Mixed\n",
"\n",
"-- catMaybes :: [Maybe a] -> [a]\n",
"-- Extract only the Just values of a list.\n",
"import Data.Maybe (catMaybes)\n",
"\n",
"literalElimination :: Expr -> Expr\n",
"literalElimination e =\n",
" let ls = Set.toList (literals e)\n",
" ps = map (literalPolarity e) ls\n",
" \n",
" -- Find assignments we can make\n",
" extractPolarized :: Char -> Maybe Polarity -> Maybe (Char, Bool)\n",
" extractPolarized v (Just Positive) = Just (v, True)\n",
" extractPolarized v (Just Negative) = Just (v, False)\n",
" extractPolarized _ _ = Nothing\n",
" \n",
" -- Find *all* possible assignments\n",
" assignments :: [(Char, Bool)]\n",
" assignments = catMaybes $ zipWith extractPolarized ls ps\n",
" \n",
" -- Apply all the assignments.\n",
" replacers :: [Expr -> Expr]\n",
" replacers = map (uncurry guessVariable) assignments\n",
" \n",
" replaceAll :: Expr -> Expr\n",
" replaceAll = foldl (.) id replacers\n",
" in replaceAll e"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can verify that it works by testing it on our earlier example of $(A \\vee B) \\wedge (A \\vee \\overline{C})$:"
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"And (Or (Const True) (Var 'b')) (Or (Const True) (Not (Var 'b')))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"literalElimination $ And (Or (Var 'a') (Var 'b')) (Or (Var 'a') (Not (Var 'b')))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"You'll note that the literal elimination left $B$ alone, since it appeared in positive and negative polarity, but replaced occurences of $A$ with an assignment of true, since all $A$s occurred in positive polarity.\n",
"\n",
"#### Unit Propagation\n",
"\n",
"Next, we'll implement the other DPLL heuristic, unit propagation, in which we find single-literal clauses and assign them a value. First, we'll determine which of the clauses are unit clauses (have only one literal):"
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"-- Given a clause, determine whether it is a unit clause.\n",
"-- If it is, then return the variable name and the polarity;\n",
"-- if it isn't, return Nothing.\n",
"unitClause :: Expr -> Maybe (Char, Bool)\n",
"unitClause (Var v) = Just (v, True)\n",
"unitClause (Not (Var v)) = Just (v, False)\n",
"unitClause _ = Nothing\n",
"\n",
"-- Reduce an expression into a list of clauses.\n",
"-- This has to traverse a tree of And constructors\n",
"-- and create a list out of them.\n",
"clauses :: Expr -> [Expr]\n",
"clauses (And x y) = clauses x ++ clauses y\n",
"clauses expr = [expr]\n",
"\n",
"-- Extract all unit clauses from a CNF expression.\n",
"allUnitClauses :: Expr -> [(Char, Bool)]\n",
"allUnitClauses = mapMaybe unitClause . clauses"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Then, we effect our replacement for all the unit clauses, just like we did in literal elimination:"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"unitPropagation :: Expr -> Expr\n",
"unitPropagation expr = replaceAll expr\n",
" where\n",
" assignments :: [(Char, Bool)]\n",
" assignments = allUnitClauses expr\n",
" \n",
" replaceAll :: Expr -> Expr\n",
" replaceAll = foldl (.) id (map (uncurry guessVariable) assignments)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Testing it on our earlier example of $A \\wedge (B \\vee \\overline{A})$ yields what we expect:"
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"And (Const True) (Or (Var 'b') (Not (Const True)))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"unitPropagation $ And (Var 'a') (Or (Var 'b') (Not (Var 'a')))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Using unit propagation and literal elimination steps, we can augment our backtracking search to implement the DPLL algorithm. Note how the majority of the code looks identical to what we had before:"
]
},
{
"cell_type": "code",
"execution_count": 22,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"-- The only important thing that changed is the\n",
"-- addition of the 'where' clause.\n",
"satisfiableDPLL :: Expr -> Bool\n",
"satisfiableDPLL expr =\n",
" case freeVariable expr' of\n",
" Nothing -> unConst $ simplify expr'\n",
" Just v ->\n",
" let trueGuess = simplify (guessVariable v True expr)\n",
" falseGuess = simplify (guessVariable v False expr)\n",
" in satisfiableDPLL trueGuess || satisfiableDPLL falseGuess\n",
"\n",
" where\n",
" -- Apply our backtracking search *after* literal elimination\n",
" -- and unit propagation have been applied!\n",
" expr' = literalElimination $ cnf $ unitPropagation expr"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Luckily we get the same result on our puzzle:"
]
},
{
"cell_type": "code",
"execution_count": 23,
"metadata": {
"collapsed": false
},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"satisfiableDPLL constraints"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"At this point, you should have a good understanding of backtracking search for SAT solving, as well as DPLL, which is the basis for all further optimizations and heuristics that must come together for a high performance SAT solver. As a disclaimer, note that the code above is *not* meant for performance; it makes a number of assumptions and uses data structures that are not optimal if you want a fast SAT solver.\n",
"\n",
"In the next section, we'll discuss what tricks can be used to make DPLL perform extraordinarily quickly, allowing modern SAT solvers to handle millions of variables and clauses in seconds. We won't focus any more on code, as it quickly gets too unweidly for a blog post when it comes to writing high performance code."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Further Heuristics and Optimizations\n",
"\n",
"When discussing DPLL and backtracking, we've left a few key steps of the algorithm only partially specified. For example:\n",
"- If there are multiple free variables available in an expression, how do we choose which one to branch on?\n",
"- How do we decide whether we should guess true or false for a variable?\n",
"- What data structures should we use for storing clauses, and how do we detect unit clauses and polarized literals?\n",
"\n",
"Accelerating SAT solving relies on answering these, and other questions, in clever ways. As mentioned before, we can't improve the *asymptotic* complexity of our algorithms by answering these questions differently, but we can improve real-world efficiency of our solvers.\n",
"\n",
"Deciding on the next branching literal can be done in a number of ways. In our implementation, we simply used the first literal we encountered. This is not necessarily the best solution – one can imagine a situation in which the first encountered literal happens to conflict with the last chosen literal, and so if the wrong path is chosen, half the search space must be looked at before the error can be fixed.\n",
"\n",
"There exist a number of heuristics which have been used to compute branching literals. For example, you can find the literal that is mentioned in the most clauses. By doing so, you either reduce the search space dramatically (by reducing the number of clauses and maybe variables), or you quickly reach a conflict, which means you waste less time searching through that part of the solution space. While this heuristic is pretty good, it can be fairly expensive to keep track of how many times a literal is used, especially once you have thousands or millions of variables!\n",
"\n",
"Heuristics can also exist for the initial guess on a variable. For example, if a variable occurs more times in the negative than in the positive polarity, it may be better to guess a value of false for it before guessing true. Once again, the value of the heuristic has to be weighed against the cost of computing it.\n",
"\n",
"One last optimization worth mentioning is known as **clause learning**. Clause learning is based off two ideas. First of all, when we encounter a conflict, we can deduce what decisions we made to cause that conflict; from that, we can learn a new clause, forcing us not to make those decisions. Second, we can track which variable assignments imply other assignments, and when a conflict is reached, instead of backtracking one level higher, we can *backjump* as many levels up as necessary to fix the source of the conflict. Together, these two things allow quickly pruning large regions of the search space, dramatically increasing the number of clauses and variables SAT solvers can handle. Many modern SAT solvers are based off DPLL augmented with clause learning, yielding an algorithm known as Conflict-Driven Clause Learning (CDCL)."
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Haskell",
"language": "haskell",
"name": "haskell"
}
},
"nbformat": 4,
"nbformat_minor": 0
}