So far, we’ve developed a 01 knapsack solver in Part I and then generalized it somewhat. The solver is setup to solve general branch and bound solutions of any type (for maximums), given (these are the parameters of BandB
):
 A function
f
that evaluates the objective function where all decisions are made  A function
g
that provides an upper bound estimate for a partially decided problem instance, such that it gives an upper bound for any possible subsequent settings  A function
unFinished
that determines if all decisions have been made  A node of the search tree, starting with all decisions unmade
 An objective function initial value that is less than any valid solution.
So we can now provide the solver with a different set of functions to instead solve the MaxSat problem. The goal of this problem is to maximize the number of true clauses in a Boolean formula. More precisely, given a Boolean formula in disjunctive normal form, decide a setting for variables such that the number of clauses satisfied (true) is maximum.
Consider the following formula:
Here we have nine clauses, each with three literals. There are a total of six Boolean variables (x_{1} through x_{6}) involved in the problem – the setting of these is the decision that needs to be made. Note the ¬ symbol is logical negation, the ∧ symbol is logical conjunction (and) and the ∨ is logical disjunction (or). The problem is to find settings for each of the variables such that the maximum number of the nine clauses are satistfied. This happens to be in ‘3SAT’ form where each clause has 3 literals (a Boolean variable or its negation) but the code will not require this. For example above, if x_{1} = true, x_{2} = false and x_{4} = false, then clause 1 is satisfied since at least one literal is true (¬x_{4} is true).
The evaluation function f
for this problem is quite simple, for a given variable setting evaluate each clause and determine if it is satisfied, and then add them up. Similarly, the unFinished
function is also very simple, test to see if all variables are set; we basically did this for the 01 knapsack already. A searchspace ‘node’ of the problem is also quite similar to the 01 knapsack, its a set of variables such that some may have been decided and some still unset. An initial value less than any valid solution would be 1, that is because a valid number of clauses satisfied would range from 0 to the number in the problem instance (as many as 9 in Eq 3 above).
So that leaves what is usually the most challenging function in branch and bound, the estimator g
.
This is a simple form of MaxSat solver, this problem has a very long history see this for solvers that use branch and bound as well
Well, one simple upper limit is, “evaluate each clause against the variables that have been decided already, and then assume that literals that are not decided yet will be true.” Conversely, that is if all the literals in a clause are false, then there are no future settings that will change this. So the upper bound function will be the total number of clauses, less those that are already known to be false.
With these concepts in hand, we can tackle the coding. Our first step is the define a variable of the problem.
1: 2: 3: 4: 5: 6: 7: 
type MaxSatDiscreteVar = { (* this is a record type in F# *) Name : string; Setting : ZeroOneVarSetting; // discrete value setting } with member var.isUnset = (var.Setting = ZeroOneVarSetting.Unset) 
This is similar to the 01 knapsack variable, but we don’t need Weight or Utility. It does use the ZeroOneVarSetting
from our DiscreteVarTypes
module, although it might be better to use a different type, say one that had Unset, True
and False
instead but we interpret Zero
as false and One
as true. It also introduces the abilty to write member functions for types, here it creates a function isUnset
that returns true if the ZeroOneVarSetting
is Unset
. Next, let’s consider how we are going to represent our problem in F#. Here is a sample:
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 
let vars2 = [ {Name = "v1"; Setting = Unset}; {Name = "v2"; Setting = Unset}; {Name = "v3"; Setting = Unset}; {Name = "v4"; Setting = Unset}; {Name = "v5"; Setting = Unset}; {Name = "v6"; Setting = Unset} ] let clauses2 = [ [1; 2; 4]; // positive = var at that index; negative means not var at index [1; 3; 4]; [2; 3; 4]; [2; 4; 5]; [ 2; 3; 6]; [ 3; 5; 6]; [4; 5; 6]; [2; 5; 6]; [ 3; 5; 6]; ] 
Here we have a variable array of MaxSatDiscreteVar
with given names such that all are Unset, setting up the top node in our search tree. To represent the clauses, we decided on using an integer array of arrays. Each row of the array is a clause, and each element of the row is an index such that an positive index is used for nonnegated literals and a negative value for negative (not) literals. We used indexing that starts at 1 rather than 0 since we could not distinguish +0 and 0. So, a literal 4 means that this is the fourth variable in the variable array in negated (¬) form. A literal 5 is the fifth one in positive form (since F# uses zerobased indexing the fifth variable is at index 4). The example above should correspond to Eq 3 above.
We’ll put the MaxSat related code in a module MaxSat
, here is the whole thing:
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: 27: 28: 29: 30: 31: 32: 33: 34: 35: 36: 37: 38: 39: 40: 41: 42: 43: 44: 45: 46: 47: 48: 49: 50: 51: 52: 53: 54: 55: 56: 57: 58: 59: 60: 61: 62: 63: 64: 65: 66: 67: 68: 69: 70: 71: 72: 73: 74: 75: 76: 77: 78: 79: 80: 81: 82: 83: 84: 85: 86: 87: 88: 89: 90: 91: 
namespace BandBapplication //open DiscreteVarTypes open System.Collections.Generic type MaxSatDiscreteVar = { (* this is a record type in F# *) Name : string; Setting : ZeroOneVarSetting; // discrete value setting } with member var.isUnset = (var.Setting = ZeroOneVarSetting.Unset) module MaxSat = let clausefulleval clauses (vars:MaxSatDiscreteVar array) = // assume all vars are set clauses > Array.map (fun clause > clause > Array.fold (fun acc literal > let literalIndex = (abs literal)  1 let literalTrue = match vars.[literalIndex].Setting with  Zero > if literal < 0 then true else false  One > if literal > 0 then true else false  _ > failwith "Attempt to eval with an Unset var" max acc (if literalTrue then 1 else 0) ) 0 ) > Array.sum let clauseNumFalse (clauses:int array array) (vars:MaxSatDiscreteVar array) = let mutable count = 0 for clause in clauses do let mutable clauseIsDefinitelyFalse = true // an empty clause is false? for literal in clause do let literalIndex = (abs literal)  1 let literalTrueOrUnknown = match vars.[literalIndex].Setting with  Zero > if literal < 0 then true else false  One > if literal > 0 then true else false  _ > true clauseIsDefinitelyFalse < clauseIsDefinitelyFalse && (not literalTrueOrUnknown) count < count + if clauseIsDefinitelyFalse then 1 else 0 // add an always false clause! clauses.Length  count let clauseNumFalseFunc clauses (vars:MaxSatDiscreteVar array) = let count = ref 0 Array.iter (fun clause > let clauseIsDefinitelyFalse = ref true // an empty clause is false? Array.iter (fun literal > let literalIndex = (abs literal)  1 let literalTrueOrUnknown = match vars.[literalIndex].Setting with  Zero > if literal < 0 then true else false  One > if literal > 0 then true else false  _ > true clauseIsDefinitelyFalse := !clauseIsDefinitelyFalse && (not literalTrueOrUnknown) ) clause count := !count + if !clauseIsDefinitelyFalse then 1 else 0 // add an always false clause! ) clauses clauses.Length  !count (* return index of unset (first) var, or 1 if all are set (to One or Zero) *) let unsetVarIndex vars = try Array.findIndex (fun var > var.Setting = ZeroOneVarSetting.Unset) vars with  :? KeyNotFoundException > 1 // only create feasible solutions. In this case, all settings are feasible let maxsat_branch g bestSolution vars = let mutable branches = [] let unsetVarIndex = unsetVarIndex vars // should only be called when there are Unset vars, so no 1 check let varArrayZero = vars > Array.mapi (fun index var > if index = unsetVarIndex then {var with Setting = Zero} else var) let varArrayOne = vars > Array.mapi (fun index var > if index = unsetVarIndex then {var with Setting = One} else var) let gEstimateZero = g varArrayZero let gEstimateOne = g varArrayOne if gEstimateZero > bestSolution then branches < [varArrayZero] if gEstimateOne > bestSolution then branches < varArrayOne :: branches branches 
The code will assume that zerolength clauses are false
There are three (purposely) different styles of coding used in clausefulleval
, clauseNumFalse
, and clauseNumFalseFunc
.
The first function clausefulleval
is going to be used for our f
function, that is to determine how many clauses are true for a fully decided variable set. We note that it is explicitly typing the last argument, vars
as an array of MaxSatDiscreteVar
like this: let clausefulleval clauses (vars:MaxSatDiscreteVar array)
. Why is this needed? Well this module is included along with the knapsack01
module from before. Note that it uses the Settings value, but there isn’t enough in the body of the code to determine if these vars are MaxSatDiscreteVar
or KnapDiscreteVar
— if the code accessed Weight or Utility then it would be clear. But as it stands, we need to clarify that these are MaxSatDiscreteVar
. Notice that this function requires that all of the variables be set, otherwise it failswith a message (think ‘throws an exception’). This function follows a primarily idiomatic functional style.
From the two for
loops in clauseNumFalse
, the compiler can deduce that clauses
is an array of array (technically it only knows that it is a sequence of sequence type), and that the elements must be ints since on line 22 we use an expression that would require the element to be int. However, if we don’t explicitly type the clauses
argument as: (clauses:int array array)
then the compile fails at the clauses.Length
(line 44). Why? Exactly because the for loops only imply a sequence, not necessarily an Array or List type; and sequences are lazily evaluated that is they are only evaluated when an element of the sequence is needed. Therefore they don’t really have a defined length (and can be conceptually infinite – as long as you don’t ask for the value at index ∞), So we needed to clarify that clauses
is an int array of array. The body of the code is straightforward, looping through each clause and then each literal of the clause. If a clause is determined to be true, then the mutable value count is incremented and ultimately returned as the number of true clauses.
The functions clauseNumFalse
and clauseNumFalseFunc
do the same thing, the latter uses a ref
value to accumulate the needed value but the former only needs a mutable one. But in clauseNumFalseFunc
notice that there is no need to define the type for clauses
– this is because the Array.iter applications clarify what clauses must be. Each of these could be rewritten in the functional style of clausefulleval
but I will leave them in the more imperative form, emphasizing that not everything must be in a functional structure. Which is easier to read and maintain is probably subjective.
The final function of interest is maxsat_branch
on lines 7389 in listing above for MaxSat
. It must take an existing search tree node (called vars
since the search node is an array of variables) and branch to feasible new settings. Like in knapsack, we find an Unset variable, and branch to each of One and Zero settings (with the interpretation that One is true and Zero is false). There is no need for a feasibility test as in 01 knapsack where we made sure that the weight limit was not exceeded — all possible settings of Boolean variables are feasible for the problem. We do test that the new settings can be better by testing the upperbound (g
) of the search node against the best known so far.
Now we just need to use our new code for MaxSat in the main program (note that open MaxSat
was included prior to the entry point code shown):
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: 27: 28: 29: 30: 31: 32: 33: 34: 35: 36: 37: 38: 39: 40: 41: 42: 43: 44: 45: 46: 47: 48: 49: 50: 51: 52: 53: 54: 55: 
[<EntryPoint>] let main argv = (* *************************************************************************************** *) (* KNAPSACK EXAMPLE 1 *) let vars1 = [{Name = "food"; Setting = ZeroOneVarSetting.Unset; Weight = 5.0; Utility = 8.0}; {Name = "tent"; Setting = ZeroOneVarSetting.Unset; Weight = 14.5; Utility = 5.0}; {Name = "gps"; Setting = ZeroOneVarSetting.Unset; Weight = 1.0; Utility = 3.0}; {Name = "map"; Setting = ZeroOneVarSetting.Unset; Weight = 0.5; Utility = 3.0} ] let weightLimit1 = 16.0 let vars1Sorted = (Array.sortBy (fun elem > elem.Utility / elem.Weight) vars1) // still have this let gknap1 = knapestimator weightLimit1 let knapAnyUnset = Array.exists (fun (elem:KnapDiscreteVar) > ZeroOneVarSetting.isUnset elem.Setting) (* Invoke *) let (solutionUtility, solutionVars) = BandB knapmultiplySumUtility gknap1 branchknap knapAnyUnset vars1Sorted 1.0 printfn "Best Utility = %f" solutionUtility for var in solutionVars do printfn "%A" var (* *************************************************************************************** *) (* MAXSAT EXAMPLE 1 *) let vars2 = [ {Name = "v1"; Setting = Unset}; {Name = "v2"; Setting = Unset}; {Name = "v3"; Setting = Unset}; {Name = "v4"; Setting = Unset}; {Name = "v5"; Setting = Unset}; {Name = "v6"; Setting = Unset} ] let clauses2 = [ [1; 2; 4]; // positive = var at that index; negative means not var at index [1; 3; 4]; [2; 3; 4]; [2; 4; 5]; [ 2; 3; 6]; [ 3; 5; 6]; [4; 5; 6]; [2; 5; 6]; [ 3; 5; 6]; ] let f2 = clausefulleval clauses2 // partial func application let g2 = clauseNumFalseFunc clauses2 let maxsatAnyUnset = Array.exists (fun elem > elem.Setting = ZeroOneVarSetting.Unset) // no qualifier needed let (bestValue2, solution2) = BandB f2 g2 maxsat_branch maxsatAnyUnset vars2 1 printfn "Solution 2:" printfn "# clauses satisfied = %d out of %d" bestValue2 clauses2.Length solution2 > Array.iter (fun elem > printfn "%s = %s" elem.Name (match elem.Setting with  ZeroOneVarSetting.Unset > "<ERR:UNSET>"  ZeroOneVarSetting.Zero > "false"  _ > "true")) System.Console.ReadKey() > ignore // don't close the output window until a key is hit 0 
We see that we are using our solver for both the previous 01 knapsack and our new MaxSat formulation. Let’s investigate the types in the BandB
calls, which is:
This says that:
BandB
takes a first argumentf
that takes an (generic) argument of'a
and produces a'b
.BandB
takes a second argumentg
that takes an (generic) argument of'c
.BandB
takes a third argumentbranch
that takes an (generic) argument of'a
and produces an'a list
.BandB
takes a fourth argumentunFinished
that takes generic argument of'a
and produces abool
.BandB
takes a fifth argumentnode
that is of type'a
.BandB
takes a sixth argumentinitLowestValue
which is of type'b
. And finally,
BandB
produces a tuple of type'b * 'a
.
Other than the bool
result for unFinished
all of the arguments are generic. The specific types are a bit different for each of the invocations, for example 'b
is an float for knapsack (line 16) but an int for MaxSat (line 46). We will revisit this topic after we do the traveling salesman problem on the next page. But for now if we run the code we get:
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: 27: 
BandB: total settings queued = 13, total number of evals: 1 Best Utility = 14.000000 {Name = "map"; Weight = 0.5; Utility = 3.0; Setting = One;} {Name = "gps"; Weight = 1.0; Utility = 3.0; Setting = One;} {Name = "food"; Weight = 5.0; Utility = 8.0; Setting = One;} {Name = "tent"; Weight = 14.5; Utility = 5.0; Setting = Zero;} BandB: total settings queued = 14, total number of evals: 3 Solution 2: #clauses satisfied = 9 out of 9 v1 = true v2 = true v3 = true v4 = true v5 = false v6 = false 
Looking at the new results for MaxSat we see that we were able to satisfy all nine clauses with the given variable settings. We also note that there are 6 variables, so there are 2^{6} = 64 possible variable settings and 2^{6+1} – 1 = 127 nodes in the search tree, but we were able to determine an optimum result queueing only 14 nodes and evaluating 3 settings.
Download code so far
As on the previous page, the download is a Visual Studio solution file.
Refactoring and improving
At this point, we see that the queue we are creating, based on the branch function for each problem type, is unsorted. That is, the queue is simply built by concatenanting new nodes from the branch function. However, we would like to do a bestfirst search, that is select the node from the queue that has the best (highest) possible upper limit. The idea is that this may lead to a good solution faster (with less exploration of the search tree).
As it stands now, the upperlimit bound function g
is embedded in the branch function; the functionality of which is to both provide branches that are feasible and to ensure that they meet the upperbound limit. But if we want to sort the queue by bound, then we need to know the g
value at in the BandB
function where the whole queue is, not just in the branch function. We could invoke it again in the BandB
function but that is wasteful.
So we are going to refactor the code, that is ‘move functionality around’. We can remove both the g
function and bestUtility arguments from the branch functions. And then apply g
in the BandB
function using it to sort or prune nodes returned by the branch.
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: 27: 28: 29: 30: 31: 32: 33: 34: 35: 36: 37: 38: 
module BandB = let BandB f g branch unFinished node initLowestValue = let bestUtility = ref initLowestValue; // update: queue elements are now a 2tuple (pair) of gupperbound estimate and node let mutable queue = [ (g node, node) ] let mutable bestNode = node // best var settings found, nothing so far. // these are only informational, not needed in the routine let mutable numberOfQueues = 1 // we just queued the start, so 1 let mutable numberOfEvals = 0 // number of times we evaluated the function with all vars set while not queue.IsEmpty do match queue with  (gNode,curNode) :: restOfQueue > if unFinished curNode then // update: apply `g` here instead, simplifying branch, and sort the queue let toQueueAll = branch curNode let toQueueAugmented = toQueueAll > List.map (fun elem > ((g elem), elem)) let toQueue = toQueueAugmented > List.filter (fun elem > (fst elem) > !bestUtility) queue < (toQueue @ restOfQueue) > List.sortBy (fun elem > fst elem) > List.rev numberOfQueues < numberOfQueues + toQueue.Length else let util = f curNode numberOfEvals < numberOfEvals + 1 if util > !bestUtility then bestUtility := util bestNode < curNode queue < restOfQueue // we've processed curNode, take it off the queue  _ > () // queue isempty, do nothing printfn "BandB: total settings queued = %d, total number of evals: %d" numberOfQueues numberOfEvals (!bestUtility, bestNode) 
In this version, the queue is not simply the list of search nodes, but a tuple (pair) of: upper bound estimate for the node and the node. The branch function is called on line 18, now with just an argument of curNode
. We expect the branch function to return a list of nodes branched from curNode
such that each are feasible (e.g. for knapsack don’t go over weight) but do not concern themselves with bound estimates. That is handled on lines 1922 where we take the list of branched nodes (toQueueAll
), augment each with their upperbound (toQueueAugmented
) and then filter them down to only those that can be better than the best solution found so far (toQueue
). As before since we want to use the value bestUtility
in an inner closure (the filtering part) we need to make it a reference type. We will revisit line 24 later. The modified branch function for knapsack is:
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 
let branchknap wlimit vars = let unsetVarIndex = unsetVarIndex vars // should only be called when there are Unset vars, so no 1 check let varArrayZero = vars > Array.mapi (fun index var > if index = unsetVarIndex then {var with Setting = Zero} else var) let varArrayOne = vars > Array.mapi (fun index var > if index = unsetVarIndex then {var with Setting = One} else var) // not only use g but also ensure feasibilty! let zeroMakesWeight = (knapmultiplySumWeight varArrayZero) <= wlimit let oneMakesWeight = (knapmultiplySumWeight varArrayOne) <= wlimit // update the queue, first match is the match (zeroMakesWeight, oneMakesWeight) with  true,true > varArrayOne :: [varArrayZero]  true,false > [varArrayZero]  false,true > [varArrayOne]  _ > [] // Neither case, nothing 
And the modified branch for MaxSat is:
1: 2: 3: 4: 5: 6: 7: 8: 9: 
// only create feasible solutions. In this case, all settings are feasible let maxsat_branch vars = let unsetVarIndex = unsetVarIndex vars // should only be called when there are Unset vars, so no 1 check let varArrayZero = vars > Array.mapi (fun index var > if index = unsetVarIndex then {var with Setting = Zero} else var) let varArrayOne = vars > Array.mapi (fun index var > if index = unsetVarIndex then {var with Setting = One} else var) varArrayOne :: [varArrayZero] 
Each of these are simpler now that bounding functionality was moved to the main BandB
routine. The main code is the same.
Finally, let’s revisit line 24 from BandB
, it reads:
1:

queue < (toQueue @ restOfQueue) > List.sortBy (fun elem > fst elem) > List.rev 
The documentation I’ve found doesn’t say what the computational complexity of a List.sort is, but since it appears to be a comparison sort, this would be O(n log n).
The idea being that we want to sort descending on the g
upper bound estimates, using the sortBy function. This puts the node with the highest upperbound at the front of the queue for the next loop. As of F# v4.0, there is a sortDescending
function for lists, but we leave this code as is for now as we will revisit reverse sorting in Part III. We could avoid application of the lambda function that is used to sort on the upper bound only and instead use:
1:

queue < (toQueue @ restOfQueue) > List.sort > List.rev 
This would sort the values as a tuple, rather than only on the first element of the tuple (which is the g
estimate), but the downside of this is then node is required to have a comparison function. For our cases here, of KnapDiscreteVar
and MaxSatDiscreteVar
this isn’t a problem as they are sortable but in general there is no reason to require ordering of search nodes so its better to leave the sorting to just using the bound. To avoid using the list reverse, what if we sorted the elements using the negative of the fst elem
value? This should result in a reverse sorted list, so this should work:
1:

queue < (toQueue @ restOfQueue) > List.sortBy (fun elem > (fst elem)) // elem becomes int??? 
Update: From this reference, it appears that use of the unary operator () will change the generic arg to an int
But it doesn’t … it will cause the elem in the lambda function to change from a generic type to an int (see update note in gutter). As unary minus is indeed applicable to both ints and floats, we would have to explicitly type the first element argument to float to have a unary float minus operator. But we will leave this code as is for now, and revisit this in Part III.
If we run this code, we get:
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: 27: 28: 
BandB: total settings queued = 19, total number of evals: 4 Best Utility = 14.000000 {Name = "map"; Weight = 0.5; Utility = 3.0; Setting = One;} {Name = "gps"; Weight = 1.0; Utility = 3.0; Setting = One;} {Name = "food"; Weight = 5.0; Utility = 8.0; Setting = One;} {Name = "tent"; Weight = 14.5; Utility = 5.0; Setting = Zero;} BandB: total settings queued = 23, total number of evals: 4 Solution 2: #clauses satisfied = 9 out of 9 v1 = false v2 = true v3 = true v4 = true v5 = false v6 = false 
which is worse than our previous solver, requiring more queues and evals than before. So it might seem that the bestfirst idea isn’t working, but let’s wait to analyze this more in later sections. Also note that the MaxSat solution found is different, but still all the clauses are satisfied — branch and bound is a complete solver and will find an optimal solution but it may not be unique (in this case there are mulitple settings that provide the optimal solution).