1: %possible additions: prove soundness & completeness of BFM
2: % make the statements about the # of constraints lemmas, and prove.
3: %%%%%%%%%%%%%% What to change if ever becomes a journal version %%%%%%%%%%%
4: % 1. Analysis of complexity of the reduction itself should be added after conjunctions matrices, in the end of sec. 4.3.
5: % 2. Check again example 1, is there a mistake in the last line of the table?
6: % 3. some quotes are reversed (' instead of `)
7:
8: \documentclass[12 pt]{llncs}
9: \usepackage{times}
10: %\usepackage{doublespace}
11: \textwidth 14.5 cm
12: \evensidemargin=0.5cm
13: \oddsidemargin=0.5cm
14: \usepackage{epsfig}
15: \usepackage{xspace}
16: \usepackage{amsfonts}
17: \input{hmacs}
18: \input{amacs}
19:
20: \normalsize
21: \newcommand\I{\overline{I}}
22: \newcommand\bv{\overline{b}}
23: \newcommand\con{`$\land$'}
24: \newcommand\dis{`$\lor$'}
25: \newcommand\condis{\land \!\!\!\!\lor}
26: %\renewcommand\baselinestretch{2}
27: \begin{document}
28: \title{
29: Deciding Disjunctive Linear Arithmetic \\with SAT
30: \author {Ofer Strichman}
31: \institute{Computer Science Department, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh,
32: PA 15213-3891, USA\\Email: \email{ofers@cs.cmu.edu}\\
33: \emph{Keywords}: Program Verification, Decision procedures, SAT
34: }
35: \thanks{This research was supported in part by the Office of Naval Research (ONR) and the Naval
36: Research Laboratory (NRL) under contract no. N00014-01-1-0796. }
37: \thanks{An early version of this article
38: appeared in \cite{S02}.}
39: \comment{The main additions in this extended version are:
40: A theoretical discussion on the advantages of the proposed method
41: comparing to existing ones, including two new claims in section
42: \ref{sec:revised}; A thorough experimental comparison of the methods,
43: including a new benchmark of several hundred randomly generated formulas. }
44: }
45:
46:
47: \maketitle
48:
49:
50: \begin{abstract}
51: Disjunctive Linear Arithmetic (DLA) is a major decidable theory that is supported by almost all
52: existing theorem provers. The theory consists of Boolean combinations of predicates of the form
53: $\Sigma_{j=1}^{n}a_j\cdot x_j \le b$, where the coefficients $a_j$, the bound $b$ and the variables
54: $x_1 \ldots x_n$ are of type Real ($\mathbb{R}$). We show a reduction to propositional logic from
55: disjunctive linear arithmetic based on Fourier-Motzkin elimination. While the complexity of this
56: procedure is not better than competing techniques, it has practical advantages in solving
57: verification problems. It also promotes the option of deciding a combination of theories by reducing
58: them to this logic. Results from experiments show that this method has a strong advantage over
59: existing techniques when there are many disjunctions in the formula.
60: \end{abstract}
61:
62: \section{Introduction}
63:
64:
65: Disjunctive Linear Arithmetic (DLA) is a major decidable theory that is supported by almost all
66: existing theorem provers, and is used frequently when proving infinite state systems. The theory
67: consists of Boolean combinations of predicates of the form $\Sigma_{j=1}^{n}a_j\cdot x_j \le b$,
68: where the coefficients $a_j$, the bound $b$ and the variables $x_1 \ldots x_n$ are of type Real
69: ($\mathbb{R}$).
70:
71:
72: Decision procedures for this theory typically handle disjunctions by `case-splitting', i.e.,
73: transforming the formula to Disjunctive Normal Form (DNF) and then solving each clause
74: separately. Naive case-splitting procedures explicitly transform the formula to DNF, and are
75: therefore very restricted in the size of the formula that they can handle (the number of clauses in
76: the resulting formula can be exponential in the size of the original formula). More sophisticated
77: implementations split the formula only `as needed', which increases in many cases the capacity of
78: these procedures, although there can still be an exponential number of cases to solve.
79:
80: Recently a different approach was introduced almost simultaneously by three different groups
81: \cite{MRS02,ABCKS02,SBD02}. The procedure is based on a combination of a SAT procedure and an arithmetic
82: solver, and is now implemented by tools such as \tool{cvc}, \tool{mathsat} and
83: \tool{ics-sat}\footnote{\tool{ics-sat} is the name we call the version of \tool{ics} that works
84: according to this combined approach. The distinction between the two versions is important in this
85: article, as \tool{ics} works with case-splitting.}. The procedure works roughly as
86: follows. The linear predicates are encoded with Boolean variables, and then the encoded Boolean
87: formula is solved with a SAT solver. If the SAT instance is unsatisfiable, then the procedure
88: terminates and declares the formulas unsatisfiable. Otherwise, it checks whether the given
89: assignment is consistent with respect to the linear constraints. This step amounts to solving a
90: conjunction of predicates or negation of predicates, which is possible by using any number of procedures
91: (see below). If a satisfying assignment is found, then the procedure terminates and declares the
92: formula to be satisfiable. Otherwise, it backtracks in order to find a different assignment, while
93: typically (depending on the specific system) applying a learning mechanism, i.e. adding a Boolean
94: conflict clause that prevents a repetition of the bad assignment. Although this approach can still
95: be seen as case splitting, as it still may call the arithmetic solver an exponential number of
96: times, the learning and pruning power of the SAT solver makes it far more robust than naive
97: case-splitting methods. We will further discuss the advantages and disadvantages of these techniques
98: in section \ref{sec:revised}.
99:
100: The lower-bound complexity of solving each DNF clause, i.e., a conjunction of linear constraints, is
101: polynomial \cite{K79}. When considering small to medium size problems, as the ones that are
102: typically encountered in formal verification, the existing polynomial procedures are rarely better
103: in practice comparing to some exponential methods like Simplex \cite{dantzig63} and the various
104: variable-elimination techniques. For this reason, as far as we know, no automated theorem prover
105: uses a polynomial procedure for linear arithmetic.
106:
107: The most commonly used method by theorem provers is the Fourier-Motzkin (FM) variable elimination
108: method \cite{BW94}, which is used in popular tools such as \tool{pvs}\cite{PVSg},
109: \tool{ics}\cite{FORS01}, \tool{svc}\cite{BDL96}, \tool{imps}\cite{FGT92} and others. We describe the
110: FM method in detail in section \ref{fourier}. Although FM has a worst-case super-exponential
111: complexity, it is popular because it is frequently faster than competing methods for the size of
112: instances encountered in practice. Hence, the current practice in solving DLA is to solve, in the
113: worst case, an exponential number of FM instances. Theoretically this is not the best possible, as
114: explained above, but experience has showed that for the type of formulas encountered in
115: verification, it is adequate.
116:
117: The procedure described in this paper solves one FM instance in order to generate a SAT instance,
118: and then solves this instance with a standard SAT solver. It has a similar complexity to what we
119: just described as the common practice, but we expect it to be better in practice because of reasons
120: that we will later discuss. SAT solvers are generally far more efficient than case splitting in
121: handling propositional combinations of formulas, although both have the same theoretical
122: complexity. Propositional SAT checkers apply techniques like {\it learning}, {\it pruning} and {\it
123: guidance} (`guidance' refers to heuristics for prioritizing the internal steps of the decision
124: procedure) that can not be easily imitated by case-splitting. We refer the reader to \cite{SSB02}
125: where an elaborated discussion of this distinction is given. Based on this observation, our
126: suggested procedure is expected to be more efficient than case-splitting methods in deciding
127: formulas where the case-splitting itself is the bottleneck of the procedure, i.e., formulas that
128: their equivalent DNF has many clauses, but each one of them is relatively small.
129:
130: An efficient reduction of DLA to propositional logic not only enables to (potentially) solve them
131: faster, but also to integrate them with other theories on the propositional logic level. Many other
132: decidable theories that are frequently encountered in verification (e.g. bit-vector arithmetic
133: \cite{J01}) already have such reductions to propositional logic. Solving mixed theories by reducing
134: them to a common logic facilitates the application of various learning techniques between
135: sub-expressions that originate from different theories. Furthermore, current popular techniques for
136: integrating theories such as Nelson-Oppen \cite{NO79} invoke different procedures for deciding each
137: theory, and propagate equalities between them in order to decide the combined theory. The overhead
138: of this mutual updating can become significant. This overhead is avoided if only one procedure (SAT
139: in this case) is used.
140:
141:
142:
143: The rest of the article is structured as follows. In the next section we briefly describe the FM
144: method. In section \ref{propositional} we present a propositional version of the same procedure and
145: explain how it can be used to reduce DLA to SAT. In section \ref{conjunctions} we present a method called `conjunctions matrices',
146: which is useful for reducing the complexity of the procedure described in section
147: \ref{propositional}. In section \ref{experiments} we summarize our experiments with this method on
148: both real examples and random instances.
149:
150: \section{Fourier-Motzkin Elimination}
151: \label{fourier}
152: A linear inequality predicate over $n$ variables has the form $\Sigma_{j=1}^{n}a_j\cdot x_j \le
153: b$. A conjunction of $m$ such constraints is conveniently described by $C: A\I \le \bv$ where $A$ is
154: an $m \times n$ real-valued coefficient matrix, $\I = x_1...x_n$ is a vector of $n$ variables, and
155: $\bv$ is a vector of real-valued bounds. Given a variable order $x_1...x_n$ the FM method eliminates
156: (existentially quantifies) them in decreasing order. Each variable is eliminated by projecting its
157: constraints on the rest of the system. The procedure works as follows: at each elimination step, the
158: list of constraints is partitioned to three segments, according to the sign of the coefficient of
159: $x_n$ in each constraint. Let $a_{i,n}$ denote the coefficient of $x_n$ in constraint $i$, for $i
160: \in[1..m]$.
161:
162: \begin{minipage}{12 cm}
163: \vspace{0.1 cm}
164: The three segments are:
165: \begin{enumerate}
166: \item For all $i$ s.t. $a_{i,n}>0$: \hspace{1 cm} \hspace{1.3 cm} $a_{i,n}\cdot x_n\ \le \ b_i - \Sigma_{j=1}^{n-1}a_{i,j}\cdot x_j$
167: \item For all $i$ s.t. $a_{i,n}<0$: \hspace{1 cm} $\Sigma_{j=1}^{n-1}a_{i,j}\cdot x_j-b_i\ \le \ -a_{i,n}\cdot x_n$
168: \item For all $i$ s.t. $a_{i,n}=0$: \hspace{1 cm} \hspace{0.7 cm}$\Sigma_{j=1}^{n-1}a_{i,j}\cdot x_j\ \le\ b_i$
169: \end{enumerate}
170: \vspace{0.1 cm}
171: \end{minipage}
172:
173: The first and second segments correspond to upper and lower bounds on $x_n$, respectively. To
174: eliminate $x_n$, FM replaces each pair of lower and upper bound constraints $L \le c_l \cdot x_n$
175: and $c_u \cdot x_n \le U$, where $c_l,c_u >0$, with the new constraint $c_u\cdot L \le c_l \cdot U$.
176: If, in the process of elimination, the procedure derives the constraint $c \le 0$ where $c$ is a
177: constant greater than 0, it terminates and indicates that the system is unsatisfiable.
178:
179: Note that it is possible that variables are not bounded from both ends. In this case it is possible
180: to simplify the system by removing these variables from the system together with all the constraints
181: to which they belong. This can make other variables unbounded. Thus, this simplification stage
182: iterates until no such variables are left.
183:
184: The FM method can result in the worst case in $m^{2^n}$ constraints, which is the reason that it is
185: only suitable for a relatively small set of constraints with small number of variables. There are
186: various heuristics for choosing the elimination order. A standard greedy criteria gives priority to
187: variables that their elimination produces less new constraints.
188: \begin{example}
189: Consider the following formula:
190: \[
191: \varphi = x_1 - x_2 \le 0\quad \land \quad x_1 - x_3 \leq 0 \quad \land \quad -x_1 + 2x_3 + x_2\le 0 \quad \land \quad -x_3 \le -1 \]
192:
193: \nin The following table demonstrates the elimination steps following the variable order $x_1$,$x_2$,$x_3$:
194:
195: \begin{center}
196: \begin{tabular}{|c|c|c|c|}\hline
197: \ Eliminated\ & Lower & Upper & New \\
198: var & bound & bound & constraint \\ \hline
199: $x_1$ &\ $x_1-x_2\le 0\ $&$\ -x_1+2x_3+x_2\le 0\ $&$2x_3 \le 0$ \\
200: &$x_1-x_3\le 0$&$-x_1+2x_3+x_2\le 0$&$\ x_2 + x_3 \le 0\ $ \\ \hline
201: $x_2$ & \multicolumn{3}{|c|}{ no lower bound}\\ \hline
202: $x_3$ & $2x_3\le 0$ &$ -x_3 \le -1$& $2 \le 0 $\\ \hline
203: \end{tabular}
204: \end{center}
205: The last line results in a contradiction, which implies that this system is unsatisfiable.
206: \qed
207: \end{example}
208:
209: \nin The extension of FM to handle a combination of strict ($<$) and weak ($\le$) inequalities is
210: simple. If either the lower or upper bound are a strict inequality,
211: then so is the resulting constraint.
212:
213:
214: In the next section we present a Boolean version of the FM method.
215:
216: \section {A Boolean version of Fourier-Motzkin}
217: \label{propositional}
218: Given a DLA formula $\varphi$, we now show how to derive a
219: propositional formula $\varphi'$ s.t. $\varphi$ is satisfiable iff $\varphi'$ is satisfiable. The
220: procedure for generating $\varphi'$ emulates the FM method.
221: \begin{enumerate}
222: \item \label{normalize} Normalize $\varphi$:
223: \begin{enumerate}
224: \item \label{eq} Rewrite equalities as conjunction of inequalities.
225: \item \label{nnf} Transform $\varphi$ to Negation Normal Form (negations are allowed only over
226: atomic constraints).
227: \item Eliminate negations by reversing inequality signs.
228: \end{enumerate}
229: \item \label{encode} Encode each inequality $i$ with a Boolean variable $e_i$. Let $\varphi'$ denote
230: the encoded formula.
231: \item \label{perform}
232: \begin{enumerate}
233: \item Perform FM elimination on the set of all constraints in $\varphi$, while
234: assigning new Boolean variables to the newly generated constraints.
235: \item At each elimination step, for every pair of constraints $e_i,e_j$ that result in the new
236: constraint $e_k$, add the constraint $e_i \land e_j \rightarrow e_k$ to $\varphi'$.
237: \item If $e_k$ represents a contradiction (e.g., $1 \le 0$), replace $e_k$ by \false.
238: \end{enumerate}
239: \end{enumerate}
240: %
241: We refer to this procedure from here on as Boolean Fourier Motzkin (BFM).
242: \begin{example}
243: \label{ex_fm}
244: Consider the following formula:
245: \[\varphi = 2x_1 -x_2 \le 0 \quad \land \quad (2x_2 - 4x_3 \le 0 \quad \lor \quad x_3 - x_1 \le - 1)\]
246: By Assigning an increasing index to the predicates from left to right we initially get $\varphi' =
247: e_1 \land (e_2 \lor e_3)$.
248:
249: Let $x_1,x_2,x_3$ be the elimination order. The following table illustrates the process of updating
250: $\varphi'$:
251:
252: \begin{center}
253: \begin{tabular}{|c|c|c|c|c|c|}\hline
254: Elimina- & Lower & Upper & New & Enco- & Add to $\varphi'$ \\
255: ted var & bound & bound & constraint & ding & \\ \hline
256: $x_1$ & $x_3-x_1 \le -1 $ & $2x_1-x_2 \le 0$ & $2x_3-x_2 \le -2$ & $e_4$ & $e_3 \land e_1 \rightarrow e_4$ \\
257: $x_2$ & $2x_3-x_2 \le -2$ & $2x_2-4x_3 \le 0$& $4 \le 0 $ & \false & $e_4 \land e_2 \rightarrow \mbox{\false} $ \\\hline
258:
259: \end{tabular}
260: \end{center}
261:
262: \nin Thus, the resulting satisfiable formula is:
263: \[\varphi' = (e_1 \land (e_2 \lor e_3)) \land (e_1 \land e_3 \rightarrow
264: e_4) \land (e_4 \land e_2 \rightarrow \mbox{\false})\]
265: \qed
266: \end{example}
267:
268:
269:
270: Example \ref{ex_fm} demonstrates the main drawback of this method. Since in step \ref{encode} we
271: consider all inequalities, regardless of the Boolean connectives between them, the number of
272: constraints that the FM procedure adds is potentially larger than those that we would add if we
273: considered each case separately (where a `case' corresponds to a conjoined list of inequalities). In
274: the above example, case splitting would result in two cases, none of which results in added
275: constraints. Since the complexity of FM is the bottleneck of this procedure, this drawback may
276: significantly worsen the overall run time and risk its usability.
277:
278: As a remedy, we will suggest in section \ref{conjunctions} a polynomial method that bounds the number of
279: constraints to the same number that would otherwise be added by solving the various cases
280: separately.
281:
282: \subsubsection{Complexity of deciding $\varphi'$.}
283: The encoded formula $\varphi'$ has a unique structure that makes it easier to solve comparing to a general
284: propositional formula of similar size. Let $m$ be the set of encoded
285: predicates of $\varphi$ and $n$ be the number
286: of variables.
287: \begin{proposition}
288: $\varphi'$ can be decided in time bounded by $O(2^{|m|}\cdot |m|^{2^n})$.
289: \end{proposition}
290: \begin{proof} SAT is worst case exponential in the number of decided
291: variables and linear in the number of clauses. The Boolean value assigned to the predicates in $m$
292: imply the values of all the generated predicates\footnote{Note that the constraints added in step
293: \ref{perform} are Horn clauses. This means that for a given assignment to the predicates in $m$,
294: these constraints are solvable in linear time.}. Thus, we can restrict the SAT solver to split only
295: on $m$. Hence, in the worst case the SAT procedure is exponential in $m$ and linear in the
296: number of clauses, which in the worst case is $|m|^{2^n}$.
297: \qed
298: \end{proof}
299:
300: \section{Conjunctions matrices}
301: \label{conjunctions}
302: Case splitting can be thought of as a two step procedure, where in the first step the formula is
303: transformed to DNF, and in the second each clause, which now includes a conjunction of constraints,
304: is solved separately. In this section we show how to predict, in polynomial time, whether a given
305: pair of predicates would share a clause if the formula was transformed to DNF. It is clear that
306: there is no need to generate a new constraint from two predicates that do not share a clause.
307:
308: \subsection{Joining operands}
309: \label{joining}
310: We assume that $\varphi$ is normalized, as explained in step \ref{normalize}. Let $\varphi'_f$
311: denote the encoded formula after step \ref{encode} and $\varphi'_c$ denote the added constraints of
312: step \ref{perform} (thus, after step \ref{perform} $\varphi' = \varphi'_f \land \varphi'_c$). All
313: the internal nodes of the parse tree of $\varphi'_f$ correspond to either disjunctions or
314: conjunctions. Consider the lowest common parent of two leaves $e_i,e_j$ in the parse tree. We call
315: the Boolean operand represented by this node the {\em joining operand} of these two leaves and denote
316: it by $J(e_i,e_j)$.
317: \begin{example}
318: \label{ex1} In the formula $\varphi'_f = e_1 \land (e_2 \lor e_3)$, $J(e_1,e_2)=$ \con\ and $J(e_2,e_3)=$ \dis.
319: \qed
320: \end{example}
321:
322: \nin
323: For simplicity, we first assume that no predicates appear in $\varphi$ more than once. In section
324: \ref{handling} we solve the more general case. Denote by $\varphi^D$ the DNF representation of $\varphi$. The
325: following proposition is the basis for the prediction technique:
326: \begin{proposition}
327: \label{share}
328: Two predicates $e_i,e_j$ share a clause in $\varphi^D$ iff $J(e_i,e_j) =$ \con.
329: \end{proposition}
330: \begin{proof}
331: Recall that $\varphi'_f$ does not contain negations and no predicate appears more than
332: once. ($\Rightarrow$) Let $node$ denote the node joining $e_i$ and $e_j$, and assume it
333: represent a disjunction ($J(e_i,e_j)=$\dis). Transform the right and left branches descending from
334: $node$ to DNF. A disjunction of two DNF formulas is a DNF, and therefore the formula under $node$ is
335: now a DNF expression. If $node$ is the root or if there are only disjunctions on the path from
336: $node$ to the root, we are done. Otherwise, the distribution of conjunction only adds elements
337: to each of the clauses under $node$ but does not join them into a single clause. Thus, $e_i$ and
338: $e_j$ do not share a clause if their joining operand is a disjunction. ($\Leftarrow$) Again let
339: $node$ denote the node joining $e_i$ and $e_j$, and assume it represents a conjunction
340: ($J(e_i,e_j)=$\con). Transform the right and left branches descending from $node$ to
341: DNF. Transforming a conjunction of two DNF sub formulas back to DNF is done by forming a clause for
342: each sequence of literals from the different clauses. Thus, at least one clause contains $e_i \land
343: e_j$. Since there are no negations in the formula, the literals in this clause
344: remain together in $\varphi^D$ regardless of the Boolean operands above $node$.
345: \qed
346: \end{proof}
347:
348: \nin For a given pair of predicates, it is a linear operation (in the height of the parse tree $h$)
349: to check whether their joining operand is a conjunction or disjunction. If there are $m$ predicates
350: in $\varphi$, constructing the initial $m \times m$ {\em conjunctions matrix $M_\varphi$} of
351: $\varphi$ has the complexity of $O(m^2h)$. $M_\varphi$ is a binary, symmetric matrix, where
352: $M_\varphi[e_i,e_j] = 1$ if and only if $J(e_i,e_j)=$\con. For example, $M_\varphi$ corresponding
353: to $\varphi'_f$ of example \ref{ex1} is given by
354: \[
355: M_\varphi = \left(
356: \begin{array}{c|ccc}
357: & e_1 & e_2& e_3 \\ \hline
358: e_1 & 0 & 1 & 1 \\
359: e_2 & 1 & 0 & 0 \\
360: e_3 & 1 & 0 & 0 \\
361: \end{array} \right)\]
362:
363: \nin Given proposition \ref{share}, this
364: means that these predicates share at least one clause in $\varphi^D$. New entries are added to
365: $M_\varphi$ when new constraints are generated, and other entries, corresponding to constraints with
366: non-zero coefficients over eliminated variables, are removed. The entry for a new predicate $e_k$
367: that was formed from the predicates $e_i,e_j$ is updated as follows:
368: \[\forall l \in [1..k-1].\ M_\varphi[e_k,e_l] = M_\varphi[e_i,e_l] \land M_\varphi[e_j,e_l]\]
369: This reflects the fact that the new predicate is relevant only to predicates that share a clause with both
370: $e_i$ and $e_j$.
371:
372: \subsection{Handling repeating predicates}
373: \label{handling}
374: Practically most formulas contain predicates that appear more than once, in different parts of the
375: formula. We denote by $e^k_i$, $k \ge 1$ the $k$ instance of the predicate $e_i$ in
376: $\varphi'$. It is possible that the same pair of predicates has different joining operands,
377: e.g. $J(e^1_i,e^1_j)=$\con\ but $J(e^1_i,e^2_j)=$\dis. There are two possible solutions to this
378: problem:
379: \begin{enumerate}
380: \item Represent each predicate instance as a separate predicate.
381: \item Assign $M_\varphi[e_i,e_j] = 1$ if there exists an instance of $e_i$ and of $e_j$
382: s.t. $J(e_i,e_j) =$ \con.
383: \end{enumerate}
384:
385: The first option leads to a higher complexity of constructing the initial conjunctions matrix,
386: because it is determined by the number of predicate instances rather than the number of unique
387: predicates. More specifically, if $m'$ denotes the number of predicate instances, then the
388: complexity of constructing the initial matrix $M_\varphi$ is $O(m'^2h)$.
389:
390:
391: \nin The second option has a more concise representation, but may result in redundant constraints, as the
392: example below demonstrates.
393: \begin{example}
394: Let $\varphi'_f = e_1 \land (e_2 \lor e_3) \lor (e_2 \land e_3)$. According to option 2, $\varphi'$
395: contains only three predicates $e_1 \dots e_3$ and therefore $M_\varphi$ is a $3 \times 3$ matrix
396: with an entry `1' in all its cells. Thus, $M_\varphi$ does not contain the information that the
397: three predicates never appear together in the same clause, which potentially results in
398: redundant constraints. \qed
399: \end{example}
400:
401:
402: \nin Conjunctions matrices can be used to speed up many of the other decision procedures that were
403: published in the last few years for subset of linear arithmetic
404: \cite{GSZAS98,BV00,BGV99,BGV01,PRSS99,SSB02}. We refer the reader to a technical report \cite{S02tech}
405: for a detailed description of how this can be done.
406:
407: \subsection{A revised decision procedure and its complexity}
408: \label{sec:revised}
409: Given the initial conjunctions matrix $M_\varphi$, we now change step \ref{perform} as follows:
410:
411: % if we change the numbering of step (b), update the line beneath the procedure (in the sentance
412: % 'the main difference...')
413:
414: \begin{enumerate}
415: \item[\ref{perform}.] \label{perform2}
416: \begin{enumerate}
417: \item Perform FM elimination on the set of all constraints in
418: $\varphi$, while assigning new Boolean variables to the newly generated constraints.
419: \item \label{ateach2} At each elimination step consider the pair of constraints $e_i,e_j$ only if $M_\varphi[e_i,e_j] = 1$. In this case let $e_k$ be the new predicate.
420: \begin{enumerate}
421: \item Add the constraint $e_i \land e_j \rightarrow e_k$
422: to $\varphi'$.
423: \item If $e_k$ represents a contradiction (e.g., $1 \le 0$), replace $e_k$ by \false.
424: \item Otherwise update $M_\varphi$ as follows: \\ $\forall l \in [1..k-1].\ M_\varphi[e_k,e_l] =
425: M_\varphi[e_i,e_l] \land M_\varphi[e_j,e_l]$.
426:
427: \end{enumerate}
428: \end{enumerate}
429: \end{enumerate}
430:
431:
432: \nin
433: \newcommand\bfm{$bfm$\xspace}
434: \newcommand\split{$split$\xspace}
435: \newcommand\comb{$comb$\xspace}
436:
437: The main difference between this procedure and the previous one is that now step \ref{perform}(b) is
438: restricted to pairs of predicates that are conjoined in the DNF of the formula.
439:
440: Given the revised procedure, we now compare the number of constraints that it generates comparing to
441: the case-splitting methods, and the combined SAT/FM method \cite{MRS02,ABCKS02,SBD02} that was
442: described in the introduction. Let \bfm, \split and \comb be the number of constraints that are
443: generated by these three techniques, respectively.
444:
445: \begin{nclaim}
446: For unsatisfiable formulas, BFM generates less or equal number of constraints to the accumulated number of constraints that are
447: generated by case splitting (\bfm $\le$ \split).
448: \end{nclaim}
449: This claim can be easily justified with the observation that due to conjunctions matrices, no
450: constraint is generated in BFM that is not a resolvent of two constraint in a DNF clause. This means
451: that the same resolvent is generated by case-splitting methods. In satisfiable instances, the number
452: of constraints generated by case splitting depends on the location of the first satisfiable
453: clause. While case splitting terminates after finding the first such clause, \bfm generates all
454: constraints.
455:
456: \begin{nclaim}
457: In most cases in which the formula is unsatisfiable, \bfm$ \ll$ \split.
458: \end{nclaim}
459: The reason for the big difference between the two procedures is that constraints that are repeated
460: in many separate cases resolve in a single new constraint in BFM. For example, naive case splitting
461: over the formula $\varphi' = e_1 \land e_2 \land (e_3 \lor e_4)$ generates the resolvent of $e_1$
462: and $e_2$ twice, while BFM only generate it once\footnote{Smarter implementation of case splitting
463: can identify, in this simple example, that the resolvent has to be generated once. But in the
464: general case redundant constraints can be generated.}. As states above, the comparison of the two
465: methods is harder in the case of satisfiable formulas, since the number of constraints generated by
466: case splitting procedures depends on the location of the first satisfiable clause.
467:
468: The value of \comb is harder to compare to \bfm and \split, because in practice it strongly depends
469: on the success of the heuristics in the SAT procedure to prune the search space. By guiding the
470: search, the SAT solver may eventually call the arithmetic procedure for only a small subset of the
471: possible combinations of predicates. In the worst case, however, \comb can be larger than \split, because it may
472: generate resolvents of constraints that belong to different DNF clauses (adding conjunctions
473: matrices to this method can solve this problem. Such an optimization was not described, though, in
474: the literature \cite{MRS02,ABCKS02,SBD02}).
475:
476: Conjunctions matrices is not the only reason for the potentially larger number of constraints that
477: are generated by the SAT/FM combined procedure. Unlike BFM, this algorithm may generate the same
478: constraint more than once. Such repeated resolution can occur, for example, if a pair of consistent
479: predicates appear in many satisfying assignments. When each of these assignments is checked for
480: consistency, the resolvent of this pair is potentially regenerated. Although saving this information
481: in a hash table may save some of this repeated work, it may introduce a new source of complexity
482: because of the possibly exponential number of resolvents.
483:
484: A third source for a large number of redundant constraints in the combined procedure, which does not
485: occur in \tool{bfm}, is the following. Given a set of predicates $p_1 \ldots p_n$, assume that only
486: $p_1$ and $p_2$ are contradictory. Once the conflict in the set $p_1\ldots p_n$ is identified, a
487: conflict clause of size $n$ is added, which prevents a repetition of this assignments. This clause
488: does not, however, prune the other $2^{n - 2} - 1$ contradictory assignments to this set. There are
489: several solutions to this problem, all of which are either computationally expensive or not
490: optimal. \tool{cvc} tries to overcome this problem by identifying a small (yet not necessarily
491: minimal) subset of these literals that actually cause the conflict. In our example, ideally it
492: identifies that $p_1$ and $p_2$ alone cause the conflict. Consequently it adds a conflict clause of
493: size two, pruning away the redundant assignments as well as the corresponding resolvents and
494: conflict clauses. The \tool{ics-sat} tool \cite{MRS02} copes with this problem by following a
495: trial-and-error approach, in which in each step it tries to remove a predicate and see whether the
496: conflict still occurs. If the answer is affirmative - it removes the reference to this predicate from the
497: conflict clause. The success of this approach naturally depends on the order in which the predicates
498: are removed, and in general does not detect a minimal subset.
499:
500: %%%%%%%%%%%%%%%%%% new section (not submitted)
501: \comment{
502: \section{A generalized framework}
503: The proposed method is a very simple example of a more broad framework
504: of converting decision procedures for disjunctive theories to
505: SAT. With this framework, every procedure that is based on generating and solving a
506: sequence of problems $\varphi_0 \ldots \varphi_n$ (where $\varphi_0$
507: is the original problem and for all $i > 0$ $\varphi_i$ is satisfiable
508: only if $\varphi_{i-1}$ is satisfiable) can be extended to handle a
509: Boolean combination of the theory through SAT. The framework is the
510: following:
511: \begin{enumerate}
512: \item Let $S, |S| = n$ denote the set of existing distinct atoms in the formula. Encode each atom $a_i \in S$ (e.g. a predicate) with a Boolean variable $e_i$.
513: \item Use the decision procedure to decide $\bigwedge_{i=0}^{n-1}$.
514: \item If a new subformula is derived from
515: a subset $s$ of $S$, add an implication $\wedge_{s_i \in s}s_i \rightarrow s_{n+1}$ where
516: $s_{n+1}$ is the encoding of the new subformula. $s_{n+1}$ is replaced by the constant \false if a
517: contradiction is derived.
518: \item Solve the resulting SAT instance.
519: \end{enumerate}
520:
521: In the FM case, each $\varphi_i$ corresponds to a projection of the problem to a reduced set of
522: variables, hence $n$ is bounded by the number of variables in the original formula $\varphi_0$. In
523: the case of equality formulas (Boolean combination of equalities), the procedure of Bryant et
524: al. \cite{Bryant} can be seen as an instance of this framework as well:
525: }
526: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
527:
528: \section{Experiments}
529: \label{experiments}
530: To test the efficiency of BFM, we implemented a tool called \tool{bfm} on top of \tool{porta} \cite{porta}. We
531: then randomly generated formulas in 2-CNF style (that is, a 2-CNF where the literals are linear
532: inequalities) with different number of clauses and variables. The coefficients were chosen
533: randomly in the range $-10..10$. The time it takes to generate the SAT instance with \tool{bfm} is
534: summarized in \Figr{table}. The time it takes Chaff \cite{chaff01} to solve each of the instances
535: that we are able to generate is relatively negligible. Normally it is less than a second, with the
536: exception of 3 instances that take 10-20 seconds each to solve. All experiments were run on a 1.5
537: GHz AMD Athlon machine with 1.5 G memory, on top of Linux.
538:
539: \begin{figure}
540: \begin{center}
541: \begin{tabular}{|c||c|c|c|c|c|c|c|c|}\hline
542: & \multicolumn{8}{c|}{\# clauses} \\ \hline
543: \# vars & {\ \bf 10}&{\ \bf 30}&{\ \bf 50}&{\ \bf 70}&{\ \bf 90}&{\bf 110}&{\bf 130}&{\bf 150} \\ \hline \hline
544: {\bf 10}& \e & 0.2& 0.2& 1.1& 56& 103& 208& 254 \\ \hline
545: {\bf 30}& \e & 0.1& 0.2& 2.5& 61.1& 68& 618& \E \\ \hline
546: {\bf 50}& 0.1& 0.1& 0.2& 0.3& 4.9& 8& 173& 893 \\ \hline
547: {\bf 70}& 0.1& 0.2& 0.2& 0.4& 13.4& 108& \E& \E \\ \hline
548: {\bf 90}& 0.2& 0.2& 0.3& 0.3& 0.5& 1& 14& 181 \\ \hline
549: {\bf 110}& 0.3& 0.3& 0.5& 8.2& 396& 594& \E& \E \\ \hline
550: {\bf 130}& 0.3& 0.3& 0.4& 0.7& 2.9& 195& 2658& \E \\ \hline
551: {\bf 150}& 0.2& 0.3& 0.5& 0.8& 18.4& 334& 1227& \E \\ \hline
552: \end{tabular}
553: \caption{Time, in seconds, required for generating a SAT instance for
554: random 2-CNF style linear inequalities with a varying number of
555: clauses and variables. `\E' indicates running time exceeding 2 hours. }
556: \label{fig:table}
557: \end{center}
558: \end{figure}
559: %
560: We also ran these instances with \tool{ics} and \tool{cvc}. \tool{ics} solves these type of formulas
561: with FM combined with case-splitting, while \tool{cvc} implements a combined SAT/FM procedure, as
562: described in the introduction. Both tools can solve only one of these instances (the 10 x 10
563: instance) in the specified time bound. They either run out of memory or out of time in all other
564: cases. This is not very surprising, because in the worst case $2^c$ separate cases need to be
565: solved, where $c$ is the number of clauses.
566:
567: The CNF style formulas are harder not only for \tool{ics} and
568: \tool{cvc}, but also for \tool{bfm} because they make conjunctions
569: matrices ineffective. Each predicate in $\varphi$ appears with all
570: other predicates in some clause of $\varphi^D$, except those
571: predicates it shares a clause with in $\varphi$. Thus, almost all the
572: entries of $M_\varphi$ are equal to `1'. In general, conjunctions
573: matrices only prevent \bfm from adding redundant constraints, and in
574: CNF formulas only little redundancy is created in the first place. In
575: order to check the effectiveness of these matrices and experiment with
576: a larger set of formulas, we ran another batch of examples, where this
577: time the Boolean connectives (conjunction or disjunction) between the
578: linear constraints is chosen randomly. That is, a formula with $n$
579: variables and $m$ clauses has the form ${\condis}_{1 \ldots m}(p(n)
580: \ {\condis}\ p(n))$ where $\condis$ denotes either a conjunction or a
581: disjunction, and $p(n)$ is a linear predicate with $n$ variables and randomly chosen coefficients. For each cell in the table of figure
582: \ref{fig:table-new} we generated six random instances (a total of 384
583: random formulas). The numbers in the table represent the average time
584: it takes to generate the SAT instance with BFM \emph{without}
585: conjunctions matrices. For comparison, the time it takes to generate
586: the corresponding SAT instances \emph{with} conjunctions matrices is
587: almost negligible (a few seconds to generate the entire set). The
588: reason for this performance can be attributed to the random
589: construction which apparently results in very few concurrent
590: constraints. As before, solving the generated SAT formulas does not
591: consume a significant amount of time. We also ran \tool{cvc} on this
592: batch of examples. \tool{cvc} can solve 18 formula out of the 384
593: rather rapidly (the longest took about three minutes), but exceeds the
594: time bound or, more frequently, runs out of memory in all other cases.
595:
596: There are several interesting things to note about the results in
597: figure \ref{fig:table-new}. First, the results tend to be worse when
598: the ratio between the number of clauses to number of variables is
599: high. This is not surprising because FM is sensitive to the product of
600: upper and lower bounds on each variable. The higher the ratio is, the
601: larger this product is on average. Second, although not listed here,
602: there seems to be a very large variance between the different samples,
603: in particular when the formulas are large. For example, the standard
604: deviation of the results in each of the cells in the right-most column
605: is around 400. The reason for these extreme differences is not the
606: different Boolean structures (to which BFM is insensitive if
607: conjunctions matrices is inactive), rather it is the different number
608: of lower and upper bounds on each variable, which is determined by the
609: randomly selected sign of the coefficients.
610:
611: \begin{figure}
612: \begin{center}
613: \begin{tabular}{|c|c|c|c|c|c|c|c|c|} \hline
614: & \multicolumn{8}{c|}{\# clauses} \\ \hline
615: \# vars & {\ \bf 10}&{\ \bf 30}&{\ \bf 50}&{\ \bf 70}&{\ \bf
616: 90}&{\bf 110}&{\bf 130}&{\bf 150} \\ \hline \hline
617: {\bf 10} & \e & \e & 0.1 & 0.5 & 2.4 & 2.8 & 385.0 & 719.8 \\ \hline
618: {\bf 30} & \e & \e & 0.1 & 0.7 & 0.3 & 174.2 & 534.4 & 672.0 \\ \hline
619: {\bf 50} & \e & \e & 0.2 & 1.6 & 3.9 & 114.3 & 393.3 & 696.0 \\ \hline
620: {\bf 70} & \e & \e & 0.2 & 4.2 & 1.2 & 10.2 & 542.3 & 446.1 \\ \hline
621: {\bf 90} & \e & 0.1 & 0.1 & 0.4 & 0.6 & 285.2 & 103.4 & 425.4 \\ \hline
622: {\bf 110}& \e & 0.1 & 0.2 & 0.7 & 0.3 & 8.27 & 107.4 & 171.0 \\ \hline
623: {\bf 130}& \e & 0.1 & 0.2 & 0.7 & 0.7 & 1.37 & 13.8 & 166.6 \\ \hline
624: {\bf 150}& \e & 0.1 & 0.2 & 0.3 & 0.5 & 0.55 & 0.7 & 0.8 \\ \hline
625: \end{tabular}
626: \caption{Average time, in seconds, required for generating a SAT
627: instance for a formula with random Boolean structure, without
628: conjunctions matrices. With conjunctions matrices the time is almost
629: negligible.}
630: \label{fig:table-new}
631: \end{center}
632: \end{figure}
633:
634: \begin{figure}
635: \begin{center}
636: \begin{tabular}{|c|c|c|c|c|}\hline
637: \bf{Source} & \bf{Instance}& \ \tool{bfm}\ & \ \tool{ics}\ &\ \tool{cvc}\ \\ \hline
638: Hardware & 1-- 5 & \e & \e & \e \\ \cline{2-5}
639: designs & 6-7 & \e & \E & \e \\ \hline
640: Scheduling & 1--2 & \e & \e & \e \\ \cline{2-5}
641: problems & 3 & 90 & \E & \e \\ \cline{2-5}
642: & 4 & 3 & 952 & 221 \\ \hline
643: Timed & 1-2 & \e & \e & \e \\ \cline{2-5}
644: Automata & 3 & \e & 35 & \e \\ \hline \hline
645: Random & 1 & \E & 2 & \E \\ \cline{2-5}
646: (Conjoined) & 2 & \E & 7 & \E \\ \hline
647: \end{tabular}
648: \caption{ Results achieved by the three tested solvers on several realistic examples from different origins. `\E' indicates running time exceeding 2 hours. }
649: \label{fig:table2}
650: \end{center}
651: \end{figure}
652: %
653: Next, we ran \tool{bfm}, \tool{ics} and \tool{cvc} on several real examples. The results, which are
654: not as conclusive as with the random instances (many of them can be solved easily by all three
655: tools), are summarized in figure \ref{fig:table2}. As in the random
656: instances, here too there seems to be an extreme variation in the
657: performance of the tools with respect to the different formulas, which can probably be attributed to
658: the FM method. If the number of constraints starts to grow exponentially, it is typically impossible
659: to solve the instance in a short time. The examples shown in the table are the following. The first
660: batch includes seven formulas resulting from symbolic simulation of hardware designs. The second
661: batch includes four formulas resulting from scheduling problems. The third batch of examples
662: contains three standard timed-automata verification problems, namely the verification of a railroad
663: crossing controller. The first three sets of examples consist of a Boolean combination of
664: \emph{separation predicates} rather than full linear arithmetic, i.e. predicates of the form $x < y
665: + c$, where $c$ is a constant. This is obviously a special case of linear arithmetic. We also
666: examined two standard \tool{ics} benchmarks, `linsys-035' and `linsys-100', which consist of 35 and
667: 100 variables and linear inequalities, respectively. The results corresponding to these examples
668: appear as the last batch in the table. Note that while \tool{ics} solves these instances in a few
669: seconds, both \tool{bfm} and
670: \tool{cvc} cannot solve them in the specified time limit. The reason for this seemingly inconsistency is that the \tool{ics} benchmark
671: formulas consist of a conjunction of linear equalities, and therefore no case splitting is
672: required. The better performance of \tool{ics} can be attributed to the higher quality of
673: implementation of FM comparing to that of \tool{porta}, on top of which \tool{bfm} is built, and \tool{cvc}.
674:
675: Our conclusion from the experiments is that the advantage of \tool{bfm}, as stated in the
676: introduction, is in solving formulas that have a large number of disjunctions and hence are hard for
677: any method that is based on solving the various cases separately. The results in figures
678: \ref{fig:table} and \ref{fig:table-new} prove this observation. The results shown in figure \ref{fig:table2}, however, are
679: not conclusive. \tool{bfm} has recently been integrated in the theorem prover C-\tool{prover}
680: \cite{K02}, which means that in the long run additional data concerning the performance of this
681: technique when solving real verification problems will be gathered.
682:
683: Finally, as direction for future research, we note that since both DLA and SAT are NP-complete,
684: there is no complexity argument to rule out the option of finding a polynomial reduction of DLA to
685: SAT. Finding such a reduction will enable to solve larger formulas than can be solved by \tool{bfm}.
686:
687: \bibliographystyle{plain}
688: \bibliography{biblio}
689:
690: \end{document}
691:
692:
693:
694:
695:
696: