Solving Non-Boolean Satisfiability Problems with the Davis-Putnam Method Peter G. Stock October 1999 -- March 2000 Abstract The Davis-Putnam method has received recent attention for its ability to solve large problems. Many of these problems are non-Boolean, in that they are most naturally expressed as formulas containing variables with domains of more than two values. There are two approaches to solving non-Boolean formulas --- either translate the problem into a Boolean equivalent and solve this with a Boolean procedure, or use a non-Boolean procedure directly on the non-Boolean formula. This project develops a direct non-Boolean Davis-Putnam procedure and compares the results of using the two approaches. \pagenumbering{roman} \tableofcontents Notation used = Equality \equiv Equivalence () Grouping parentheses {a,b,c}, A Sets \in Set membership \notin Set non-membership \subseteq Subset relation \supset Proper superset relation \cup Set union \cap Set intersection \setminus Set subtraction \neg Logical ``not'' \vee Logical ``or'' \wedge Logical ``and'' T, F Truth values x Boolean variable X Non-Boolean variable X\in {a,b} Non-Boolean literal x \mapsto T Boolean variable assignment X \mapsto a Non-Boolean variable assignment Introduction \pagenumbering{arabic} Boolean satisfiability The satisfiability problem (SAT) is fundamental in solving many practical problems and spans a wide range of areas of computer science, such as computer vision, scheduling, circuit design and automated reasoning. Methods for solving SAT are therefore important for the development of efficient computing systems. SAT is of particular interest in the field of theoretical computer science, because it was the first problem to be proven to be NP-complete by Stephen Cook in 1971 \cite{Cook}. Even though SAT may be intractable (all algorithms to solve SAT currently take exponential time in the worst case), a good average case performance is sought. Davis-Putnam Although the Davis-Putnam method (DP) was developed nearly forty years ago (first published in 1960 \cite{DP}, revised in 1962 \cite{DPL}), it still remains one of the best complete procedures for determining Boolean satisfiability. The best currently available DP-based solvers do not vary significantly from the concept described in \cite{DPL}, although their performance has advanced significantly. Modern DP-based solvers can now routinely solve formulas containing hundreds of variables --- ``SATO'' has solved over one hundred open quasi-group problems in design theory. Although incomplete methods have recently come into the limelight for their performance, they cannot decide SAT, i.e. they cannot prove unsatisfiability. Non-Boolean problems Many problems are non-Boolean, i.e. they are most concisely formulated in terms of variables with domains other than {True, False}. A non-Boolean formula is constructed from variables which have domains of size k. In this way, non-Boolean formulas generalise Boolean formulas. The traditional approach to solving a non-Boolean formula is to translate it into equivalent Boolean formula and solve this with a Boolean solver. The direct approach is to modify a Boolean solver so that it operates directly on the non-Boolean formula. A previous project by a student at the university of York \cite{Peugniez} explored the direct approach by developing a non-Boolean stochastic local search procedure (NB-walksat). The results showed that the two methods are not trivially different --- the direct method significantly outperformed the translation method on a range of problems. Non-Boolean Davis-Putnam The success of NB-walksat led to the idea that a non-Boolean generalisation of the Davis-Putnam method may show similar results. This project develops a non-Boolean version of the Davis-Putnam procedure and empirically compares it with the translation approach. The results show that as domain size increases, the direct method performs significantly better than the translation method on a number of problems, while on others the translation approach is more efficient. The performance is analysed, the strengths and weaknesses of each of the methods are discussed and a number of possible improvements are presented. Project outline Chapter 2 reviews the current state of the art and discusses the topics which are relevant to the development of a non-Boolean Davis-Putnam SAT solver. Chapter 3 introduces the non-Boolean Davis-Putnam procedure and outlines it's implementation. The empirical tests are also described. Chapter 4 presents the experimental results and analyses them. Chapter 5 concludes the report and suggests explanations for the observed trends. The advantages and disadvantages of the non-Boolean Davis-Putnam procedure are discussed and avenues for future development are proposed. Review 2.1 Boolean formulas A Boolean formula is constructed from literals (variables or constants) using the operators \neg , \vee and \wedge (the \neg operator conventionally has highest precedence). There are other Boolean operators but formulas containing these may be expressed as equivalent formulas containing only \neg , \vee and \wedge . A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals, each of which may either be positive (a variable or constant) or negative (a variable or constant with the \neg operator applied to it). All Boolean formulas can be expressed as equivalent CNF formulas. e.g. (b \vee r) \wedge (r \vee s) \wedge (\neg b \vee \neg r) A Boolean variable can have one of two values: True or False. For any variable x, x is a Boolean formula. For any Boolean formulas x and y, the following are also Boolean formulas and define the semantics of the operators \neg (not), \vee (or) and \wedge (and). \neg x is True if x is False; otherwise it is False. x \vee y is True if x is True or y is True (or both x and y are True); otherwise it is False. x \wedge y is True if both x and y are True; otherwise it is False. +--+--------+ |x | \neg x | +--+--------+ +--+--------+ |F | T | +--+--------+ |T | F | +--+--------+ +--+---+---------+ |x | y | x\vee y | +--+---+---------+ +--+---+---------+ |F | F | F | +--+---+---------+ |F | T | T | +--+---+---------+ |T | F | T | +--+---+---------+ |T | T | T | +--+---+---------+ +--+---+-----------+ |x | y | x\wedge y | +--+---+-----------+ +--+---+-----------+ |F | F | F | +--+---+-----------+ |F | T | F | +--+---+-----------+ |T | F | F | +--+---+-----------+ |T | T | T | +--+---+-----------+ Truth assignments A truth assignment is a function from variables to the set of values {True, False}, a total truth assignment is a total function (every variable from the formula is mapped to a value). A truth assignment A satisfies a formula f if and only if the result of applying A to f (replacing each variable in f with its associated value from A) is True. 2.1.1 The satisfiability problem The satisfiability problem (SAT) is to decide for a given formula whether there exists a satisfying truth assignment. Most automated SAT solvers operate on Boolean formulas in CNF, so there is no loss of generality in considering only formulas of this type. Indeed, it is often the case that CNF is the natural encoding of many problems([footnote] Other options include nested and/or and DNF (Disjunctive Normal Form) where each disjunct specifies the criteria for a possible solution. Formulas in DNF are trivially solvable for SAT in linear time, but the translation to DNF can introduce massive growth in the formula (effectively enumerating all possible solutions).) . Let's consider an example where 3 friends are organising a fireworks night: Ted wants to have either Bangers or Rockets (or both). Paul wants either Rockets or Sparklers (or both). Sally doesn't like all the noise, and doesn't want both Bangers and Rockets. Let b mean Bangers are included r mean Rockets are included s mean Sparklers are included Then Ted's constraint is: b \vee r Paul's is: r \vee s Sally's is: \neg (b \wedge r) \equiv \neg b \vee \neg r (by DeMorgan's law) To please everybody we must satisfy (b \vee r) \wedge (r \vee s) \wedge (\neg b \vee \neg r) There are three solutions that conform to everybody's constraints. Either have only rockets, have rockets and sparklers, or have bangers and sparklers. These solutions correspond to the assignments: b \mapsto F, r \mapsto T, s \mapsto F b \mapsto F, r \mapsto T, s \mapsto T b \mapsto T, r \mapsto F, s \mapsto T +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |b | r | s | b\vee r | r\vee s | \neg b\vee \neg r | (b\vee r)\wedge (r\vee s)\wedge (\neg b\vee \neg r) | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |F | F | F | F | F | T | F | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |F | F | T | F | T | T | F | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |F | T | F | T | T | T | T | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |F | T | T | T | T | T | T | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |T | F | F | T | F | T | F | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |T | F | T | T | T | T | T | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |T | T | F | T | T | F | F | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ |T | T | T | T | T | F | F | +--+---+---+---------+---------+-------------------+-----------------------------------------------------+ The truth-table can be constructed to enumerate all possible solutions with brute force. This method quickly becomes very inefficient for all but the simplest problems. It requires exponential space and time in the number of variables since it examines every possible truth assignment. 2.2 The Davis-Putnam method In 1960, Martin Davis and Hilary Putnam published an article describing an efficient way of searching the truth-assignment space. Referred to as The Davis-Putnam method (or DP([footnote] It is more apt to refer to the method in Loveland's form, which introduced the splitting rule in \cite{DPL}.) for short), this procedure is a systematic search through a tree of partial truth assignments. At each node in the tree a variable is branched on --- two simpler subtrees are created by assigning the variable to True in one subtree and False in the other. DP recursively explores these subtrees, essentially performing a depth-first search through the tree. The Davis-Putnam method was soon improved by the addition of a heuristic to choose which variable to make a branch at each node in the tree. This is an important part of the DP procedure which affects how quickly solutions and contradictions are found. Now, DP can solve fairly large problems, but has been overshadowed recently by local search methods. It has recently gained attention from the development of more sophisticated heuristics and SATO (a DP-based solver) has solved some open quasi-group problems. DP is usually restricted to work on CNF formulas, since this makes the implementation of the simplification step more efficient. If a variable is assigned to True, all clauses containing negative occurrences of that variable have the variable removed from them and all clauses containing positive occurrences of that variable are removed from the formula (vice-versa for False). If the resulting formula is empty, it has been satisfied by the current truth assignment (and any total truth assignment that extends it also satisfies the formula). If an empty clause([footnote] An empty clause is one with no literals, which is False under all assignments because it can never contain a True literal.) is found then an unsatisfiable state has been reached and the procedure backtracks to the last choice point in the tree and explores the other branch. If all branches have been explored then the formula is unsatisfiable. Certain simplification steps may be applied at each node in the search tree, such as unit propagation and pure literal elimination, both described in the original Davis-Putnam article. Both techniques fix the values of variables which would otherwise be considered choice points. The unit propagation rule states that if a clause contains only a single variable, it may immediately be assigned the value that satisfies that clause (since assigning the opposite value would falsify the clause and also the formula). e.g. (\neg x \vee \neg y \vee z) \wedge y y \mapsto T \Rightarrow (\neg x \vee F \vee z) \wedge T \Rightarrow (\neg x \vee z) Pure literal elimination searches the formula for literals that only appear positively or only negatively. They can be assigned a value immediately, eliminating a potential choice point. It should be noted that this technique commits to branches whose alternative may not lead to immediate failure (as in unit propagation). This gives the intuitive impression of being a particularly powerful technique, although in practice pure literals do not occur frequently enough in the search to produce significant efficiency gains (see \cite{Freeman}). e.g. (x \vee y \vee \neg z) \wedge (x \vee \neg y) \wedge (y \vee z) x \mapsto T \Rightarrow (T \vee y \vee \neg z) \wedge (T \vee \neg y) \wedge (y \vee z) \Rightarrow (y \vee z) 2.2.1 Definition of the Davis-Putnam method Definition: \overline{l}=\neg x if l is x (i.e. positive) \overline{l}=x if l is \neg x (i.e. negative) function Davis-Putnam(formula f) return Boolean is /* unit propagation */ repeat for each unit clause l in f do remove from f all clauses that contain l remove \overline{l} from all clauses in f in which it appears end for if f is empty then return True else if f contains the empty clause then return False end if until there are no unit clauses in f /* pure literal elimination */ for all variables x that only appear positively in f do remove from f all clauses that contain x end for for all variables x that only appear negatively in f do remove from f all clauses that contain \neg x end for /* branching */ pick a variable x from f if Davis-Putnam(f\wedge x) or Davis-Putnam(f\wedge \neg x) then return True else return False end if end function \label{Boolean Davis-Putnam} Note that this definition does not dictate the order of variables chosen for branching (the variable order), or the method of exploring the branches of the search tree. It is common to use a depth-first method, presenting a choice of which branch to explore first (the value order). These topics are examined a little further on. This procedure determines whether or not a formula is satisfiable; by keeping track of the current assignment, the procedure can return a satisfying assignment if the formula is satisfiable. Mathematical definition of unit propagation For any CNF formula f_{n} and variable assignment A_{n}, the process of unit propagation on (f_{n},A_{n}) produces (f_{n+1},A_{n+1}), where A_{n+1}=A_{n}\bigcup \{l\mapsto val(l)\mid l\in U\} f_{n+1}=simplify(f_{n},A_{n+1}) where U is the set of all literals that appear in unit clauses in f_{n} val(l) is True if l appears positively in U, False otherwise simplify(f,A) returns the simplified formula arising from applying the substitutions in A to f For all satisfying assignments A_{sat}, if A_{sat} extends A_{n}, A_{sat} also extends A_{n+1}. Mathematical definition of pure literal elimination For any CNF formula f_{m}and variable assignment A_{m}, the process of pure literal elimination on (f_{m},A_{m}) produces (f_{m+1},A_{m+1}), where A_{m+1}=A_{m}\bigcup \{l\mapsto val(l)\mid l\in P\} f_{m+1}=simplify(f_{m},A_{m+1}) where P is the set of all pure literals that appear in f_{m} (either all positive or all negative) val(l) is True if l appears positively in P, False otherwise simplify(f,A) returns the simplified formula arising from applying the substitutions in A to f If there exists a satisfying assignments A_{sat} that extends A_{m}, then there exists a satisfying assignment A_{sat}' that extends A_{m+1} (A_{sat} and A_{sat}' may be the same). In other words, if there exists a satisfying truth assignment that extends the current variable assignment, there must also exist a satisfying assignment after the process of pure literal elimination, although the process may restrict the search, pruning some branches which contain satisfying assignments. Both unit propagation and pure literal elimination are complete for the problem of finding a single satisfying variable assignment (given a satisfiable state([footnote] A satisfiable state is a state in the search from which it is possible to reach a solution. An unsatisfiable state is one where it is impossible to reach a solution from.) , they do not produce an unsatisfiable state). While unit propagation is complete for the problem of finding all solutions, pure literal elimination is not, since it may eliminate areas of the search space which contain more general solutions. Most SAT solvers interpret the satisfiability problem as determining if there exists a satisfying assignment and if so returning a single solution. 2.2.2 An example of the Davis-Putnam procedure Taking our previous fireworks example, we have the following start formula: f_{0} = (b \vee r) \wedge (r \vee s) \wedge (\neg b \vee \neg r) A_{0} = {} There are no unit clauses so unit propagation can't take place. Suppose r is chosen to branch on. Then we have the choices r \mapsto T and r \mapsto F. Suppose r \mapsto T is explored first. r \mapsto T f_{1} = (b \vee T) \wedge (T \vee s) \wedge (\neg b \vee F) f_{1} = \neg b A_{1} = {r \mapsto T} Unit propagation is now applied to make the assignment b \mapsto F. b \mapsto F f_{2} = T f_{2} = empty formula A_{2} = {b \mapsto F, r \mapsto T} The empty formula has been found and the formula has been satisfied. Note that it has been satisfied with the non-total assignment A_{2} (S has not been given a value). This means that any total assignment that extends A_{2} will satisfy f_{0}. The two total assignments are: {b \mapsto F, r \mapsto T, s \mapsto T} {b \mapsto F, r \mapsto T, s \mapsto F} Suppose we had chosen r \mapsto F as the first branch to explore, instead of r \mapsto T. Then the search would have discovered the other solution from our truth table. r \mapsto F f_{1} = (b \vee F) \wedge (F \vee s) \wedge (\neg b \vee T) f_{1} = b \wedge s A_{1} = {r \mapsto F} Unit propagation forces b \mapsto T and s \mapsto T. b \mapsto T s \mapsto T f_{2} = T \wedge T f_{2} = empty formula A_{2} = {b \mapsto T, r \mapsto F, s \mapsto T} \rotatebox{270}{\includegraphics{tree.eps}} The search tree above shows both solution points. Note that the procedure does not need to explore the whole tree and that backtracking was unnecessary in this instance. 2.2.3 Variable order The large size of the potential search space is the main problem with the DP procedure, but choosing the best variable to branch on at each node in the search tree can greatly reduce the size of the explored search space. The variable order dictates which variable is chosen to branch on at each node in the search tree and has a dramatic effect on the efficiency of the Davis-Putnam procedure. The branching heuristic decides the variable order. There are a number of choices of heuristic, both static (where the complete variable ordering is determined before the search begins) and dynamic (which identify the next variable to branch on at each node in the search tree). Most modern solvers use dynamic heuristics --- the reduction in search tree size far outweighs the computational cost of applying the heuristic at each node. The simple moms heuristic A popular heuristic is to choose a variable([footnote] There may be more than one candidate, so a tie-breaking heuristic is sometimes used.) that has Maximal Occurrences in Minimal Size clauses (the mom's heuristic). Intuitively it chooses the most constrained variable to branch on, increasing the effect of unit propagation after the branch. e.g. f = (a \vee e) \wedge (\neg a \vee b) \wedge (\neg a \vee c) \wedge (\neg b \vee \neg d) \wedge (b \vee \neg c \vee d) +---------++--------------------+----------+----------++--------------------+----------+----------+ | || Occurrences in | | || Occurrences in | | | |Variable ||clauses of length 2 | positive | negative ||clauses of length 3 | positive | negative | +---------++--------------------+----------+----------++--------------------+----------+----------+ +---------++--------------------+----------+----------++--------------------+----------+----------+ | a || 3 | 1 | 2 || 0 | 0 | 0 | +---------++--------------------+----------+----------++--------------------+----------+----------+ | b || 2 | 1 | 1 || 1 | 1 | 0 | +---------++--------------------+----------+----------++--------------------+----------+----------+ | c || 1 | 1 | 0 || 1 | 0 | 1 | +---------++--------------------+----------+----------++--------------------+----------+----------+ | d || 1 | 0 | 1 || 1 | 1 | 0 | +---------++--------------------+----------+----------++--------------------+----------+----------+ | e || 1 | 1 | 0 || 0 | 0 | 0 | +---------++--------------------+----------+----------++--------------------+----------+----------+ The variable a would be chosen to spilt on, since it occurs most often in the smallest clauses (in this case binary clauses). In the case of a tie, it would seem appropriate to consider the next smallest clauses. although many implementations of the mom's heuristic consider only binary clauses and disregard all others (for optimisation). Some implementations of the mom's heuristic favour balanced variables (those which occur frequently both positively and negatively). +---------++--------------------+----------+----------+ | || Occurrences in | | | |Variable ||clauses of length 2 | positive | negative | +---------++--------------------+----------+----------+ +---------++--------------------+----------+----------+ | p || 4 | 3 | 1 | +---------++--------------------+----------+----------+ | q || 4 | 2 | 2 | +---------++--------------------+----------+----------+ +---------++--------------------+----------+----------+ | r || 9 | 1 | 8 | +---------++--------------------+----------+----------+ | s || 7 | 4 | 3 | +---------++--------------------+----------+----------+ For instance q would be chosen over p as it is the more balanced variable. The motivation for this choice is that it maximises the effect of unit propagation in both subtrees arising from the branch. This principle can be extended to favour balanced variables over more frequently occurring unbalanced ones (e.g. s being preferable to r). Let n(l) be the number of times literal l occurs in the shortest clauses The basic mom's heuristic chooses the variable x for which n(x)+n(\neg x) is maximal, while the balanced mom's heuristic maximises min(n(x),n(\neg x)). The generalised moms heuristic +---------++--------------------+---------------------+ | || Occurrences in | Occurrences in | |Variable ||clauses of length 2 | clauses of length 3 | +---------++--------------------+---------------------+ +---------++--------------------+---------------------+ | x || 5 | 1 | +---------++--------------------+---------------------+ | y || 4 | 8 | +---------++--------------------+---------------------+ In the above example x would be chosen by the moms heuristic, but should it be? It has been suggested that all clauses should be considered with larger clauses being given an exponentially decreasing weight \cite{Jeroslow and Wang}, \cite{Hooker and Vinay}. The Jeroslow-Wang branching rule chooses the literal l which maximises J(l).J(l)=\sum _{c\in C_{l}}2^{n_{c}} Where C_{l} is the set of all clauses which contain l, and n_{c} is the number of literals in clause c. Chu Min Li \cite{Satz} suggests (from the result of empirical tests) that a clause of length n should be counted as 5 clauses of length n+1 (in particular 1 binary clause is worth 5 ternary clauses). Thus in the example above, y would be chosen. This is only a small extension to the basic moms heuristic however and does not show significant performance gains over the basic moms heuristic, possibly because this situation occurs infrequently. The unit propagation lookahead heuristic The unit propagation (UP) heuristic is quite different from the moms heuristic, although it has the same aim --- to maximise the effect of unit propagation in the subtrees resulting from the branch. The UP heuristic calculates the number of clauses that would be shortened (have fewer literals) from branching on each variable (the ``lookahead'') and chooses the variable which shortens the most clauses. This is achieved by examining a set of variables at each branch; a variable x in a formula f is examined by the following procedure: * The formula p is obtained by performing unit propagation on f\wedge x. * The formula q is obtained by performing unit propagation on f\wedge \neg x. * The individual weights of x and \neg x are given by w(x)=diff(p,f) and w(\neg x)=diff(q,f), where diff(a,b) is the number of clauses that are shorter in a than in b. * The overall weight([footnote] Suggested by Freeman in \cite{Freeman}, to balance the number of positive and negative occurrences.) given to the variable is H(x)=w(x)\times w(\neg x)\times 1024+w(x)+w(\neg x). At each node in the search, the pure UP heuristic examines all variables that appear in the formula, choosing the variable x that has the highest H(x) value. To examine every variable is computationally expensive, so a restriction on the variables examined is a good compromise between the speed and accuracy of the heuristic, to obtain the overall fastest procedure. Chu Min Li \cite{Satz} suggests that a restriction based on the familiar moms heuristic performs well, where a variable is examined if it has at least i binary occurrences, of which at least j are positive and j negative. Suggested values for i and j are 1\leq i\leq 4 and 0\leq j\leq 2. Intuitively this restricts the heuristic to variables which are most constrained and therefore more likely to be the best branching candidates. It is widely appreciated that more variables should be examined earlier on in the tree, to increase the power of the heuristic in the more crucial early branches, and all implementations of the UP heuristic attempt to do this. POSIT (Freeman) has a maximum bound on the number of variables examined, as a function of the search tree depth. Satz (Li) shows performance gains from a minimum bound where all variables are examined if the number of variables determined by the restriction is less than this minimum. As an example, early on in the search there are usually few constrained variables so the restriction would not usually give enough variables to exceed the minimum bound, and all variables would be examined. This ``dynamic'' bound on the number of examined variables allows performance gains by adapting to the current state of the search --- if there are few constrained variables (anywhere in the tree) then many variables will be examined, but if there are a sufficient number of constrained variables then only these will be examined. A second benefit of the UP heuristic is that it can detect, for each variable examined, which values falsify the formula after the unit propagation step (commonly called failed literals). The UP heuristic can be easily adapted to detect failed literals simply by testing if each unit propagation lookahead step produces an empty clause (a trivial addition to the unit propagation step). 2.2.4 Value order Each variable branch generates two subtrees. Assuming a depth-first implementation of DP, the subtrees must be explored in some order --- this is the value order. There has been a lot of disagreement as to whether the value order has an affect on the performance of DP. C-SAT \cite{Dubios} chooses the value that satisfies as many literals (and thus clauses) as possible, intuitively choosing the branch that is more likely to lead to a solution. Freeman \cite{Freeman} suggests that the value should be chosen that falsifies as many literals in short clauses as possible. Although this technique seems intuitively to choose the subtree less likely to contain a solution, it maximises the effect of unit propagation in the first subtree explored, thus reaching a global solution quickly if one exists. Both these strategies are based on sound intuitive arguments but they are in conflict with each other --- you can't please both. Furthermore, Freeman compares his recommended method to a fixed value order (i.e. for branching variable x, first explore x \mapsto T then x \mapsto F) and shows that there is no significant performance difference, either in the search tree size or run time on hard random 3-SAT formulas. Tableau \cite{Crawford and Auton} uses a fixed value order, as does satz, which is currently one of the best performing DP solvers. It is worth mentioning that the value order does not affect the performance of the DP procedure on unsatisfiable formulas since the whole tree must be explored. My opinion on the topic is that there is no clear winner out of all the value ordering strategies presented. Theoretically speaking, any satisfiable formula has it's solution (or one of them) expressible as a function of the original formula. Given a suitably powerful technique (for instance the function from all possible satisfiable formulas to their respective satisfying assignments), satisfiability can be determined in a single step simply by examining the formula. Taking this argument to the value ordering level, at any branch the best subtree is a function of the formula. Although I do not argue that the value order does not affect the search, no value order which I am aware of is significantly better on a range of problems than a fixed one. 2.2.5 Other modifications to the DP procedure Preprocessing techniques POSIT uses a technique called initial k-literal deletion, described in the original Davis-Putnam article \cite{DP}. This technique eliminates variables from the formula that have k positive or k negative occurrences. If the literal x occurs in the clauses (x\vee C_{1}),(x\vee C_{2}),\ldots ,(x\vee C_{k}) and it's complement \overline{x} occurs in the clauses (\overline{x}\vee C_{1}'),(\overline{x}\vee C_{2}'),\ldots ,(\overline{x}\vee C_{k'}'), x is eliminated by deleting these clauses and replacing them with \bigwedge ^{k}_{i=1}\bigwedge ^{k'}_{j=1}(C_{i}\vee C_{j}'). This typically increases both the number and size of the clauses in the formula . It is too costly to perform at each node in the tree and only has limited use at the root --- Freeman concludes that search performance is only improved for k=1 and k=2. Many formulas do not have many 1- and 2-literals and therefore cannot be simplified in this way. A limited form of resolution can sometimes be used to refine the input formula before the search begins (again, it is usually too slow to use during the search). It can only be used on certain classes of problems. Problem-dependent techniques If more information about the problem is available, various tweaks can be made to the heuristic to increase performance. For randomly generated formulas, a version of tableau takes as it's input the formula and which parameters where used to generate it. The behaviour of the heuristic is then modified given this information. Symmetry detection is the technique of detecting pairs of variables which can be interchanged without affecting the overall structure of the formula. This is obviously limited to certain classes of structured problems, but can improve performance significantly on these types of problems, removing redundancy from the search. Randomisation and restarts By incorporating randomisation in the heuristic, the Davis-Putnam procedure can be made non-deterministic. The search can then be given a time bound and re-started if it exceeds this. The time bound is initially small, but increases during the search. This technique has generated good results, on several classes of problems \cite{Freeman}. Integration with local search Local search procedures can be used in conjunction with the Davis-Putnam procedure. The input formula is run on local search procedure; if it does not find a solution, the final assignment is input to DP, which uses it to tailor the heuristic. This has been shown by James Crawford in \cite{Local search and DP} to improve performance by about 10%. Crawford tests on random formulas but hypothesises that this technique would better on structured problems. Parallelism The Davis-Putnam procedure is well-suited to coarse-grained parallelism, since the tree can be divided up, and each sub-tree can be explored independently. It is, however, a brute-force method, and doubling the number of processors working on the problem will only permit a constant increase in the feasible problem size. A number of different techniques can be used in parallel (e.g. DP, local search, genetic algorithms) to offset each other's disadvantages. Look-back techniques The backtracking search can often explore regions of the search space which contain no solutions or rediscover the same contradictions repeatedly. For example, if the assignment x \mapsto F leads to a contradiction, the following search could be carried out, repeatedly doing the same work. This incorrect variable ordering can be cured to some extent by using a strong heuristic (e.g. the UP heuristic detects failed literals). \resizebox*{!}{1.5in}{\rotatebox{270}{\includegraphics{tree4.eps}}} When a contradiction is discovered, chronological backtracking explores the most recent unexplored subtree. This may be a branch which was not responsible for the contradiction, so the same contradiction will be found again. There are two main approaches to tackling this problem: selective backtracking and lateral pruning. Selective backtracking consists of testing whether each potential backtracking point was responsible for the failure and skipping over it if it was not. Lateral pruning determines a new constraint each time it finds a contradiction and adds it to the current problem, to ensure that the same contradiction is not repeatedly found. A search procedure which tries to avoid these problems is said to have dependency-directed backtracking. If implemented efficiently, it is particularly useful on certain classes of structured problems. 2.3 Non-Boolean formulas Some problems are not suited to a Boolean encoding, but are more naturally expressed in terms of variables with domain sizes greater than two. Non-Boolean formulas are logical formulas, just as Boolean formulas are, but they contain variables with an arbitrary (but finite) domain size. They are introduced in \cite{NB-walksat}. A non-Boolean literal consists of a variable and an associated value set (consisting of values taken from the variable's domain). For a non-Boolean literal with variable X with value set {a_{1},a_{2},a_{3},\ldots{}}, the semantics are defined as: X\in {a_{1},a_{2},a_{3},\ldots{}} True under an assignment which contains X \mapsto a_{1} or X \mapsto a_{2} or X \mapsto a_{3}, \ldots{}; False otherwise. It can be seen that non-Boolean literals evaluate to either True or False, as in the Boolean case. The logical operators \neg , \vee and \wedge used in non-Boolean formulas have the same semantics as those in Boolean formulas. For any non-Boolean variable X with domain D and any non-empty value set {a_{1},a_{2},\ldots{},a_{n}} \subseteq D, X\in {a_{1},a_{2},\ldots{},a_{n}} is a non-Boolean formula. For any non-Boolean formulas A and B, \neg A, A \vee B and A \wedge B are non-Boolean formulas with semantics identical to the Boolean case. Examples of problems whose encoding into a non-Boolean (NB) formula is simpler than a Boolean encoding are the n-queens problem, constraint satisfaction problems, the Hamiltonian circuit problem, graph colouring and planning. A graph colouring problem consists of an undirected graph and two constraints: that each node has exactly one colour (taken from a set of available colours) and that no two adjacent nodes may be the same colour. The task is to decide if there exists a colouring that satisfies these constraints and if so determine what it is. The figure below shows a simple graph, along with the possible colouring domains for each node. This simple example illustrates the contrast between the direct non-Boolean encoding and the Boolean translation. \rotatebox{270}{\includegraphics{graph_col.eps}} The problem is intuitively expressed as: f= X\neq Y \wedge nodes X and Y must not both be the same colour X\neq Z \wedge nodes X and Z must not both be the same colour Y\neq Z nodes Y and Z must not both be the same colour This can be converted into a non-Boolean formula according to the previously described syntax. f_{NB}= \neg (X\in {r}\wedge Y\in {r}) \wedge \neg (X\in {g}\wedge Y\in {g}) \wedge \neg (X\in {b}\wedge Y\in {b}) \wedge \neg (X\in {r}\wedge Z\in {r}) \wedge \neg (X\in {g}\wedge Z\in {g}) \wedge \neg (X\in {b}\wedge Z\in {b}) \wedge \neg (Y\in {r}\wedge Z\in {r}) \wedge \neg (Y\in {g}\wedge Z\in {g}) \wedge \neg (Y\in {b}\wedge Z\in {b}) Applying DeMorgan's law allows the formula to be re-written in CNF. f_{NB}= (\neg X\in {r}\vee \neg Y\in {r}) \wedge (\neg X\in {g}\vee \neg Y\in {g}) \wedge (\neg X\in {b}\vee \neg Y\in {b}) \wedge (\neg X\in {r}\vee \neg Z\in {r}) \wedge (\neg X\in {g}\vee \neg Z\in {g}) \wedge (\neg X\in {b}\vee \neg Z\in {b}) \wedge (\neg Y\in {r}\vee \neg Z\in {r}) \wedge (\neg Y\in {g}\vee \neg Z\in {g}) \wedge (\neg Y\in {b}\vee \neg Z\in {b}) 2.4 Translating non-Boolean formulas into Boolean formulas All the translation methods presented here are previously described in \cite{NB-walksat}. 2.4.1 The unary translation The straightforward Boolean translation (the unary translation) of this formula is achieved by creating a Boolean variable for every (NB-variable, value) pair. For each NB-variable X and value a from the domain, a Boolean variable x_a is created; the interpretation of the assignment is that X \mapsto a if x_a \mapsto T. For instance z_r, z_g and z_b would be created to stand for the three possible values that the NB-variable Z may take in the previous example. Each literal X\in {a_{1},a_{2},\ldots{},a_{n}} is translated as x_a_{1} \vee x_a_{2} \vee \ldots{} \vee x_a_{n}. The resulting Boolean formula is known as the kernel of the translation. kernel= (\neg x_r\vee \neg y_r) \wedge (\neg x_g\vee \neg y_g) \wedge (\neg x_b\vee \neg y_b) \wedge (\neg x_r\vee \neg z_r) \wedge (\neg x_g\vee \neg z_g) \wedge (\neg x_b\vee \neg z_b) \wedge (\neg y_r\vee \neg z_r) \wedge (\neg y_g\vee \neg z_g) \wedge (\neg y_b\vee \neg z_b) The space of possible variable assignments (the search space) is now larger than that of the corresponding NB-formula (2^{9}=512 possible assignments compared to 3^{3}=27). To preserve the singular nature of the non-Boolean encoding, extra clauses must be added to the translation. A non-singular variable assignment of the Boolean translation is where a corresponding NB-variable is not given a single value. For each NB-variable X, with domain size n, an assignment is singular if exactly one of the corresponding Boolean variables x_1, x_2, \ldots{}, x_n is True. Examples of non-singular assignments from the above example are: {z_r \mapsto F, z_g \mapsto F, z_b \mapsto F} and {z_r \mapsto T, z_g \mapsto T, z_b \mapsto F}. Non-singular assignments are enforced by the inclusion of extra clauses (the at least one (ALO) and at most one (AMO) formulas). The ALO clauses stipulate that each corresponding NB-variable must be assigned at least one value. For each NB-variable X with domain size n, the clause (x_1 \vee x_2 \vee \ldots{} \vee x_n) is present in the ALO sub-formula. ALO= (x_r\vee x_g\vee x_b) \wedge (y_r\vee y_g\vee y_b) \wedge (z_r\vee z_g\vee z_b) The AMO clauses state that for each NB-variable must be assigned at most one value. For each NB-variable X and any values i and j from the domain, x_i and x_j must not both be True in the Boolean translation. Thus for all NB-variables X and values i and j, the clause (\neg x_i \vee \neg x_j) is included in the AMO clauses. AMO= (\neg x_g\vee \neg x_b) \wedge (\neg x_r\vee \neg x_b) \wedge (\neg x_r\vee \neg x_g) \wedge (\neg y_g\vee \neg y_b) \wedge (\neg y_r\vee \neg y_b) \wedge (\neg y_r\vee \neg y_g) \wedge (\neg z_g\vee \neg z_b) \wedge (\neg z_r\vee \neg z_b) \wedge (\neg z_r\vee \neg z_g) The conjunction of the kernel, ALO clauses and AMO clauses gives the unary Boolean translation. Translation = kernel \wedge ALO \wedge AMO f_{B}= (\neg x_r\vee \neg y_r) \wedge (\neg x_g\vee \neg y_g) \wedge (\neg x_b\vee \neg y_b) \wedge (\neg x_r\vee \neg z_r) \wedge (\neg x_g\vee \neg z_g) \wedge (\neg x_b\vee \neg z_b) \wedge (\neg y_r\vee \neg z_r) \wedge (\neg y_g\vee \neg z_g) \wedge (\neg y_b\vee \neg z_b) \wedge (x_r\vee x_g\vee x_b) \wedge (y_r\vee y_g\vee y_b) \wedge (z_r\vee z_g\vee z_b) \wedge (\neg x_g\vee \neg x_b) \wedge (\neg x_r\vee \neg x_b) \wedge (\neg x_r\vee \neg x_g) \wedge (\neg y_g\vee \neg y_b) \wedge (\neg y_r\vee \neg y_b) \wedge (\neg y_r\vee \neg y_g) \wedge (\neg z_g\vee \neg z_b) \wedge (\neg z_r\vee \neg z_b) \wedge (\neg z_r\vee \neg z_g) It turns out that the AMO clauses can be omitted for graph colouring problems, since a solution that colours a node with more than one colour can be transformed into one that colours the node with a single colour, by simply choosing any one of the assigned colours (all clauses relating to that node will still be satisfied). This is intuitively understood because the kernel consists solely of negative literals --- changing a variable from True to False will not cause any clauses to be falsified. Non-singular assignments can be split into two groups: those which are empty and those which are multiple. Some examples are shown below, on the NB-variable X, over the domain {a,b,c,d}. +----+-----+-----+-----+----------------------------+-------------------------+ |x_a | x_b | x_c | x_d | Non-Boolean interpretation | Singular/non-singular | +----+-----+-----+-----+----------------------------+-------------------------+ +----+-----+-----+-----+----------------------------+-------------------------+ | T | F | F | F | X\mapsto a | singular | +----+-----+-----+-----+----------------------------+-------------------------+ | F | F | T | F | X\mapsto c | singular | +----+-----+-----+-----+----------------------------+-------------------------+ | F | F | F | F | X\mapsto nothing | non-singular (empty) | +----+-----+-----+-----+----------------------------+-------------------------+ | F | T | F | T | X\mapsto b or d | non-singular (multiple) | +----+-----+-----+-----+----------------------------+-------------------------+ Positive and negative formulas A (Boolean or non-Boolean) formula is positive if it contains only positive literals, it is negative if it contains only negative literals. By changing a variable from False to True in a positive Boolean CNF formula, all clauses which were previously satisfied will remain satisfied (i.e. more clauses may be satisfied but none will be broken). The opposite is true for negative Boolean CNF formulas, where changing a variable from True to False preserves satisfied clauses. +------------------------------------------------------------------------------------+--------------------+ | Formula | Positive/Negative? | +------------------------------------------------------------------------------------+--------------------+ +------------------------------------------------------------------------------------+--------------------+ | (x\vee y) \wedge (x\vee z) \wedge (y\vee z) | Positive | +------------------------------------------------------------------------------------+--------------------+ |(\neg p\vee \neg q) \wedge (\neg p\vee \neg r) \wedge (\neg q\vee \neg r) | Negative | +------------------------------------------------------------------------------------+--------------------+ | (a\vee \neg b) \wedge (\neg b\vee \neg c) \wedge (\neg a\vee c) | --- | +------------------------------------------------------------------------------------+--------------------+ For any unary translation, if the kernel is positive then the ALO is unnecessary, since any variable can be changed from False to True without breaking any kernel clauses. If we exclude the ALO clauses from the translation (but, of course, include the AMO --- to enforce non-multiple assignments) any solution which contains empty assignments can be transformed into a solution which contains only singular assignments. To do this each NB-variable X which is assigned no value (x_1 \mapsto F, x_2 \mapsto F, \ldots{}, x_n \mapsto F) pick one variable from x_1, x_2, \ldots{}, x_n and assign it to True. This cannot break any clauses, either in the kernel or the AMO. For translations with negative kernels the opposite is True, where the AMO is unnecessary (but the ALO must still be included). In general, a positive NB formula gives rise to a positive kernel under the unary translation and a negative NB formula produces a negative kernel. The effect of the ALO and AMO clauses on the Davis-Putnam procedure\label{Effect of ALO and AMO clauses} As previously mentioned, the size of the search space is increased (sometimes, quite dramatically) in going from the NB-formula to the unary translation. The extra clauses added to enforce singular assignments prevent the Boolean search from actually exploring these non-singular assignments, so although the potential search space is enlarged, none of it will actually be explored([footnote] The search may deviate into a state corresponding to a non-singular (partial) assignment, but it will immediately backtrack because one of the ALO or AMO clauses will be violated.) (in contrast to local search methods such as those in \cite{NB-walksat}). This is quite an important point, as the non-Boolean search procedure does not have as much of an advantage over the translation method as it might first appear. The downside of translating and solving is that the extra clauses hamper the search by storing the singular restriction in the data structures, rather than implicitly in the algorithm. The effect of this is that the data structures must be modified as the search progresses, which takes time. Obviously this effect is greater for formulas with more ALO and AMO clauses. An additional effect is that the extra clauses in the translation (ALO and AMO) may make the heuristic less powerful. The moms heuristic, which picks the variable which occurs most often in the smallest clauses, would give much attention to the AMO clauses (all binary). In the AMO, all unassigned variables appear with relatively equal frequencies, so the kernel formula will have less effect on which variable is chosen. The pure UP heuristic will not be affected by the extra clauses in this way, although the lookahead step may be slower because of the extra clauses (the above point). It is not clear how the UP heuristic with the moms restriction (as in satz) will perform. 2.4.2 The binary translation Another method for translating non-Boolean formulas into equivalent Boolean formulas is the binary translation. In the unary translation one Boolean variable represented a single value for an NB-variable, in the binary translation each Boolean variable represents two values. For the NB-variable X and domain {1,2,3,4}, the Boolean encoding would use two variables, x_a and x_b, with the non-Boolean interpretation being defined as: +----+-----+----------------------------+ |x_a | x_b | Non-Boolean interpretation | +----+-----+----------------------------+ +----+-----+----------------------------+ | F | F | X\mapsto 1 | +----+-----+----------------------------+ | F | T | X\mapsto 2 | +----+-----+----------------------------+ | T | F | X\mapsto 3 | +----+-----+----------------------------+ | T | T | X\mapsto 4 | +----+-----+----------------------------+ In general, for domain size d this method uses \left\lceil \log _{2}d\right\rceil Boolean variables for each non-Boolean variable (the unary encoding uses d Boolean variables). This does not allow non-singular assignments in the search space, but unfortunately can cause large growth in the formula when re-written in CNF --- the innermost conjunctions may need to be distributed outwards([footnote] For negative non-Boolean formulas, this is not a problem since \vee is still the innermost operator.) . This can make the binary translation unfeasibly large for many formulas. An example of this translation method is given below, the conversion to CNF has been omitted. non-Boolean clause X\in {1,2} \vee Y\in {1,3} \vee Z\in {2,4} binary translation (\neg x_a\wedge \neg x_b) \vee (\neg y_a\wedge \neg y_b) \vee (\neg z_a\wedge z_b) \vee (\neg x_a\wedge x_b) \vee (y_a\wedge \neg y_b) \vee (z_a\wedge z_b) 2.4.3 The unary-binary translation The unary-binary translation uses the same unary encoding for the kernel formula, but the clauses to enforce singular assignment have the binary encoding. Therefore the search space is the same, but again, not all of it will be explored. Extra variables are used in the clauses to enforce singular assignments (\left\lceil \log _{2}d\right\rceil for each variable), but the number of clauses is often less, giving smaller formulas. For a non-Boolean variable X with domain {1,2,3}, singular assignments are enforced by ensuring for all values of x_a and x_b, exactly one of x_1, x_2 and x_3 are true. In this example, the domain size is not a power of two so the remaining combinations x_a and x_b must be constrained not to occur. (x_1\Leftrightarrow \neg x_a\wedge \neg x_b) \wedge (x_2\Leftrightarrow \neg x_a\wedge x_b) \wedge (x_3\Leftrightarrow x_a\wedge \neg x_b) \wedge \neg (x_a\wedge x_b) \equiv (x_1\Rightarrow \neg x_a\wedge \neg x_b) \wedge (\neg x_a\wedge \neg x_b\Rightarrow x_1) \wedge (x_2\Rightarrow \neg x_a\wedge x_b) \wedge (\neg x_a\wedge x_b\Rightarrow x_2) \wedge (x_3\Rightarrow x_a\wedge \neg x_b) \wedge (x_a\wedge \neg x_b\Rightarrow x_3) \wedge \neg (x_a\wedge x_b) \equiv (\neg x_1\vee \neg x_a) \wedge (\neg x_1\vee \neg x_b) \wedge (x_a\vee x_b\vee x_1) \wedge (\neg x_2\vee \neg x_a) \wedge (\neg x_2\vee x_b) \wedge (x_a\vee \neg x_b\vee x_2) \wedge (\neg x_3\vee x_a) \wedge (\neg x_3\vee \neg x_b) \wedge (\neg x_a\vee x_b\vee x_3) \wedge (\neg x_a\vee \neg x_b) 2.4.4 Translating negative literals\label{Translating negative literals} Any non-Boolean literal can be represented both positively and negatively. For non-Boolean variable X with domain D, the following are equivalent. \neg X\in {a_{1},a_{2},a_{3},\ldots{}} \equiv X\notin {a_{1},a_{2},a_{3},\ldots{}} \equiv X\in (D\setminus {a_{1},a_{2},a_{3},\ldots{}}) For certain NB formulas (for example graph colouring), the formula is more concisely written using negative literals instead of positive ones. For domain {a_{1},a_{2},a_{3},\ldots{},a_{n}}, the following are equivalent (simply a special case of the above equivalence). X\in {a_{1},a_{2},\ldots{},a_{k-1},a_{k+1},\ldots{},a_{n}} \equiv \neg X\in {a_{k}} For formulas of this kind, using the negative encoding on the NB formula produces much smaller Boolean translations, especially for large domains. This increases the speed of the Boolean search on the translation. Negative literals such as \neg X\in {a_{j},a_{k}} can be smaller than their positive equivalents, but translating a formula full of these will result in many clauses when expressed in CNF. For domain {a,b,c,d,e,f}, the clause \neg X\in {a,d} \vee \neg Y\in {b,e} \vee \neg Z\in {c,f} is translated as: \neg X\in {a,d} \vee \neg Y\in {b,e} \vee \neg Z\in {c,f} \neg (x_a \vee x_d) \vee \neg (y_b \vee y_e) \vee \neg (z_c \vee z_f) \equiv (\neg x_a \wedge \neg x_d) \vee (\neg y_b \wedge \neg y_e) \vee (\neg z_c \wedge \neg z_f) \equiv (\neg x_a \vee \neg y_b \vee \neg z_c) \wedge (\neg x_d \vee \neg y_b \vee \neg z_c) \wedge (\neg x_a \vee \neg y_e \vee \neg z_c) \wedge (\neg x_d \vee \neg y_e \vee \neg z_c) \wedge (\neg x_a \vee \neg y_b \vee \neg z_f) \wedge (\neg x_d \vee \neg y_b \vee \neg z_f) \wedge (\neg x_a \vee \neg y_e \vee \neg z_f) \wedge (\neg x_d \vee \neg y_e \vee \neg z_f) The positive equivalent, X\in {b,c,e,f} \vee Y\in {a,c,d,f} \vee Z\in {a,b,d,e}, is translated as: X\in {b,c,e,f} \vee Y\in {a,c,d,f} \vee Z\in {a,b,d,e} x_b \vee x_c \vee x_e \vee x_f \vee y_a \vee y_c \vee y_d \vee y_f \vee z_a \vee z_b \vee z_d \vee z_e Therefore, it is not usually worth re-writing these types of formula as their negative equivalents before translating (to avoid the AMO clauses) because the translation is usually larger when it is expressed in CNF. Design 3.1 Non-Boolean Davis-Putnam Conceptually, the Boolean DP method is fairly simple: When there is no choice to be made (when there is a unit clause or pure literal in the formula) then do the assignment and simplification, and recurse. Otherwise split up the problem (branch) committing to a new assignment in each subtree. This general concept still holds in the non-Boolean case and provides a suitable level of abstraction to consider the NB-DP procedure. Unit clauses may not consist of a variable with a single value, so unit propagation may now not fully assign a variable. The NB unit propagation step consists of the partial assignment of the variable (the removal of values which would contradict the unit clause variable) and the simplification of the resulting formula. The following example illustrates this. f_{0}= (X\in {a,b}) \wedge (X\in {a,b,c}\vee \alpha ) \wedge (X\in {a,c}\vee \beta ) \wedge (X\in {c,d}\vee \gamma ) X \mapsto {a,b} The assignment of X \mapsto {a,b} is read as ``X is partially assigned to either a or b'', and all other values are ruled out for X at this point in the search. After removing all other values from all literals X in the formula, all occurrences of X\in {a,b} can be assigned True because they will be True whichever of {a,b} actually end up being assigned to X (they exactly match the constraint being propagated). Also, all occurrences of X\in {} can be assigned False, as they will never be satisfied by either X \mapsto a or X \mapsto b. All other literals cannot be simplified to a truth value because they represent a tighter constraint than the original unit clause (e.g. X\in {a} is more tightly constrained than X\in {a,b}). f_{1}= (X\in {a,b}) \wedge (X\in {a,b}\vee \alpha ) \wedge (X\in {a}\vee \beta ) \wedge (X\in {}\vee \gamma ) f_{1}= T \wedge (T\vee \alpha ) \wedge (X\in {a}\vee \beta ) \wedge (F\vee \gamma ) f_{1}= (X\in {a}\vee \beta ) \wedge \gamma The pure literal rule is a little more general([footnote] This may seem trivial, but the Boolean implementation assumes that x is only pure if either x or \neg x does not appear in the formula.) , including variables which occur in the formula with more than one value. (X\in {a,b}\vee Y\in {a,b}) \wedge (X\in {a,c}\vee Y\in {b,c}) \wedge (X\in {a,d}Y\in {c,d}) Here, the value `a' is pure since all occurrences of X appear with the value `a'. Note that this is the case even though `a' is not the only value to appear with X in the formula (e.g. X\in {a,b} appears in the formula). 3.1.1 Non-Boolean branching In the Boolean search, each branch is binary (it produces two subtrees). Additionally, each of the subtrees represents a full commitment to a particular value. These are both good properties. * A small branching factor is more preferable than a large one because each branch produces fewer subtrees --- for the most favourable branch([footnote] The branch with the best ``worst subtree''.) , the worst subtree (the one most difficult to search) is more likely to be better if there are fewer subtrees. From the point of view of the heuristic, the optimal branch is more likely to give rise to more unit propagations in the worst of two subtrees than the worst of three. * A full commitment to a value is useful in each subtree because it means that the most simplification can happen (unit propagation and pure literal elimination). Those properties both occur in the Boolean search, but the non-Boolean search cannot have both, since branches either have to be non-binary or make only a partial commitment (to a subset of values). I have identified three approaches to non-Boolean branching. 1. For n possible values, each branch produces n subtrees, each making a full commitment to a single value. 2. The set of all values that could be explored is divided into two partitions. Each branch produces 2 subtrees, one making a partial commitment to one partition, the other making a partial commitment to the other partition. 3. For active values V, a branch on variable X and value a is binary, where one subtree makes the full commitment X\mapsto a and the other makes the partial commitment X\mapsto V\setminus a. The three branching strategies are illustrated below. \resizebox*{0.8\textwidth}{!}{\rotatebox{270}{\includegraphics{branches.eps}}} Strategies 2 and 3 introduce a further choice into the heuristic in addition to the choice of variable: a partitioning of the value set must be determined for the 2nd strategy and a single value must be chosen for the 3rd. The 3rd strategy is a less general case of the 2nd, but one subtree benefits from a full commitment to a value. In this strategy each branch is unbalanced. The 2nd branching strategy is the most complex --- to decide how to partition for optimal unit propagation is quite(!) difficult. For this reason, I decided against method 2, because I felt that the efficiency of the search would depend heavily on the choice of partition at each branch. I did not have any ideas on how a good partitioning could be determined efficiently, since each value in a partition affects the unit propagation in it's subtree. The binary translation effectively operates like method, but does an arbitrary (but roughly equal) partitioning of the domain. Such a partitioning probably does not allow much simplification. The 3rd strategy is a more specific instance of the 2nd, but commits to a single value in one subtree. The other is unlikely to produce much unit propagation since it commits to all other available values (i.e. all other values that have not been eliminated from inquiry). Sooner or later, this commitment must be refined by another branch, again removing another value. The branching variable should be chosen so as to have the maximum simplification effect on the formula (unit propagation). This process suffers from the same problem as the 2nd strategy --- how are a set of values chosen to maximise unit propagation on the set? In this case, the number of possible partitions is reduced due to the restriction that one partition must consist of a single value, but the problem of optimising unit propagation on values sets still remains. This method is very similar to how the Boolean search operates on the unary translation, by exploring a single value at a time. It also has the same disadvantages, namely that there is little simplification that can be done in the partial-commitment subtree. The 1st method does not suffer from this complexity, but more commitment is given than may be necessary. For example, if choosing X \mapsto a produces a similar subtree as choosing X \mapsto b, then redundant work can be avoided by choosing X \mapsto {a,b}. This method may do more work than is necessary, but it's effectiveness does not depend on a difficult set partitioning decision. For this reason I chose to implement the 1st branching strategy. 3.1.2 Assumptions I assume that all input formulas are positive, i.e. negative formulas are translated to equivalent positive formulas (see page \pageref{Translating negative literals}). This is done to simplify the implementation and does not restrict the range of formulas that the non-Boolean search can operate on, although it may increase their size. Of course, when translating to a Boolean equivalent, the most efficient representation is used (i.e. graph colouring formulas are expressed as negative formulas, then translated). I also assume that all clauses in the input formula contain at most one occurrence of each variable. If this is not the case, clauses can be re-written to obey this restriction. X\in A \vee X\in B \vee \alpha \equiv X\in (A\cup B) \vee \alpha 3.1.3 Abstract definition of non-Boolean unit propagation I first present an abstract definition of non-Boolean unit propagation, which sets the scene for the more procedural explanation of the whole NB procedure. For a non-Boolean unit clause X\in A, all clauses X\in B \vee \alpha are re-written according to the following rules: 1. If A \cap B = {} then replace X\in B \vee \alpha with \alpha . 2. If A \subseteq B then remove X\in B \vee \alpha form the formula. 3. If A \supset B then leave X\in B \vee \alpha as it is. 4. Otherwise replace X\in B \vee \alpha with X\in (A\cap B) \vee \alpha . 3.1.4 Definition of the non-Boolean Davis-Putnam method The Boolean method described on page \pageref{Boolean Davis-Putnam} can be expanded to give the outline of the non-Boolean procedure. It is assumed that all variables have value domains D([footnote] This may not be true in the general case, but this assumption allows optimisations to be made in the implementation. Extra clauses can be used to constrain the domain of variables if necessary, for variable-specific domains.) . function NB_Davis-Putnam(formula f) return Boolean is /* unit propagation */ repeat for each unit clause l in f do let l=X\in \{a_{1},a_{2},\ldots ,a_{n}\} for all values a\in D\setminus \{a_{1},a_{2},\ldots ,a_{n}\} replace all literals X\in \{a,b_{1},b_{2},\ldots ,b_{n}\} that appear in f with X\in \{b_{1},b_{2},\ldots ,b_{n}\} end for remove from f all clauses that contain the literal X\in \{a_{1},a_{2},\ldots ,a_{n}\} remove X\in \{\} from all clauses in f in which it appears end for if f is empty then return True else if f contains the empty clause then return False end if until there are no unit clauses in f /* pure literal elimination */ for all variables X whose occurrences in f all have the value a in their value set do remove from f all clauses that contain X end for /* branching */ pick a variable X from f for all values a that X appears with in f do if NB_Davis-Putnam(f\wedge X\in \{a\}) then return True end if end for return False end function \label{Non-Boolean Davis-Putnam} Again, the current assignment is kept track of, so the procedure can return a satisfying assignment if the formula is found to be satisfiable. 3.1.5 An example of non-Boolean Davis-Putnam As an example we use the previous graph colouring problem, re-written using only positive literals, for simplicity. f_{0}= (X\in {g,b}\vee Y\in {g,b}) \wedge (X\in {r,b}\vee Y\in {r,b}) \wedge (X\in {r,g}\vee Y\in {r,g}) \wedge (X\in {g,b}\vee Z\in {g,b}) \wedge (X\in {r,b}\vee Z\in {r,b}) \wedge (X\in {r,g}\vee Z\in {r,g}) \wedge (Y\in {g,b}\vee Z\in {g,b}) \wedge (Y\in {r,b}\vee Z\in {r,b}) \wedge (Y\in {r,g}\vee Z\in {r,g}) A_{0}= {} There are no unit clauses so unit propagation cannot take place. Suppose X is chosen to branch on. Then we have the choices X \mapsto r, X \mapsto g and X \mapsto b. Suppose X \mapsto r is explored first. X \mapsto r f_{1}= (F\vee Y\in {g,b}) \wedge (T\vee Y\in {r,b}) \wedge (T\vee Y\in {r,g}) \wedge (F\vee Z\in {g,b}) \wedge (T\vee Z\in {r,b}) \wedge (T\vee Z\in {r,g}) \wedge (Y\in {g,b}\vee Z\in {g,b}) \wedge (Y\in {r,b}\vee Z\in {r,b}) \wedge (Y\in {r,g}\vee Z\in {r,g}) f_{1}= (Y\in {g,b}) \wedge (Z\in {g,b}) \wedge (Y\in {g,b}\vee Z\in {g,b}) \wedge (Y\in {r,b}\vee Z\in {r,b}) \wedge (Y\in {r,g}\vee Z\in {r,g}) A_{1}= {X\mapsto r} Unit propagation now forces Y \mapsto {g,b} and Z \mapsto {g,b}. Y \mapsto {g,b} Z \mapsto {g,b} f_{2}= (Y\in {g,b}) \wedge (Z\in {g,b}) \wedge (Y\in {g,b}\vee Z\in {g,b}) \wedge (Y\in {b}\vee Z\in {b}) \wedge (Y\in {g}\vee Z\in {g}) f_{2}= T \wedge T \wedge (T\vee T) \wedge (Y\in {b}\vee Z\in {b}) \wedge (Y\in {g}\vee Z\in {g}) f_{2}= (Y\in {b}\vee Z\in {b}) \wedge (Y\in {g}\vee Z\in {g}) A_{2}= {X\mapsto r, Y\mapsto {g,b}, Z\mapsto {g,b}} There is now the choice of branching on Y or Z. Suppose Y is chosen. Only the branches Y \mapsto g and Y \mapsto b need to be explored since Y \mapsto r was eliminated by the unit propagation step. Suppose Y \mapsto g was chosen. Y \mapsto g f_{3}= (F\vee Z\in {b}) \wedge (T\vee Z\in {g}) f_{3}= Z\in {b} A_{3}= {X\mapsto r, Y\mapsto g, Z\mapsto {g,b}} Finally, unit propagation forces Z \mapsto b. Z \mapsto b f_{4}= T f_{4}= empty formula A_{4}= {X\mapsto r, Y\mapsto g, Z\mapsto b} The empty formula has been found, therefore the formula is satisfied by the assignment A_{4}. \resizebox*{0.8\textwidth}{1in}{\rotatebox{270}{\includegraphics{tree2.eps}}} The non-Boolean search tree, showing the variable and value assignments at each branch. \resizebox*{0.8\textwidth}{3in}{\rotatebox{270}{\includegraphics{tree3.eps}}} The search tree of the unary Boolean translation (with assignments omitted from some branches). The potential search space of the translation is much larger (due to non-singular assignments), although not all of it will be explored, as described on page \pageref{Effect of ALO and AMO clauses}. The non-Boolean search tree is flatter, because each branch represents a larger commitment, as previously discussed. 3.1.6 Variable and value order The variable ordering heuristic has the same function as in the Boolean procedure, and I conjecture that it has the same critical effect on it's efficiency. Both the moms and the UP heuristics can be generalised to operate on the non-Boolean search. As in the Boolean procedure, the value order has no effect on the efficiency of the search on unsatisfiable formulas. 3.2 Implementation The first decision regarding the design was to select a suitable Boolean Davis-Putnam SAT solver on which to base the non-Boolean version. It would, of course, be possible to write the non-Boolean version from scratch but this would require significantly more effort and would be repeating work which has already been done. Many highly-optimised Boolean versions have publicly available source code. SATLIB([footnote] http://www.informatik.tu-darmstadt.de/AI/SATLIB) provides source code for six Davis-Putnam based solvers: grasp, ntab, POSIT, rel_sat, SATO and satz. Of these, POSIT has the best documentation in Freeman's thesis \cite{Freeman}. In \cite{SATO}, SATO is compared against grasp, POSIT and ntab and is shown to perform well on a variety of problems. Satz (described in \cite{Satz}) is a relatively new program and was written in the same year as this paper was published (I assume that is why it was not included). When I conducted tests of SATO against satz on the same publicly-available problems as in \cite{SATO}, I found that satz performed well([footnote] The problems marked * particularly suit dependency-directed backtracking. The performances marked ** are particularly bad on a single instance.) . +--------------+--------------------------------------+ |Problem class | Av|erage run t|ime (seconds) | | | POSIT | SATO | satz | +--------------+-------------+----------+-------------+ +--------------+-------------+----------+-------------+ | aim-50 | 0.04 | 0.01 | 0.83 | +--------------+-------------+----------+-------------+ | aim-100 | 34.90 | 0.02 | 0.21 | +--------------+-------------+----------+-------------+ | aim-200 | >5000.00 | 0.06 | 0.25 | +--------------+-------------+----------+-------------+ | bf | >5000.00 | 0.97 | 5.20 | +--------------+-------------+----------+-------------+ | dubois* | >5000.00 | 0.03 | >5000.00 | +--------------+-------------+----------+-------------+ | hanoi | >5000.00 | >5000.00 | >5000.00 | +--------------+-------------+----------+-------------+ | hole | 149.17 | 141.83 | 87.21 | +--------------+-------------+----------+-------------+ | ii8 | 1.19 | 0.08 | 0.56 | +--------------+-------------+----------+-------------+ | ii16 | ** >5000.00 | 0.64 | 16.68 | +--------------+-------------+----------+-------------+ | ii32 | 42.75 | 0.96 | ** >5000.00 | +--------------+-------------+----------+-------------+ | jnh | 0.10 | 0.06 | 0.33 | +--------------+-------------+----------+-------------+ | par8 | 0.10 | 0.03 | 0.11 | +--------------+-------------+----------+-------------+ | par16 | 5.72 | 77.06 | 27.61 | +--------------+-------------+----------+-------------+ | pret* | >5000.00 | 0.62 | >5000.00 | +--------------+-------------+----------+-------------+ | ssa | 11.39 | 0.64 | 187.02 | +--------------+-------------+----------+-------------+ SATO's trie data structures (described in \cite{SATO tries}) did not seem to be easily generalisable to handle non-Boolean formulas, and it's dependency-directed backtracking adds a further layer of complexity to the program. On the other hand, the simpler array-based implementations of other solvers are quite easily generalisable. I chose to base my NB solver on satz because I felt that the benefit of it's simplicity outweighed the performance gain from using SATO. Satz is written in 1500 lines of ANSI C code, which is convenient and relatively small compared to some other solvers. 3.2.1 Satz Satz has a fairly straightforward array- and stack-based implementation. There are two parts of the internal representation, one which remains static throughout the search and one which changes (dynamic). For the formula (a \vee b \vee \neg c) \wedge (\neg b \vee c) \wedge (\neg a \vee \neg c) \wedge a, the initial state of the data structures is depicted below. \resizebox*{0.9\columnwidth}{!}{\rotatebox{270}{\includegraphics{satz.eps}}} This shows the main data structures, the other parts (such as storing for each variable the current value and unexplored value) are not so important for explaining the operation of the program. The internal representation uses integers to represent variables and clauses; this allows efficient indexing. The static part of the data structure does not change throughout the search, the changes in the state of the formula are flagged in the dynamic part. This reduces the amount of data that needs to be updated during the search and thus reduces the amount necessary to be stored for backtracking. * The formula is stored in the sat array. It is an array of clauses, each clause is an array of literals. * The pos_in and neg_in arrays hold, for each variable, the clauses in which it occurs positively (pos_in) and negatively (neg_in). They allow efficient simplification of the formula after a variable assignment. * The clause_length array holds the current length of each clause. * The clause_state array holds the states of each clause. A clause is DEAD if it has been removed from the formula (i.e. it is True), otherwise it is LIVE. * The var_state array holds the states of each variable. A variable is DEAD if it has been assigned a value, otherwise it is LIVE. The length of each clause is kept up-to-date during the search, which allows unit clauses to be identified quickly (for efficient implementation of unit propagation). The four stacks hold integer values, corresponding to the variables/clauses that are stored. They are used to store and recall data, to allow efficient backtracking. * When a variable is assigned a value, the variable is pushed onto the variable_stack. * When a clause has been removed from the formula (i.e. it evaluates to True), it is pushed onto the clause_stack. * When a clause has a literal removed from it (i.e. the literal is False) and the resulting clause is non-unit, it is pushed onto the managedclause_stack. If a clause has had two literals removed, it will have two occurrences in the managedclause_stack. * When a clause has a literal removed from it and the resulting clause is unit (i.e. the clause length is 1), it is pushed onto the unitclause_stack ([footnote] Initially, the unitclause_stack contains the unit clauses present in the input formula.) . The heuristic used by satz is a restricted UP heuristic, as described earlier. This requires additional data structures for the lookahead, but these have been omitted from the explanation for clarity --- they only affect the heuristic, and are irrelevant to the rest of the procedure. Variable assignment and backtracking in satz When an active variable x is assigned True, all active clauses that x occurs positively in are removed and all active clauses that x occurs negatively in have \neg x removed from them. What this amounts to is the following: 1. Set var_state[x]:=DEAD. 2. Push x onto variable_stack. 3. For all clauses c from pos_in[x], if clause_state[c]=LIVE then set clause_state[c]:=DEAD and push c onto clause_stack. 4. For all clauses c from neg_in[x], if clause_state[c]=LIVE then set clause_length[c]:=clause_length[c]-1. If clause_length[c]=0 then backtrack, if clause_length[c]=1 then push c onto unitclause_stack, otherwise push c onto managedclause_stack. The treatment of assigning a variable False is analogous. Discriminating between unit and non-unit clauses at this stage improves the efficiency of unit propagation. The process backtracks by simply undoing the variable assignments. 1. For all variables x on variable_stack up to the backtracking point, set var_state[x]:=LIVE. 2. For all clauses c on clause_stack up to the backtracking point, set clause_state[c]:=LIVE. 3. For all clauses c on managedclause_stack up to the backtracking point, set clause_length[c]:=clause_length[c]+1. 4. For all clauses c on unitclause_stack up to the backtracking point, set clause_length[c]:=clause_length[c]+1. The formula has been satisfied if all clauses have been satisfied (i.e. the clause_stack is full), it is unsatisfiable if the search backtracks past the first branch (i.e. the variable_stack is empty). Unit propagation is simply a case of finding the only remaining active (LIVE) literal in each clause in the unitclause_stack and assigning it's underlying variable True if it is positive and False if it is negative. The heuristic The heuristic is implemented with the same operation for assigning variables as detailed above. It effectively explores (to the next level of depth) the subtrees which would result from branching on certain variables. There are separate stacks for variables assigned, shortened non-unit clauses and shortened unit clauses --- this is done to maintain a ``tentative'' state for each variable examined, which can be reset quickly. 3.2.2 NB-satz The non-Boolean procedure described on page \pageref{Non-Boolean Davis-Putnam} differs from the Boolean one in a number of features. 1. The domain size is not known at compile-time, so the data structures must not be domain size specific (e.g. pos_in and neg_in from the Boolean implementation). 2. Each literal may have an arbitrary value set (limited in size by the domain). 3. Individual literals must be able to be eliminated from the formula. This contrasts to removing all literals l and all clauses \overline{l}\vee \alpha , as in the Boolean procedure. The first two points are relatively trivial to implement and do not pose a problem, although the third is not so easy to implement efficiently. This contrasts heavily to the Boolean implementation where a single flag for each variable was sufficient (var_state). This point is discussed later. The same basic data structures as satz are used, but extra ones are introduced to follow the procedure on page \pageref{Non-Boolean Davis-Putnam}. The static representation is altered to allow efficient indexing, with pointers to literals being used instead of array indices. Two new stacks are introduced to hold restricted value sets (restrictedlit_stack) and individual literals eliminated from the formula (removedlit_stack). For the formula (A\in {1} \vee B\in {2}) \wedge (A\in {2} \vee B\in {1,3}), the initial state of the data structures is shown below. \resizebox*{0.9\textwidth}{!}{\rotatebox{270}{\includegraphics{NB-satz.eps}}} Each entry in the sat array is now a 4-tuple, holding the variable, it's value set, the clause it occurs in and the individual literal state --- the only part of the sat data structure that is dynamic. The operation of the dynamic part of NB-satz is identical in operation to that in satz, except for the addition of lit_state, restrictedlit_stack, removedlit_stack and the addition of individual literal states. The value set for a particular variable is restricted by flagging it's state in the lit_state array, similarly to how a clause is removed. Each of these restrictions is pushed on the restrictedlit_stack, so that they can be restored when backtracking. Individual literals are removed by setting their state and pushing the literal pointer (address) onto the removedlit_stack (for backtracking). The individual literal state is necessary from requirement 3 above. Although these three data structures for the states of literals create redundancy (var_state, lit_state and the individual literal state), having all three improves time efficiency. Since the procedure is operating on individual literals, it is necessary to have the pos_in/neg_in arrays replaced by ones that index individual literals rather than clauses (as in the Boolean implementation). Some operations still operate on clauses, so each literal also stores it's clause. The extra array ``lits_with_var'' is used for unit propagation. Variable assignment and backtracking in NB-satz When an active variable X is assigned the value a, all active clauses that contain X\in {a,\ldots{}} are removed. All other active clauses that contain the literal X\in {\ldots{}} have X\in {\ldots{}} removed from them. 1. Set var_state[X]:=DEAD. 2. Push X onto variable_stack. 3. For all clauses c from lits_with_var_with_val[X][a]->clause, if clause_state[c]=LIVE then set clause_state[c]:=DEAD and push c onto clause_stack. 4. For all clauses c from lits_with_var_without_val[X][a]->clause, if clause_state[c]=LIVE then set clause_length[c]:=clause_length[c]-1. If clause_length[c]=0 then backtrack, if clause_length[c]=1 then push c onto unitclause_stack, otherwise push c onto managedclause_stack. As before, the process backtracks by simply undoing the variable assignments. 1. For all variables X on variable_stack up to the backtracking point, set var_state[X]:=LIVE. 2. For all clauses c on clause_stack up to the backtracking point, set clause_state[c]:=LIVE. 3. For all clauses c on managedclause_stack up to the backtracking point, set clause_length[c]:=clause_length[c]+1. 4. For all clauses c on unitclause_stack up to the backtracking point, set clause_length[c]:=clause_length[c]+1. At each branch in the search, only the subtrees corresponding to currently active values are explored (i.e. for the variable X with active values {a_{1},a_{2},\ldots{}a_{n}} and inactive values {b_{1},b_{2},\ldots{}b_{n}}, only X \mapsto {a_{1}}, X \mapsto {a_{2}}, \ldots{}, X \mapsto {a_{n}} are explored). Unit propagation Unit propagation is not as simple as in the Boolean procedure, since it may entail a partial assignment. Each active unit clause X\in {a_{1},a_{2},a_{3},\ldots{}} in the unitclause_stack is propagated by the following method. 1. For all values a \in (D\setminus {a_{1},a_{2},a_{3},\ldots{},a_{n}}), if lit_state[X][a]=LIVE then set lit_state[X][a]:=DEAD and push (X,a) onto restrictedlit_stack. 2. For all literals l in lits_with_var[X], if l->state=LIVE and clause_state[l->clause]=LIVE then: (a) Let c=l->clause. (b) If l={a_{1},a_{2},a_{3},\ldots{},a_{n}} then set clause_state[c]:=DEAD, push c onto clause_stack. (c) If l={} then set l->state:=DEAD and push l onto removedlit_stack. Set clause_length[c]:=clause_length[c]-1. If clause_length[c]=0 then backtrack, if clause_length[c]=1 then push c onto unitclause_stack, otherwise push c onto managedclause_stack. The internal representation of literals All literals are internally represented positively. This can be inefficient if the formula is most concisely expressed using negative literals (e.g. graph colouring problems), because the internal data structures are larger and more state needs to be maintained during the search. The Boolean translation can have a more compact representation and avoid this problem to an extent, because the more concise translation can be used (see page \pageref{Translating negative literals}). Non-Boolean heuristics In the chosen branching method, the number of branches at each node increases with domain size (each node has more subtrees). Because of this, if the ``goodness'' of a branch is determined by it's worst subtree, this has a negative effect on the NB procedure. By grouping more sub-searches into one branching point, the best branch is less likely to be very much better than an average branch. This affects the choice of variable ordering heuristic --- if the best branch is not much better than a good one, a heuristic that is rough but quick may outperform a more accurate but slower one. For this reason, I implemented a version of NB-satz with the moms heuristic as well as one with the UP heuristic. Let n_{2}(l) be the number of times literal l occurs in binary clauses n_{3}(l) be the number of times literal l occurs in ternary clauses w(l)=(5\times n_{2}(l))+n_{3}(l) The basic non-Boolean moms heuristic is a straightforward generalisation of the Boolean balanced and weighted version. Over all active variables X, with active values a_{1},a_{2},\ldots a_{n}, the basic moms heuristic selects the variable X which maximises min\left( w(X\in \{a_{1},\ldots \}),w(X\in \{a_{2},\ldots \}),\ldots ,w(X\in \{a_{n},\ldots \})\right) . Recall that for each variable examined, the UP lookahead step explores the effects of assigning all active values to that variable. The chosen NB branching method therefore forces the cost of examining a single variable to be greater as domain size increases. Combined with the previous point (the best branch is not much better than a good one), this reduces the efficiency of the UP heuristic. The lookahead step is easily generalised; a variable X with active values \{a_{1},a_{2},\ldots ,a_{n}\} in a formula f is examined by the following procedure: * The formula p_{k} is obtained by performing unit propagation on f\wedge X\in \{a_{k}\}. * The individual weights of each X\mapsto k are given by w(X\mapsto k)=diff(p_{k},f), where diff(a,b) is the number of clauses that are shorter in a than in b. * The overall weight given to the variable is H(X)=\frac{1}{k}\Sigma ^{k}_{i=1}w(X\mapsto k). I found that this weight function performed better than the straight generalisation of Freeman's weight function, which is H(X)=1024\times \Pi ^{k}_{i=1}w(X\mapsto k)+\Sigma ^{k}_{i=1}w(X\mapsto k), which ignores the number of active values. I dropped the \Pi term because it didn't improve the heuristic (it is unlikely to be significant for large domains, since at least one branch is likely to be poor). I added the \frac{1}{k} factor because it alters H(X) to favour smaller sets of active values --- this produced the largest performance gain I could obtain from tweaking the UP heuristic. This non-Boolean generalisation of the UP heuristic was less effective on increasing domain sizes. To try to decrease the search time, I tried to restrict it in the same way as is done with the Boolean version. I kept the same concept, but generalised it to be ``at least i occurrences, at least j with each active value''. For various domain sizes, I tried various values for i and j, but for larger domains, I did not observe performance gains such as those seen in the Boolean procedure \cite{Satz}. After looking at the search trees and the number of variables examined at each node, I thought of a more relaxed restriction method: ``at least i occurrences, at least j with each value from a subset of k active values''. I tried many values for i, j and k for various domain sizes but could not find any restrictions that performed better than the pure UP heuristic (unrestricted) on large domains (size > 4). The implementation used for testing uses the pure UP heuristic. I conducted these tests on random formulas, as in \cite{Satz}. Refining the moms heuristic The moms heuristic attempts to select the most constrained variable based on syntactic analysis of the formula. The Boolean procedure considers the number of occurrences of each variable and the size of the clauses they occur in (and attempts to maximise the number of occurrences and minimise clause size). The non-Boolean procedure introduces another varying factor --- the size of the value set. The unit propagation step can be applied to any literal, regardless of the size of it's value set. Although a unit clause containing a literal with a large value set may actually produce more unit propagation than one with a smaller value set, it is less likely to do so (variables with smaller value sets are intuitively more tightly constrained). It is the task of the heuristic to estimate the effect of branching on a particular variable, so this estimation should take into account the value set size of literals. Implementing this idea is non-trivial because the value set size of each literal in the formula must be known. Whether this is maintained during the search or determined each time the heuristic is called, the time overhead is quite significant. A more feasible method is to consider the number of active values associated with each variable (i.e. the lit_state is LIVE), which requires time dependent on the number of variables and values, not the formula size. This is a rougher estimate, but can be computed quickly. Let n_{2}(l) be the number of times literal l occurs in binary clauses n_{3}(l) be the number of times literal l occurs in ternary clauses w(l)=(5\times n_{2}(l))+n_{3}(l) Over all active variables X, with active values a_{1},a_{2},\ldots a_{n}, the refined moms heuristic selects the variable X which maximises \frac{1}{n}\left[ min\left( w(X\in \{a_{1},\ldots \}),w(X\in \{a_{2},\ldots \}),\ldots ,w(X\in \{a_{n},\ldots \})\right) \right] . This favours variables with smaller sets of active values. I found that this performed better than the basic moms heuristic, and reduced the average search time by a factor of about 20% on hard random 3-SAT formulas. Other points A literal with n values is internally represented as a variable and a value set comprising n values; an alternative to this is to represent it as n variable-value pairs. This implementation makes the unit propagation step very difficult, because the clause length can no longer be used to indicate a unit clause. Eliminating a clause X\in {a_{1},a_{2},\ldots{},a_{n}} \vee \ldots{} because {a_{1},a_{2},\ldots{},a_{n}} is equal to the current partial assignment of X (part of the unit propagation step) also becomes difficult. The non-Boolean unit propagation step is fundamentally different from the Boolean unit propagation step, with respect to the implementation. If the clause X\in {a,b,c} is propagated, the literal X\in {c,d} will be removed, but X\in {a,b} will not. Therefore each individual literal must be able to be removed from the formula, independent of all other literals. This can be achieved two ways: either keep a state for each variable-value pair, or keep a state for every literal in the formula --- NB-satz does both of these, for time efficiency. The state of each variable-value pair (lit_state) is necessary so that the active values (those which need to be explored at each branch) can be determined quickly. The non-Boolean procedure could have been implemented without the individual literal state, but then the state of each literal (often required to be known in the procedure) would only be able to be determined performing many comparisons between the literal's value set and the states of each variable-value pair. My chosen implementation method sacrifices increased memory (and state) for a faster search. The non-Boolean UP heuristic does not discriminate between a unit propagation that assigns X \mapsto {a} and one that assigns X \mapsto {a,b}. This is a potential weakness --- the former is intuitively more preferable since it eliminates a variable from the formula. 3.3 Program verification For the verification, I assumed that satz was correctly implemented and always gives the correct solution (satisfiable or unsatisfiable). The first task was to show that NB-satz agreed with satz as to whether a formula is satisfiable or unsatisfiable. To do this I repeatedly generated a random non-Boolean formula, solved it with NB-satz and solved it's Boolean translation with satz. A simple batch file did this and halted if they gave a different result. I chose to repeat this procedure using hard([footnote] Generated at the phase transition, explained later.) random formulas over a number of domain sizes and formula sizes, to maximise the chance of finding a discrepancy. After a few thousand iterations no discrepancy was found. Both the moms implementation and the UP implementation were tested in this manner, which further increased my confidence in a correct implementation. If NB-satz and satz had the same behaviour on formulas with domain size 2, this would aid verification immensely since both searches could be traced and compared --- it would be extremely unlikely that there there was an error if both searches were the same. Since it was not possible for me to find an efficient restriction on the unit propagation heuristic, the original implementation of satz could not be directly compared to NB-satz in this way (either the moms or the UP implementation) because the different heuristic would produce a different variable ordering. I decided that this was a valuable test so I adapted satz to use the same moms heuristic as in NB-satz and found that both produced the same search on all formulas I tested them on. A small thing that confused me was that initially it gave the same results (i.e. number of branches, backtracks etc.) for unsatisfiable formulas but not the same search, while for satisfiable formulas neither the results or the search was always the same. I then realised that the converter used the binary encoding X\in {0} = \neg x and X\in {1} = x, and that the Boolean value order (T first, then F) was opposite to how I implemented it in NB-satz (0, 1, 2, \ldots{}). When I reversed the value order in satz, all the searches and solutions were identical. The UP implementation of NB-satz differs from the moms version only in the heuristic (the variable order), so these tests gave me confidence that both were correct. When a formula is determined to be satisfiable, the solution is checked by a simple procedure that puts the values found back into the formula and tests if all clauses are satisfied, an error message appears if this is not so. This simple step ensures that all satisfying assignments output by the program actually satisfy the formula (i.e. it confirms the validity of each solution produced). The program never produced a ``duff'' assignment on any of it's runs. Of course all these tests are necessary but not sufficient to show a valid implementation, i.e. they do not prove that NB-satz is correct. 3.4 Program evaluation To evaluate the performance of NB-satz, it has to be tested on a number of formulas. Obviously a wide range of test formulas would be good, to give as much information as possible, but the formulas should be related (controlled) in some way, so as to enable conclusions to be drawn from the data. I based the decision of which problems to use as a test on these requirements. 3.4.1 Randomly generated formulas Many SAT search procedures are tested on randomly generated formulas because they can be easily generated and with a high degree of control. The number of variables, number of clauses and the domain size can be varied, and the formulas can be generated in such a way so that they are hard to solve (few solutions). There are disadvantages though --- the formulas do not relate to the encoding of any real-world problems (whose formulas may be very different) and they are all similar in structure. This controllable similarity can be a good thing for benchmarking, but a SAT solver is not of practical use if it only performs well on random formulas. Boolean random SAT formulas are commonly generated using the constant clause length model (k literals per clause --- called k-SAT). Each clause in a k-SAT formula is generated by choosing k distinct variables at random from the set of variables, and negating them with probability \frac{1}{2}. Random 3-SAT is usually used to test solvers because it is NP-complete. Non-Boolean random formulas are generated in a similar way, but a constant literal set size is imposed. A NB (k,l)-SAT clause is generated by picking k distinct variables at random, and l distinct values at random for each of the variables. Frisch and Peugniez \cite{NB-walksat} use the model where l is equal to half the domain size. This stays true to the Boolean random formula model when the domain size is two. I chose this method (as opposed to l=1 for instance) because it puts a relatively equal constraint on each variable, independent of domain size. Examples of literals generated in this way are given below. | | Domain = {1,2} | Domain = {1,2,3,4} | Domain = {1,2,3,4,5,6,7,8} ---------------+--------------------+---------------------------- ---------------+--------------------+---------------------------- A\in {1} | A\in {1,2} | A\in {3,4,6,8} B\in {2} | B\in {2,3} | B\in {1,4,5,7} C\in {1} | C\in {2,4} | C\in {2,3,5,7} D\in {1} | D\in {1,4} | D\in {1,2,5,6} The phase transition in random formulas In 1979, Goldberg \cite{Goldberg} showed that the Davis-Putnam procedure ran in polynomial time in the average case. He was using randomly generated formulas, but these were easy to solve, as shown by Franco and Paull in 1983 in \cite{Franco and Paull}. Around this time, there was an intellectual awakening regarding the phase transition in SAT. Taking the ratio of clauses to variables (c/v) as a measurement, the satisfiable and unsatisfiable problems can be grouped. The satisfiable formulas tend to occur with low values of c/v, the unsatisfiable ones tend to occur with a higher c/v ratio. If we keep v constant and generate a number of random formulas with varying c, this behaviour can be explained. The formulas with few clauses (low c/v) are under-constrained --- many assignments are likely to satisfy the formula because there are few clauses to be violated. Likewise, formulas with many clauses (high c/v) are over-constrained and most assignments violate at least one clause, since there are more to violate. The graph below shows the trend of satisfiability against c/v. The phase transition is the region of the curve where the percentage of formulas satisfiable goes from very high to very low. It is described as a phase transition because it mimics the knife-edge characteristics of many natural phenomenon such as water freezing. 3-SAT is the smallest k-SAT problem that is NP-complete \cite{Cook}, so is commonly used to test SAT solvers. The phase transition in 3-SAT has been studied much and the point where 50% of the formulas generated are satisfiable occurs at around c/v = 4.3. \resizebox*{0.8\textwidth}{!}{\rotatebox{270}{\includegraphics{phase.eps}}} As the ratio of clauses to variables changes, the amount of computational effort required to solve the formulas changes. For under-constrained formulas, the tree holds many solutions and one is quickly found, so not much of the tree actually needs to be explored. For over-constrained formulas, many contradictions are found early in the search, so much of the tree can be pruned away. The most difficult formulas for the Davis-Putnam method occur at the phase transition, where the formulas are only just satisfiable or very nearly satisfiable. For these formulas there are not many solutions, if any, so the search cannot stop early. Nor can it prune away much of the tree because there are no contradictions high in the tree. It is widely accepted that random formulas used for testing SAT solvers should be generated at the phase transition, as they are the more difficult problems. \resizebox*{0.8\textwidth}{!}{\rotatebox{270}{\includegraphics{phase2.eps}}} The same easy-hard-easy characteristic is shown in randomly generated non-Boolean formulas. The random formulas used to test NB-satz should be generated at the phase transition --- it was the task of early experiments to locate this point for various formula parameters. Generating formulas on the phase transition I wrote a small program which repeatedly generates random formulas (by calling another program) and solves them. Throughout this process, one of the generation parameters is systematically varied, to home in on the point where 50% are satisfiable. The number of variables is kept constant and the number of clauses is varied, as in \cite{NB-walksat}. The motivation for this is to keep the search space size constant for each domain size by choosing the number of variables in each formula; the number of clauses is then dictated by this. Search space size The size of the search space of each non-Boolean formula was kept constant for all domain sizes (the Boolean translation may, of course, increase the search space). For domain size d and v variables, the search space size is d^{v} (each of the v variables may have d values). I chose to keep d^{v}=2^{60} as these formulas are large enough to be difficult, without being too large to hamper testing. The final parameters were determined as: +------------+---------------------+-------------------+ |Domain size | Number of variables | Number of clauses | +------------+---------------------+-------------------+ +------------+---------------------+-------------------+ | 2 | 60 | 261 | +------------+---------------------+-------------------+ | 4 | 30 | 280 | +------------+---------------------+-------------------+ | 8 | 20 | 294 | +------------+---------------------+-------------------+ | 16 | 15 | 302 | +------------+---------------------+-------------------+ | 32 | 12 | 307 | +------------+---------------------+-------------------+ 3.4.2 Graph colouring Graph colouring problems were described earlier, their non-Boolean encoding is of interest because it is intrinsically non-Boolean. A number of benchmarks are available from various sources, including the DIMACS([footnote] http://dimacs.rutgers.edu/Challenges) web site. These are not entirely ideal for testing NB-satz because they are mainly too large, and the problems which differ in domain size (number of colours) also differ in other aspects. Control over the steps in domain size would be an advantage, to allow an even spread of problems, therefore I considered generating my own graphs. Randomly generated graph colouring problems When a graph colouring problem is translated into a satisfiability problem (Boolean or non-Boolean), the number of colours to be used must be specified. The problem is then not to colour the graph in the smallest number of colours, but to determine whether it can be coloured with k colours. To ensure a non-trivial problem, k must be set to the minimal number of colours for each graph. Therefore the minimal colouring number needs to be known before the translation to SAT. An iterative approach using the Davis-Putnam procedure was used to find the minimal number of colours, but this was a little awkward, because the Davis-Putnam procedure takes much longer to terminate on unsatisfiable graph colouring formulas than satisfiable ones. For any graph, the search only needs to explore one subtree of the root node, since the first commitment (choice of node and colour) can never commit to a tree devoid of a solution. For unsatisfiable graph colouring problems, the Davis-Putnam search does much unnecessary work and actually explores all colours for the first choice of node. I attempted to use a special-purpose graph-colouring algorithm to determine the minimal colouring, but the only ones I could find were incomplete and could not guarantee that the colouring they produced was minimal. I was therefore confined to generating smaller graphs than I would have liked, since determining the minimal number of colours was time-consuming using Davis-Putnam. I decided to generate graphs with randomly assigned edges, other methods (e.g. the k-colourable method) can tend to generate ``easy'' graphs. I used Joe Culberson's quasi-random graph generator([footnote] http://web.cs.ualberta.ca/~joe/Coloring/index.html) because it is simple to use and outputs graphs in the DIMACS format --- readable by the program which translates them into SAT problems. I kept the number of nodes constant at 30 and varied the number of edges (the sparsity/density of the graph), therefore altering the minimal colouring. For the tests, I selected a number of graphs with a range of domain sizes (minimal number of colours). I chose not to use any unsatisfiable graph colouring problems because the DP search is very inefficient for these, particularly on larger domain sizes (the reason for this is detailed above). Benchmark problems Most of the available graph colouring benchmarks are too large to solve feasibly (either with NB-satz or satz). The smaller graphs consist of randomly generated graphs, n-queens problems represented as graphs, geographical graphs and book graphs. The geographical graphs represent American cities --- if two cities (nodes in the graph) are within k miles of each other then there is an edge between them. The collection is made up from the same set of cities for different values of k. The nodes in the book graphs are the characters in the book, edges represent two characters coming into contact with each other. The advantage of using benchmark problems is that the minimal colouring is usually known. Non-randomly generated graphs may have different structures to randomly generated graphs, so they give a wider range of test formulas. It would have been nice to have some real-world problems, such as register allocation or timetabling, but I could not find any that were suitable. I decided to test on the following benchmarks: * miles250 and miles500 * n-queens (5x5, 6x6, 7x7, 8x8) 3.4.3 Planning Planning is an important problem in computer science, and is concerned with finding a way to achieve a certain goal. The plan is decided in the context of a world modelled by it's state (e.g. the position of objects in a room) and a number of possible actions (e.g. moving a box, pushing a switch). Actions have preconditions and effects --- certain actions can only take place at certain times and all actions may affect the state of the world. The task is to find a sequence of actions that achieves the goal, or more specifically the optimal sequence of actions (the shortest plan). Planning has important practical applications. Translating a planning problem into Boolean SAT and solving with a general-purpose SAT solver has been shown to outperform specialised planning algorithms. Matthew Slack, a student at the university, is currently doing a project on translating planning problems into non-Boolean SAT (effectively a stepping-stone between the original encoding and the Boolean SAT encoding). I gave him NB-satz and he gave me a number of planning problems in the non-Boolean encoding. This is a good source of non-random formulas with which to test NB-satz. 3.4.4 Testing procedures The test problems were solved once each --- because the procedures are deterministic, they perform exactly the same search each time they are run on a problem. I collected all the results from each class of problem in a file which was then processed to generate means etc. This was done to keep all the results from each individual formula, so that they could be examined if necessary. I ran all the tests on a Silicon Graphics workstation with a 133MHz MIPS processor and 64Mb RAM. I decided to test against the Boolean solver satz, which uses an efficiently restricted UP heuristic. This is not entirely ``fair'' because both the non-Boolean procedures that I developed use inferior heuristics. I decided against testing on a dumbed-down version of satz (a version with a moms heuristic and one with a pure UP heuristic) because I felt that although this may give more comparable results, it missed the full picture --- the Boolean solver has an efficient restriction on the UP heuristic, but I failed to discover an efficient non-Boolean generalisation. I felt that this was an important disadvantage of the non-Boolean procedure and it should be reflected in the results. Results The results are presented in the following tables and graphs. I use graphs where appropriate because they show at a glance the various trends in the data and ease visualisation. The ``formulas size'' measurement follows the same convention as in \cite{NB-walksat}; the size of a non-Boolean formula is the number of values it contains (i.e. the sum of the sizes of each literal's value set), the size of a Boolean formula is the number of literals it contains. This measure is used to compare the sizes of the original non-Boolean formulas with their Boolean translation, to give an indication of the enlargement introduced by having to enforce singular assignments in the input formula. The non-Boolean graph colouring and planning formulas are measured by their most concise representation, i.e. negative literals are used where it makes the formula smaller. It should be remembered that this measure may not reflect the size of the internal data structures. The number of times the search branches and backtracks are included to indicate the size of the search tree. For domain size d, A non-Boolean branch produces \leq d subtrees, so the proportion of branches to backtracks is typically lower for larger domains. The binary encoding is only included for the graph colouring experiments; it is omitted for the others because it was unfeasible --- the size of the translated formula was extremely large. The methods tested are: non-Boolean with moms heuristic (NB moms), non-Boolean with UP heuristic (NB UP), unary translation (U), unary-binary translation (UB) and binary translation (B). 4.1 Randomly generated formulas The results from the randomly generated formulas are split up into satisfiable and unsatisfiable formulas, to highlight the differences between them. Formulas were generated at the phase transition and solved by each of the methods. Only the results for the first fifty satisfiable formulas and the first fifty unsatisfiable formulas were kept (to keep the sample size constant). These formulas were generated using the previously described method. They are all positive formulas, so the ALO clauses are not included in the U and UB translations. Both the x and y scales on the graphs are logarithmic, to increase readability. Some methods were particularly slow, so only ten formulas were tested. These are marked with *. 4.1.1 Satisfiable formulas +---------------+---------+---------+------------+------------+-------------+---------+------------+ | Problem | Method | Formula | Mean | Mean | Mean | Mean | Mean run | | | | size | branches | backtracks | unit | pure | time (sec) | +---------------+---------+---------+------------+------------+-------------+---------+------------+ +---------------+---------+---------+------------+------------+-------------+---------+------------+ |Domain size 2 | NB moms | 783 | 27.36 | 21.82 | 422.38 | 16.32 | 0.06 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 60 variables | NB UP | | 8.08 | 3.44 | 74.86 | 8.26 | 0.04 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 261 clauses | U | 903 | 10.32 | 2.50 | 164.44 | 16.48 | 0.03 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | | UB | 1023 | 10.40 | 2.34 | 248.48 | 22.98 | 0.05 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ +---------------+---------+---------+------------+------------+-------------+---------+------------+ |Domain size 4 | NB moms | 1680 | 93.12 | 133.72 | 3850.68 | 5.92 | 0.16 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 30 variables | NB UP | | 9.38 | 16.92 | 391.16 | 1.52 | 0.15 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 280 clauses | U | 2040 | 1058.94 | 557.18 | 9024.80 | 20.60 | 1.14 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | | UB | 2160 | 1228.60 | 652.96 | 18626.20 | 17.68 | 1.14 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ +---------------+---------+---------+------------+------------+-------------+---------+------------+ |Domain size 8 | NB moms | 3528 | 1102.10 | 2816.58 | 86829.24 | 2.38 | 2.13 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 20 variables | NB UP | | 43.86 | 221.52 | 7259.96 | 0.52 | 2.56 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 294 clauses | U | 4648 | 10929.06 | 5642.52 | 101305.50 | 7.24 | 48.31 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | | UB* | 4488 | 1940551.20 | 1035063.10 | 36138227.20 | 7010.20 | 2624.50 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ +---------------+---------+---------+------------+------------+-------------+---------+------------+ |Domain size 16 | NB moms | 7248 | 3940.38 | 12754.08 | 630039.62 | 0.40 | 12.00 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 15 variables | NB UP | | 123.56 | 1200.50 | 69570.32 | 0.04 | 29.18 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 302 clauses | U* | 10848 | 194440.00 | 99145.10 | 1911379.60 | 8.90 | 1736.04 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | | UB* | 8448 | --- | --- | --- | --- | >10000.00 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ +---------------+---------+---------+------------+------------+-------------+---------+------------+ |Domain size 32 | NB moms | 14736 | 9659.02 | 41231.14 | 2917633.60 | 0.28 | 53.77 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 12 variables | NB UP | | 312.86 | 5329.20 | 514793.98 | 0.12 | 240.92 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | 307 clauses | U* | 26640 | --- | --- | --- | --- | >10000.00 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ | | UB* | 18576 | --- | --- | --- | --- | >10000.00 | +---------------+---------+---------+------------+------------+-------------+---------+------------+ \resizebox*{0.95\textwidth}{!}{\rotatebox{270}{\includegraphics{graph1.ps}}} 4.1.2 Unsatisfiable formulas +---------------+---------+---------+------------+------------+-------------+----------+------------+ | Problem | Method | Formula | Mean | Mean | Mean | Mean | Mean run | | | | size | branches | backtracks | unit | pure | time (sec) | +---------------+---------+---------+------------+------------+-------------+----------+------------+ +---------------+---------+---------+------------+------------+-------------+----------+------------+ |Domain size 2 | NB moms | 783 | 44.94 | 45.94 | 817.26 | 10.90 | 0.09 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 60 variables | NB UP | | 7.66 | 8.66 | 89.92 | 3.16 | 0.05 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 261 clauses | U | 903 | 12.90 | 7.22 | 310.26 | 6.86 | 0.04 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | | UB | 1023 | 12.22 | 6.78 | 460.32 | 8.70 | 0.05 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ +---------------+---------+---------+------------+------------+-------------+----------+------------+ |Domain size 4 | NB moms | 1680 | 190.48 | 288.56 | 8305.40 | 3.94 | 0.32 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 30 variables | NB UP | | 14.16 | 39.40 | 796.82 | 0.48 | 0.28 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 280 clauses | U | 2040 | 3094.56 | 1637.52 | 26240.84 | 39.84 | 3.35 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | | UB | 2160 | 2609.58 | 1393.32 | 39062.70 | 20.86 | 2.38 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ +---------------+---------+---------+------------+------------+-------------+----------+------------+ |Domain size 8 | NB moms | 3528 | 2550.72 | 6592.32 | 205104.10 | 2.66 | 4.93 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 20 variables | NB UP | | 92.32 | 499.80 | 16240.52 | 0.16 | 5.72 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 294 clauses | U | 4648 | 25542.32 | 13204.60 | 238834.94 | 20.06 | 113.50 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | | UB* | 4488 | 5098866.40 | 2724622.80 | 94608883.20 | 18394.30 | 6848.84 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ +---------------+---------+---------+------------+------------+-------------+----------+------------+ |Domain size 16 | NB moms | 7248 | 8866.50 | 28787.58 | 1429531.70 | 0.66 | 27.06 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 15 variables | NB UP | | 274.42 | 2710.36 | 157733.88 | 0.06 | 63.77 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 302 clauses | U* | 10848 | 452363.60 | 231142.30 | 4451014.00 | 28.60 | 4151.00 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | | UB* | 8448 | --- | --- | --- | --- | >10000.00 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ +---------------+---------+---------+------------+------------+-------------+----------+------------+ |Domain size 32 | NB moms | 14736 | 26550.30 | 114463.22 | 8196184.10 | 0.14 | 150.08 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 12 variables | NB UP | | 756.08 | 13119.96 | 1293095.60 | 0.00 | 583.72 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | 307 clauses | U* | 26640 | --- | --- | --- | --- | >10000.00 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ | | UB* | 18576 | --- | --- | --- | --- | >10000.00 | +---------------+---------+---------+------------+------------+-------------+----------+------------+ \resizebox*{0.95\textwidth}{!}{\rotatebox{270}{\includegraphics{graph2.ps}}} Both the solution times and the search tree size increase for all the methods as domain size increases. This trend is also shown to occur with NB-walksat in \cite{NB-walksat}. The results for the satisfiable formulas are very close to those for the unsatisfiable formulas, except the mean run time is roughly half, corresponding to solutions lying roughly half way through the search space on average. NB moms outperforms NB UP on domain size 8 and above, although this is a ``brute-force'' win, since the search tree size (indicated by the number of branches) is clearly worse --- the heuristic is less accurate. It seems that it is not worth the time needed to work out the best([footnote] I do not suggest that the UP heuristic finds the best variable, but I mean that it does better than the moms heuristic.) branch, but a good one will do if it is found quickly. The UB translation performs particularly poorly, the growth of which is the worst of all the methods. I would suggest that this is because it introduces more variables into the translated formula. The U translation performs better than UB, but much worse than both NB moms and NB UP as domain size increases. Looking at the number of branches and backtracks for the Boolean encodings, it can be seen that they explore more of the search space. I infer from this that using the Boolean heuristic on the translation is less accurate than using the non-Boolean heuristic on the non-Boolean formula. Both NB moms and NB UP show a bump in run time in going from domain size 2 to domain size 16. It seems that these formulas increase rapidly in difficulty between around domain size 4 and 8, after which the increase is not so large. I do not have an explanation for this phenomenon but it is clearly not a coincidence because it happens with both heuristics and both satisfiable and unsatisfiable formulas. More experiments on domain sizes between 4 and 8 would be interesting and may shed light on the underlying cause. Within the program, I recorded the unit propagation with two separate counts. One holds the number of unit propagations X \mapsto {a_{1}}, one holds the unit propagations X \mapsto {a_{1},a_{2},\ldots{},a_{n}}. These are referred to as full- and semi-unit propagation, respectively. The total amount of all unit propagation is the sum of these values, the mean of which is displayed in the table. Most of the unit propagation in these formulas was semi-unit propagation. +------------+--------------------------------------+ |Domain size | (full-UP/total UP)\times domain size | +------------+--------------------+-----------------+ | | NB moms | NB UP | +------------+--------------------+-----------------+ +------------+--------------------+-----------------+ | 4 | 0.84 | 0.68 | +------------+--------------------+-----------------+ | 8 | 0.72 | 0.32 | +------------+--------------------+-----------------+ | 16 | 0.53 | 0.16 | +------------+--------------------+-----------------+ | 32 | 0.50 | 0.11 | +------------+--------------------+-----------------+ Both NB moms and the NB UP seem to be performing worse, in terms or full-unit propagation, as domain size increases. NB UP does especially badly, suggesting that the heuristic is not putting sufficient focus on full-unit clauses. This was a concern I had at the design stage. Pure literal elimination does not occur frequently throughout the search compared to unit propagation, and it occurs less frequently as domain size increases. The average branching factor can be calculated from the unsatisfiable formulas by dividing the number of backtracks by the number of branches (actually, the formula is \frac{backtracks-1}{branches}+1). This can be done because the search backtracks up all branches for unsatisfiable formulas. +------------+---------------------------+ |Domain size | Average branching factor | +------------+--------------+------------+ | | NB moms | NB UP | +------------+--------------+------------+ +------------+--------------+------------+ | 2 | 2.00 | 2.00 | +------------+--------------+------------+ | 4 | 2.51 | 3.71 | +------------+--------------+------------+ | 8 | 3.58 | 6.40 | +------------+--------------+------------+ | 16 | 4.25 | 10.87 | +------------+--------------+------------+ | 32 | 5.31 | 18.35 | +------------+--------------+------------+ It can be seen that the average branching factor is quite a lot lower than the domain size for NB moms. This is because some values are eliminated from further inquiry before branching on a variable, either because they do not appear in the formula with that variable any more, or because the a semi-unit propagation has restricted the set of active values for that variable. NB UP has a higher average branching factor than NB moms, i.e. each branch creates more subtrees on average. Of course, these branches may be better choices (i.e. lead to a solution/contradiction more quickly) than the ones that produce less subtrees, but intuitively a lower branching factor is better. Possibly the branching factor needs more weight in the non-Boolean UP heuristic. The value of ``branches'' for the Boolean procedure does not quite fit with what I defined a branch to be; as when it finds a failed literal during a branch (and consequently sets it's value without needing to branch), it still counts it as a branch. Therefore the reported number of branches is more than the number actually carried out. Sadly, I did not have time to repeat the experiments because I noticed this too late. 4.2 Graph colouring As previously discussed, these formulas represent the minimal colouring and are all satisfiable. All these formulas are negative, so the AMO clauses are not included in the U and UB translations. 4.2.1 Randomly generated problems The table entries are marked as ``density p (q)'', where p is the specified probability of an edge occurring between 2 nodes, and q is the observed density. +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | Problem | Method | Formula | Branches | Backtracks | Unit | Pure | Run time | | | | size | | | | | (sec) | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | density 6% (4.3%) | NB moms | 76 | 3 | 0 | 19 | 8 | 0.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 30 nodes | NB up | | 3 | 0 | 19 | 8 | 0.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 19 edges | U | 136 | 3 | 0 | 41 | 16 | 0.01 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 2 colours | UB | 196 | 3 | 0 | 63 | 24 | 0.01 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 76 | 3 | 0 | 19 | 8 | 0.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ +--------------------+---------+---------+----------+------------+---------+--------+-----------+ |density 23% (24.6%) | NB moms | 856 | 10 | 9 | 202 | 8 | 0.04 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 30 nodes | NB up | | 6 | 0 | 65 | 3 | 0.12 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 107 edges | U | 976 | 13 | 4 | 333 | 23 | 0.04 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 4 colours | UB | 1216 | 6 | 0 | 147 | 15 | 0.04 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 1712 | 13 | 2 | 26 | 2 | 0.07 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ +--------------------+---------+---------+----------+------------+---------+--------+-----------+ |density 43% (40.2%) | NB moms | 2100 | 28 | 38 | 778 | 25 | 0.16 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 30 nodes | NB up | | 30 | 45 | 963 | 29 | 1.56 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 175 edges | U | 2280 | 11 | 0 | 125 | 34 | 0.08 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 6 colours | UB | 2760 | 17 | 0 | 176 | 33 | 0.11 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 5600 | 470 | 239 | 1329 | 211 | 0.94 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ +--------------------+---------+---------+----------+------------+---------+--------+-----------+ |density 62% (61.8%) | NB moms | 4304 | 52 | 84 | 1480 | 33 | 0.59 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 30 nodes | NB up | | --- | --- | --- | --- | >10000.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 269 edges | U | 4544 | 59289 | 29660 | 1455344 | 85059 | 128.19 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 8 colours | UB | 5264 | 1207 | 590 | 6073 | 1293 | 1.35 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 12912 | 330 | 152 | 264 | 0 | 2.28 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ +--------------------+---------+---------+----------+------------+---------+--------+-----------+ |density 70% (70.6%) | NB moms | 6140 | 180 | 318 | 4066 | 112 | 2.13 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 30 nodes | NB up | | --- | --- | --- | --- | >10000.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 307 edges | U | 6440 | --- | --- | --- | --- | >10000.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 10 colours | UB | 7460 | 438300 | 220045 | 1732979 | 742125 | 444.68 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 20876 | --- | --- | --- | --- | >10000.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ +--------------------+---------+---------+----------+------------+---------+--------+-----------+ |density 78% (80.5%) | NB moms | 8400 | 18 | 2 | 249 | 8 | 0.81 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 30 nodes | NB up | | --- | --- | --- | --- | >10000.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 350 edges | U | 8760 | --- | --- | --- | --- | >10000.00 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | 12 colours | UB | 10080 | 34787 | 17388 | 114755 | 33953 | 26.80 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 30800 | 1381042 | 696708 | 6278854 | 280887 | 4517.04 | +--------------------+---------+---------+----------+------------+---------+--------+-----------+ Up until domain size 6, all the methods are reasonably closely matched. At domain size 8, NB UP becomes unfeasible and U starts to show poor performance. At 10 and 12 colours, only UB and NB moms have reasonable solution times. Throughout these problems, NB moms is by far the best performing method. Unfortunately, I think that the method I used to generate the formulas made those with fewer colours too small; larger problems may have separated the methods for the smaller domain sizes. These results are particularly surprising, since the Boolean encoding is particularly concise for graph colouring problems --- the negative non-Boolean literals are represented as a single Boolean literal and the AMO clauses are not included in the unary and unary-binary translations. I would have expected better performance from the Boolean methods because these are relatively small graph colouring problems. The search tree of the UB method is similar in size to NB moms up until domain size 8. It becomes much larger at 10 and 12 colours, again indicating that the heuristic is failing. The result that NB UP so suddenly becomes inefficient is also quite intriguing. For the formulas on which NB UP terminated within 3 hours, it produced a similar sized search tree to NB moms. This suggests that the moms heuristic does not have such a lower accuracy than the UP heuristic in these formulas, although nothing can be reliably stated about the search tree size of NB UP for domain sizes 8, 10 and 12, I would not think that it is worse than that of NB moms. The UB method is the only other method that comes close to the performance of NB moms. This is surprising because the UB translation introduces more variables into the translation than the U method. Therefore it cannot be the number of variables alone that stops the U method from operating efficiently. The binary encoding (B) has good performance until domain sizes 10 and 12, where it suddenly becomes poor. For single value NB variables (e.g \neg X\in {a_{1}}), the binary translation generally produces formulas with longer clauses than the unary translation (each NB literal is translated as \left\lceil \log _{2}d\right\rceil Boolean literals). This reduces the amount of unit propagation that can occur early in the Boolean translation because unit clauses take longer to be generated during the search. The point where most methods suddenly seem to become ineffective is particularly interesting and would, in my opinion, be worth further investigation. Is it due to the increase in domain size (number of colours) or is it because of the density of the graph? Why is NB moms not affected? I would have liked to have more time to redo these tests with a set of formulas for each domain size, as this would give a better indication of the performance of the various methods. If I were to repeat them, it would be a good idea to fix the search space size (as in the randomly generated NB (3,\frac{1}{2}d)-SAT formulas) and repeatedly generate formulas, empirically determining the point where 50% are satisfiable. Unfortunately this was hampered by the poor performance of DP on unsatisfiable graph colouring problems (and the unavailability of a suitable algorithm) and the way the graph generator operated, by interactively requesting various input parameters. I did not have time to re-hash the source code to allow the generator to be systematically called from another program. 4.2.2 Benchmark problems N-queens +----------+---------+---------+----------+------------+---------+--------+-----------+ | Problem | Method | Formula | Branches | Backtracks | Unit | Pure | Run time | | | | size | | | | | (sec) | +----------+---------+---------+----------+------------+---------+--------+-----------+ +----------+---------+---------+----------+------------+---------+--------+-----------+ |n-queens | NB moms | 3200 | 6 | 0 | 86 | 0 | 0.14 | +----------+---------+---------+----------+------------+---------+--------+-----------+ |5\times 5 | NB up | | 5 | 0 | 61 | 0 | 1.37 | +----------+---------+---------+----------+------------+---------+--------+-----------+ |5 colours | U | 3325 | 5 | 0 | 96 | 9 | 0.09 | +----------+---------+---------+----------+------------+---------+--------+-----------+ | | UB | 3625 | 5 | 0 | 117 | 17 | 0.09 | +----------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 7680 | 13 | 0 | 25 | 0 | 0.31 | +----------+---------+---------+----------+------------+---------+--------+-----------+ +----------+---------+---------+----------+------------+---------+--------+-----------+ |n-queens | NB moms | 8120 | 1521 | 3278 | 68043 | 614 | 28.36 | +----------+---------+---------+----------+------------+---------+--------+-----------+ |6\times 6 | NB up | | 22 | 20 | 705 | 3 | 16.50 | +----------+---------+---------+----------+------------+---------+--------+-----------+ |7 colours | U | 8372 | 30 | 10 | 774 | 46 | 0.29 | +----------+---------+---------+----------+------------+---------+--------+-----------+ | | UB | 9092 | 253954 | 137453 | 5111813 | 371860 | 500.13 | +----------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 23200 | 2989 | 1557 | 7500 | 229 | 6.43 | +----------+---------+---------+----------+------------+---------+--------+-----------+ +----------+---------+---------+----------+------------+---------+--------+-----------+ |n-queens | NB moms | 13328 | 11747 | 29504 | 688755 | 1719 | 505.91 | +----------+---------+---------+----------+------------+---------+--------+-----------+ |7\times 7 | NB up | | 10 | 1 | 292 | 0 | 28.07 | +----------+---------+---------+----------+------------+---------+--------+-----------+ |7 colours | U | 13671 | 29 | 10 | 1075 | 37 | 0.49 | +----------+---------+---------+----------+------------+---------+--------+-----------+ | | UB | 14651 | --- | --- | --- | --- | >10000.00 | +----------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 38080 | 2118 | 1076 | 7546 | 43 | 12.03 | +----------+---------+---------+----------+------------+---------+--------+-----------+ +----------+---------+---------+----------+------------+---------+--------+-----------+ |n-queens | NB moms | 26208 | --- | --- | --- | --- | >10000.00 | +----------+---------+---------+----------+------------+---------+--------+-----------+ |8\times 8 | NB up | | --- | --- | --- | --- | >10000.00 | +----------+---------+---------+----------+------------+---------+--------+-----------+ |9 colours | U | 26784 | 3594 | 1816 | 135641 | 3548 | 7.81 | +----------+---------+---------+----------+------------+---------+--------+-----------+ | | UB | 28640 | --- | --- | --- | --- | >10000.00 | +----------+---------+---------+----------+------------+---------+--------+-----------+ | | B | 84448 | --- | --- | --- | --- | >10000.00 | +----------+---------+---------+----------+------------+---------+--------+-----------+ These formulas show a rather different trend to the random graph problems. Both NB moms and NB UP have poor performance in terms of run time; NB moms has a significantly larger search tree than NB UP on 6\times 6 and 7\times 7. The UB method is poor on all problems apart from the small one (5\times 5), B is relatively good but it is U that triumphs over all other methods in terms of run time. The search trees of the NB UP and U methods are very similar in size, but on the 6\times 6 and 7\times 7 problems, the NB UP run time is quite high --- averaging 1-3 seconds per branch. On the 8\times 8 problem, either the lookahead step is too expensive or the heuristic becomes less accurate and the search tree increases in size. The moms heuristic is not preferable to the UP heuristic on these problems --- the search tree becomes too large. These problems have quite a specific structure which may not occur in many other formulas. This may contribute to a particular method being favourable. Miles graphs +-----------+---------+---------+----------+------------+-------+------+-----------+ | Problem | Method | Formula | Branches | Backtracks | Unit | Pure | Run time | | | | size | | | | | (sec) | +-----------+---------+---------+----------+------------+-------+------+-----------+ +-----------+---------+---------+----------+------------+-------+------+-----------+ | miles250 | NB moms | 12384 | 71 | 0 | 294 | 54 | 4.49 | +-----------+---------+---------+----------+------------+-------+------+-----------+ |128 nodes | NB up | | --- | --- | --- | --- | >10000.00 | +-----------+---------+---------+----------+------------+-------+------+-----------+ |387 edges | U | 13408 | 3181 | 1552 | 21288 | 4148 | 7.13 | +-----------+---------+---------+----------+------------+-------+------+-----------+ |8 colours | UB | 16480 | 192 | 3 | 536 | 613 | 2.03 | +-----------+---------+---------+----------+------------+-------+------+-----------+ | | B | 37152 | 188 | 3 | 60 | 78 | 2.29 | +-----------+---------+---------+----------+------------+-------+------+-----------+ +-----------+---------+---------+----------+------------+-------+------+-----------+ | miles500 | NB moms | 93600 | 90 | 0 | 904 | 35 | 68.19 | +-----------+---------+---------+----------+------------+-------+------+-----------+ |128 nodes | NB up | | --- | --- | --- | --- | >10000.00 | +-----------+---------+---------+----------+------------+-------+------+-----------+ |1170 edges | U | 96160 | 96 | 0 | 786 | 1674 | 8.03 | +-----------+---------+---------+----------+------------+-------+------+-----------+ |20 colours | UB | 107424 | --- | --- | --- | --- | >10000.00 | +-----------+---------+---------+----------+------------+-------+------+-----------+ | | B | 411840 | --- | --- | --- | --- | >10000.00 | +-----------+---------+---------+----------+------------+-------+------+-----------+ The NB moms method has a very small search tree for the size of the formula, although they are very slow --- 1 branch takes nearly a second for miles500 (remember that this is the moms heuristic, so there is no lookahead). This is because the formula is very large and the setting of individual literal states required during the search takes up time. The UP heuristic cannot hope to match this because the moms heuristic is accurate on this occasion and the extra time needed to perform the lookahead makes NB UP take too long. The unary encoding (U) is the most successful method, NB moms seems to do well, but slows on miles500. The UB and B methods perform well on domain size 8 but fall down on domain size 20. Possibly the clauses become too large for B and there are too many variables for UB. From the methods that terminated within 3 hours, the figures show that there are few backtracks necessary to solve these formulas. They are relatively easy, but their large size creates difficulty. There are only two instances of these problems and they are not entirely representative of real-world problems, so they provide a limited source of information to the evaluation here. 4.3 Planning These formulas are neither positive or negative in the most concise encoding, so in general both the ALO and AMO clauses are necessary. I tried translating their positive/negative equivalents (thus excluding the ALO/AMO from the translation), but this decreased performance. All these formulas represent planning problems with the minimal number of steps needed to accomplish the plan (thus they are satisfiable). +-------------+---------+---------+----------+------------+---------+------+----------+ | Problem | Method | Formula | Branches | Backtracks | Unit | Pure | Run time | | | | size | | | | | (sec) | +-------------+---------+---------+----------+------------+---------+------+----------+ +-------------+---------+---------+----------+------------+---------+------+----------+ |6 step plan | NB moms | 3820 | 2 | 3 | 826 | 0 | 0.26 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | NB UP | | 1 | 0 | 692 | 0 | 0.36 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | U | 39532 | 1 | 0 | 1019 | 0 | 1.36 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | UB | 26203 | 1 | 0 | 909 | 53 | 1.04 | +-------------+---------+---------+----------+------------+---------+------+----------+ +-------------+---------+---------+----------+------------+---------+------+----------+ |8 step plan | NB moms | 8940 | 12 | 95 | 6168 | 0 | 1.44 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | NB UP | | 2 | 3 | 2072 | 0 | 7.10 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | U | 165740 | 6 | 3 | 6314 | 0 | 7.94 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | UB | 76364 | 3 | 0 | 3956 | 94 | 4.54 | +-------------+---------+---------+----------+------------+---------+------+----------+ +-------------+---------+---------+----------+------------+---------+------+----------+ |10 step plan | NB moms | 17754 | 201 | 2762 | 146368 | 0 | 28.18 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | NB UP | | 3 | 12 | 5250 | 0 | 120.48 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | U | 528954 | 14 | 5 | 20489 | 0 | 34.39 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | UB | 177930 | 19 | 7 | 10794 | 122 | 16.03 | +-------------+---------+---------+----------+------------+---------+------+----------+ +-------------+---------+---------+----------+------------+---------+------+----------+ |12 step plan | NB moms | 31612 | 7643 | 164852 | 8307612 | 0 | 2917.14 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | NB UP | | 7 | 193 | 32107 | 0 | 1051.44 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | U | 1400476 | 46 | 21 | 93726 | 0 | 128.29 | +-------------+---------+---------+----------+------------+---------+------+----------+ | | UB | 364516 | 177 | 88 | 46775 | 333 | 65.49 | +-------------+---------+---------+----------+------------+---------+------+----------+ \resizebox*{0.95\textwidth}{3.5in}{\rotatebox{270}{\includegraphics{graph4.ps}}} The trend in the solving methods is the opposite to that seen in the randomly generated NB (3,\frac{1}{2}d)-SAT formulas. UB is the best performing method, with a similar growth to U. NB UP performs worse on larger formulas than both U and UB, and NB moms has the poorest growth. The NB moms search tree is very large for the larger domain sizes, as the heuristic becomes less accurate (over 1000 times more branches than the NB UP search tree for the 12 step plan) --- the inaccuracy of the heuristic is what lets down NB moms. NB UP is much slower in branching than NB moms (2\frac{1}{2} minutes per branch, compared to under \frac{1}{2} second), so it is the lookahead step which is extremely slow. This is what makes NB UP slower than the corresponding Boolean translation methods. The Boolean translations perform well due to the accuracy of the heuristic and the fact that large numbers of non-Boolean literals have a single value (e.g. X\in {a_{1}} and \neg X\in {a_{2}}). These literals are concisely translated and the internal state is easily maintained throughout the search. UB performs better than U, so any negative effect of introducing extra variables is cancelled out by fewer clauses. The only pure literals are those in the UB translation; these are frequent compared to the number of branches in the search tree. These formulas are large, but solvable with relatively little backtracking by most methods apart from NB moms. Having said that, they have relatively little interdependency between actions compared to other planning problems therefore there is less unit propagation fixing the direction of the search. It would be interesting to conduct more experiments on other planning problems, especially unsatisfiable ones which may not follow the same pattern. Out of all the formulas that I tested, those representing planning problems are the only ones that could utilise variable-specific domains. I conducted tests on these same problems with a modified version of NB-satz which catered for variable-specific domains, but this showed little difference in performance. The clauses that restricted the domains of certain variables are all unit, therefore they are processed before the search begins. There are also relatively few of them (there cannot be more than the number of variables) so the loss in performance from storing them in the data structures is minimal. The non-Boolean formulas are much smaller than their Boolean translations according to the formula size measure, but the internal data structures of NB-satz are not this much smaller because all literals are stored positively. I don't think that the power of the heuristic is reduced by the ALO and AMO clauses, because these planning problems are translated including both the ALO and AMO clauses and the best performing methods are the translations --- U and UB. Although the accuracy of the heuristic is no doubt reduced with some translations, the extra clauses are not solely responsible. Conclusion 5.1 Advantages of NB-satz 5.1.1 Semi-unit propagation Probably the most significant advantage of NB-satz is that it can eliminate certain variable-value pairs from further enquiry (and in turn eliminate variables and clauses from the formula). This fixes the direction of the search where branches would otherwise be. This is a considerably valuable technique since it reduces the number of sub-problems and therefore the amount of work necessary to solve the formula. This is absent from the Boolean procedure, where the clause x_a \vee x_c would not be propagated, but the corresponding non-Boolean clause X\in {a,c} would be, and may lead to a significant amount of formula simplification. This factor is the reason why the Boolean procedure performs worse on the formulas which have many literals with large value sets (e.g. the randomly generated formulas); less unit propagation means a larger explored search space. 5.1.2 No extra clauses/variables to enforce non-singular assignments The ALO and AMO clauses in the unary translation need to be explicitly maintained during the Boolean search. This time overhead is avoided by the non-Boolean procedure, which enforces singular assignments within the algorithm. The extra clauses also make the lookahead step slower. I originally thought that the heuristic would be affected by the ALO and AMO clauses, but the results from the planning problems suggest otherwise. Those formulas are the largest which I used in testing and therefore have the largest number of ALO and AMO clauses (and many compared to the kernel formula) but the translation methods perform well, suggesting that the heuristic is not affected by the ALO and AMO clauses. Of course, this assumption cannot be proven, since this result was only observed on a number of problems taken from a single class. 5.1.3 The heuristic is not affected by problem reformulation The non-Boolean UP heuristic generally performs well in terms of search tree size (but not always in terms of time). The search tree of the Boolean Translation is significantly larger than the NB search tree on many formulas including the randomly generated graph colouring problems, suggesting that the heuristic is less accurate. Although the Boolean search does not perform semi-unit propagation, I would suggest that this may not be solely responsible for the poorer performance shown by using the translation methods. If this is so, the Boolean heuristic must in some way be adversely affected by the translation of the non-Boolean formula. Neither of these observations explain the sudden decrease in performance of all other methods except NB moms on the randomly generated graph colouring problems --- this is something that would be interesting to investigate further. 5.2 Disadvantages of NB-satz 5.2.1 Individual literal states The non-Boolean unit propagation step in the procedure on page \pageref{Non-Boolean Davis-Putnam} refers to the removal of literals from clauses in the formula. This procedure differs from the Boolean one because a situation can arise where a literal X\in {c,d} is removed, but X\in {a,b} is not. Therefore each individual literal must be able to be removed from the formula, independent of all other literals. In the Boolean procedure, all literals x are either LIVE or DEAD --- the removal of literals from clauses can be implemented efficiently by setting a single flag for each literal. However the non-Boolean procedure is implemented, it requires a larger amount of state than the Boolean procedure, so the search is slower in comparison. This problem is created by the semi-unit propagation step, which is critical to the success of the non-Boolean procedure. Unfortunately, the NB procedure cannot have semi-unit propagation without incurring the slow down due to the increased state. Possibly more sophisticated data structures could reduce this problem. 5.2.2 Difficult to find an accurate and fast heuristic The moms heuristic is often very inaccurate compared to the UP heuristic, in terms of number of branches, as seen on the randomly generated formulas, the n-queens problems and the planning problems. The UP heuristic is accurate, but sometimes extremely slow (2\frac{1}{2} minutes per branch on the largest planning problem). This is a problem and I could not solve it with a restriction for formulas with large domains. Both heuristics are inadequate compared to the performance of the Boolean procedure. The UP heuristic becomes less easy to restrict as branching commitment (number of subtrees) increases. The more subtrees there are at a single branch, the less different the branches are in terms of average effect of unit propagation at the branch. Chu Min Li \cite{Satz} shows that a Boolean pure UP heuristic outperforms a Boolean moms heuristic in terms of search time (of course, it also outperforms it in terms of search tree size). The restrictions he presents perform better still, but this trend is not seen on larger domains. On the randomly generated formulas, NB UP (non-Boolean pure UP heuristic) outperforms NB moms on problems up to and including domain size 4, but at domain size 8, NB moms wins. Furthermore, on larger domains, a well-performing restriction of the UP heuristic could not be found. As domain size increases, the extra accuracy of using the UP heuristic is not worth the extra cost. A solution to this dilemma could be to combat the cause --- the number of subtrees at each branch. A UP heuristic may then be more feasible for larger domains and an efficient restriction may be found. 5.3 Comparison to NB-walksat Non-Boolean Davis-Putnam has quite different benefits over Boolean Davis-Putnam than non-Boolean local search has over Boolean local search. The size of the explored search space is not increased, which is arguably the largest factor in the performance increase found by NB-walksat (in \cite{NB-walksat}). It is the crucial semi-unit propagation step which allows non-Boolean Davis-Putnam to perform better on formulas containing literals with large value sets. Both NB-satz and NB-walksat benefit from the reduction in problem size resulting from operating on the non-Boolean formula. Both sets of results show similar trends, although the local search procedure (both the Boolean and non-Boolean versions) have significantly shorter search times and can solve larger problems; such is their nature. 5.4 Further work 5.4.1 Different branching strategies A branch basically refines the current state --- a good branch maximises the amount of formula simplification arising from the branch while minimising the commitment. The branching method used by NB-satz carries quite a high commitment at each branch; reducing this commitment is a possible improvement to the search. With the branching method I used, the non-Boolean search tree is flatter than the Boolean search tree (whichever translation method is used). This is not really a good thing since it puts less importance on the variable order (there is less choice for the heuristic) and more importance on the value order (although not for unsatisfiable formulas). For example: for domain size d and v variables, the flattest tree is of depth 1 and branching factor d^{v} (this effectively enumerates all solutions if there is no value order). At the other end of the scale, the tallest tree is of depth (v\log _{2}d) and branching factor 2. Both have the same search space, but the latter is better because the variable ordering heuristic has more effect on the search. Assuming that a variable ordering heuristic is more accurate than a value ordering heuristic, less of the search space will need to be explored if each node has fewer subtrees. In addition to this, the more variables there are to choose from, the more choice the heuristic has. More choice for the heuristic suggests that the selected branch will be more likely to be better. I suggest that more choice for the heuristic would make a restricted non-Boolean UP heuristic feasible. Discussion Recall that the branching methods that I identified are: 1. For n possible values, each branch produces n subtrees, each making a full commitment to a single value. 2. The set of all values that could be explored is divided into two partitions. Each branch produces 2 subtrees, one making a partial commitment to one partition, the other making a partial commitment to the other partition. 3. For active values V, a branch on variable X and value a is binary, where one subtree makes the full commitment X\mapsto a and the other makes the partial commitment X\mapsto V\setminus a. Both of the alternative methods (2 and 3) make binary branches. For a variable X with n active values, there is 1 possible choice for a branch on X using method 1, n possible choices using method 2 and S(n,2) possible choices([footnote] S(m,k) is the Stirling number representing the number distinct partitions of m distinct elements into k distinct regions.) using method 3. There is more choice not only in the variable chosen at each branch, but also in the values instantiated to each subtree. Branching method 2 has as much choice as the unary translation, whereas method 3 has much more, possibly too much to examine all the possibilities. If a weaker commitment branching strategy is implemented, the UP heuristic will undoubtedly perform differently. Because there will be less commitment at each branch, the resulting amount of formula simplification will be reduced. This is the factor that guides the UP heuristic at present, so it is unclear how it will perform. It will have many more subtrees to examine with branching method 3, so some form of restriction on the partitions that get examined would be necessary. Such a heuristic may be difficult to construct. Possibly a combination of branching strategies that occur at different depths of the tree may perform well, where the branching factor can be reduced early in the tree and simplification (and commitment) can be increased towards the leaves. Of course, branching method 2 could be generalised to have n subtrees, with the active values divided between them. This would be trading a higher commitment for potentially more simplification --- I am unsure as to what value of n would perform best. 5.4.2 Improvement of the heuristic The non-Boolean moms heuristic is particularly brutal in it's regard for an unfavourable subtree. Recall that it maximises \frac{1}{n}\left[ min\left( w(X\in \{a_{1},\ldots \}),w(X\in \{a_{2},\ldots \}),\ldots ,w(X\in \{a_{n},\ldots \})\right) \right] , thus it chooses the variable with the best combination of value set size and best ``worst subtree''. It is the min function that selects the worst subtree; this is a straight generalisation of the Boolean heuristic but is perhaps a little out of place in a non-Boolean context. With increasing domain size, there are more subtrees, so basing the variable choice on the worst subtree is a little narrow-minded. I would suggest that a more gentle function would give better performance on problems with larger domains. So far, the moms heuristic has only considered the literals which have the value a in their value sets. Possibly considering the literals which do not have the value a in their value sets may be an important addition to the moms heuristic, since it is these literals which would contribute to future unit propagation. This is the ``remove clauses/remove literals'' debate from the value order section all over again. The UP heuristic seems to need to be more focused on literals with smaller value set sizes, to minimise the branching factor. This can be seen from the relative performance of NB UP and NB moms on the randomly generated formulas. A different branching strategy may allow a more efficient UP heuristic, due to more choice for the heuristic, as discussed above. 5.4.3 Dependency-directed backtracking Dependency-directed backtracking can significantly increase the performance of Boolean DP on some problems \cite{SATO}. I conjecture that a similar performance increase can be gained for non-Boolean DP. 5.4.4 Randomisation and restarts The heuristic may identify more than one ``best'' branch. Satz chooses the last of these candidates, but a random factor can be introduced without compromising the heuristic by randomly selecting one of these candidates as the branching variable. This random tie breaking is effective in Boolean DP, in combination with restarts([footnote] Satz-rand, a randomised version of satz is available from SATLIB.) . I think that non-Boolean DP would show the same benefit. 5.4.5 Modification of a Boolean solver A different approach to solving non-Boolean problems is to modify a Boolean solver to tackle some of it's shortcomings on solving translations of non-Boolean formulas. I do not believe that this approach has been taken before, but I suggest that it could be fruitful. For instance, the Boolean heuristic could be modified to only consider kernel clauses, thus it would not at all be affected by the ALO and AMO clauses and the extra variables in the unary-binary translation would not be branching candidates. A non-CNF Boolean DP solver could be used to work with binary translations, as these are not concisely expressed in CNF. 5.4.6 A non-CNF solver Certain problems get very large when translated to CNF, and it is this blow-up, rather than the actual problem that makes solving difficult. The CNF translation step could be avoided (much like the Boolean translation is avoided with a non-Boolean solver) by creating a non-CNF solver. 5.4.7 A special-purpose graph colouring algorithm The non-Boolean Davis-Putnam procedure takes part of the problem specification (the constraint of singular assignments) and moves this into the algorithm rather than the input data. This same technique can be applied to graph colouring problems, by placing the constraint that all adjacent nodes are different colours in the algorithm rather than the problem encoding, as it would be if it was encoded in SAT. A benefit arising from this is that the state is reduced, which means a quicker search. Also, the size of the problem encoding will not be dependent on the number of colours. 5.5 Summary It has been shown that NB-satz outperforms satz on a number of non-Boolean problems, despite using a heuristic which is either less powerful or slower to compute. It does performs worse on some classes of problem, but the Boolean procedure has a better heuristic and allows optimisations that reduce the complexity of certain steps in the search. I have identified points where the non-Boolean procedure has particular benefits over the translation approach and I have determined points where it is at a disadvantage. I speculate that the performance of the non-Boolean procedure can be increased by various developments, such as different branching methods, an improved heuristic and the techniques of dependency-directed backtracking and randomisation and restarts. In developing a non-Boolean Davis-Putnam procedure, I have shown that this approach is not equivalent to the translation approach. The results show large differences between the two methods. This study has suggested new directions that can be explored to further develop the non-Boolean procedure. The code for NB-satz is available on the Internet at: http://www-users.york.ac.uk/~pgs103/sat.html Acknowledgments I thank Alan Frisch, my supervisor, for his guidance throughout this project. Thank you to my parents and \heartsuit Viji for proofreading my report and to Shirley for her enthusiasm. Thanks to Kerry, who helped me with the finishing touches. References P. Cheeseman, B. Kanefsky and W. M. Taylor, ``Where the really hard problems are'', Proceedings of the IJCAI-91: pages 163--169, 1999. S. A. Cook, ``The complexity of theorem-proving procedures'', Proceedings of the Annual ACM Symposium on Theory of Computing 151--158, 1971. J. M. Crawford. ``Solving satisfiability problems using a combination of systematic and local search'', Second DIMACS Challenge: Cliques, Coloring, and Satisfiability, Rutgers University, NJ., 1993. J. M. Crawford and L. D. Auton, ``Experimental results on the crossover point in random 3SAT'', Artificial Intelligence, vol. 81, 1996. M. Davis and H. Putnam, ``A computing procedure for quantification theory'', Journal of the ACM, 7:201--215, 1960. M. Davis, G. Logemann and D. Loveland, ``A machine program for theorem proving'', CACM 5:394--397, 1969. O. Dubois, Y. Boufkhad et al., "SAT versus UNSAT, second DIMACS challenge", DIMACS Series in Discrete Mathematics and Theoretical Computer Science (AMS), 415-436, 1996. J. Franco and M. Paull, ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem'', Discrete Applied Mathematics 5(1):77--87, 1983. J. Freeman, ``Improvements to propositional satisfiability search algorithms'' , PhD thesis, The University of Pennsylvania, 1995. A. M. Frisch and T. J. Peugniez, ``Solving non-Boolean problems with stochastic local search: a comparison of encodings'', 1999. A. T. Goldberg, ``On the complexity of the satisfiability problem'', Courant Computer Science Report No. NSO-16, Courant Institute of Mathematical Sciences, Computer Science Department, New York University, 1979. J. N. Hooker and V. Vinay, ``Branching rules for satisfiability'', Journal of Automated Reasoning 15:359--383, 1995. R. G. Jeroslow and J. Wang, ``Solving propositional satisfiability problems'', Annals of Mathematics and Artificial Intelligence 1:167--187, 1990. C. M. Li and Anbulagan, ``Heuristics based on unit propagation for satisfiability problems'', Proceedings of the 15th IJCAI: pages 366--371, International Joint Conference on Artificial Intelligence, 1997. T. J. Peugniez, ``Solving non-Boolean satisfiability problems with local search'' BSc Dissertation, Department of Computer Science, University of York, March 1998. H. Zhang, M. Stickel, ``Implementing Davis-Putnam's method by tries'', Technical Report, University of Iowa, 1994. H. Zhang, ``SATO: an efficient propositional prover'', Proceedings of the International Conference on Automated Deduction 1997.