Bit vectors and bit operations are proposed for efficient propositional inference. Bit arithmetic has efficient software and hardware implementations, which can be put to advantage in Boolean satisability procedures. Sets of variables are represented as bit vectors and formulae as matrices. Symbolic operations are performed by bit arithmetic. As examples of inference done in this fashion, we describe ground resolution and ground completion.
Boolean satisfiability, though NP-complete, is a problem that is solved on a
daily basis with real-life industrial instances comprising millions of variables
and clauses. See, for example, [
Suppose B is a Boolean formula and p1, . . . , pv are its propositional variables. The Boolean satisfiability (SAT) problem is to find an assignment of truth values (0 and 1) to a subset of the variables, such that the formula becomes a tautology, or else to determine that no such assignment exists, in which case the formula is unsatisfiable.
Formulae are often framed in clausal form. A literal is any variable pj or its
negation pj. A clause c is a (multi-) set of positive and negative literals, intending
their disjunction. A (clausal) formula C is a set or list of clauses, intending their
conjunction.
1.2
Bit arithmetic enjoys efficient software and hardware implementations. These
can be put to great advantage in satisfiability procedures. Sets of variables can
be represented as bit vectors, rather than as (linked) lists, or tries. Formulae
would be represented as matrices, rather than as linked lists or binary decision
diagrams [
There has been considerable work on the use of reconfigurable hardware for SAT
solving in general or for individual instances (e.g. [
The use of bit operations on large bit arrays for the purpose of large-scale propositional inference, as elaborated here, appears to be novel.
The next section shows how formulae are encoded as vectors of bits. As
examples of the use of bit operations, the following two sections consider two
important families of propositional inference, namely, ground resolution and ground
completion. Ground resolution is the resolution rule for variable-free clauses,
as used for SAT in [
A clause c can be represented by two bit vectors c0[1: v] and c1[1: v], where v is the number of bits in the vector, c0[j] = 1 iff the negative literal pj occurs in c, and c1[j] = 1 iff the positive literal pj occurs therein. Thus, a variable pk (or literal pk) is identified with the vector containing a single 1 in position k (or k + v, respectively). Let c also denote the 2v-bit-long concatenation of c0 and c1, symbolized c0⌢c1, and c∗ the reverse concatenation c1⌢c0. To encode a tautological clause “true”, one can add a bit in the 0th position, c[0], to clauses c, and use ⊤ to abbreviate the corresponding vector p0.
The standard set operations will denote the corresponding bit-vector functions. For example, ∩ represents logical-and and ∅ is the zero-vector, which corresponds to the value false. So, if c0 ∩ c1 6= ∅, then c is tautological, as it includes both a literal and its negation. Symmetric-difference (exclusive-or) is ⊕. Set difference can be obtained in two steps when it is not directly available: x \ y = x ∩ y. We will let kck count the number of ones (the “population count”) in vector c. Inequalities of bit vectors treat the low-index bits as most significant. It is customary to also use 0 and 1 for false and true, respectively.
A binomial equation eL = eR between Boolean monomials (products of propositional variables) can likewise be represented as two bit vectors eL[1: v] and eR[1: v], where eL[j] = 1 iff the variable pj occurs in the left side eL and eR[j] = 1 iff it occurs in the right side eR. In this case, the most significant bits eL[0] and eR[0] can conveniently be set to indicate the monomial 0 (false), regardless of the values of other bits (thinking of the zero-bit as indicating a 0-factor). Thus, p0 represents the truth constant false, but so does any vector with its most significant bit on. Accordingly, the truth constant true is denoted by the zero-vector (empty monomial) ∅.
A list C of n clauses c1, . . . , cn may be represented as a pair of n × (v + 1) matrices, C0 and C1, where Cr[i, j] = 1 iff cr[j] = 1 (for r = 0, 1). To refer to i the whole jth column, one can write Cr[∗, j] (r = 0, 1, or blank). All or half of the ith row, Cr[i, ∗], is just cir (r = 0, 1, or blank, for left half, right half, or both halves, respectively). Similarly, a list of n Boolean equations may be represented as a pair of matrices, CL and CR, for left and right sides of equations. 3
A clause is empty, and hence unsatisfiable, if c = ∅ (that is, kck = 0). A clause is a unit if kck = 1, which coerces the truth value of its one literal. A clause is trivial (tautological), and may be deleted, if c0 ∩ c1 6= ∅, since it disjoins a literal and its complement. To delete a clause, we will set its (high-order) 0-bit to 1. Two clauses c and d resolve on pk if c∗ ∩ d = pk, for some (positive or negative) literal pk, producing a new clause (c ∪ d) \ (pk ∪ p∗k). The resultant clause may be empty or a unit, but resolving non-units yields a non-empty clause.
Resolution provers invariably include simplification stages, such as unit propagation and subsumption, which we discuss next. 3.1
A unit clause c propagates and simplifies clause d if c∗ ⊆ d, in which case the
result is d′ = d \ c∗. If the result d′ is empty (d = c∗), the problem is unsatisfiable.
If the result is a unit, then d′ can be used in the same fashion. Binary
constraint propagation (BCP ) is the repeated application of subsumption by units
and unit propagation – until no further simplifications are possible. BCP is a
central component of the Davis-Putnam-Logemann-Loveland backtracking SAT
procedure [
Let n be the number of clauses, and let u[0: 2v] be a bit-vector of length 2v + 1. At the conclusion of the algorithm in Fig. 1, all the units obtained by propagating the clauses of C will be marked in u. The n-step main loop repeats at most v times. An empty clause ci means the problem is unsatisfiable. To delete a row, we set ci := ⊤; it would be enough to let ci[0] := 1. The matrix can be compacted by removing the deleted rows (at any juncture) and/or the columns marked in u (after any complete pass). 3.2
Clause c subsumes clause d if c ⊆ d, in which case d is superfluous. For this to be the case, we must have c ≤ d, as binary numbers, but this is an insufficient condition. Using standard operations, c ⊆ d iff c ∪ d = d.
Subsumption is more expensive than unit propagation and should normally be preceded by BCP. It can be implemented like sorting, with the addition of u := ∅ b := true while b do b := false for i := 1, . . . , n do if u ∩ ci = ∅ then ci := ci \ u∗ if ci = ∅ then fail if kcik = 1 then u := u ∪ ci
b := true
else ci := ⊤
checking whether the smaller of any pair subsumes the larger, in which case, the
larger is deleted – for a cost of O(n lg n) vector-operations to check all clauses.
Deleted rows should be removed. For an n2 version, `a la selection sort, see Fig. 2.
Subsumption is often not cost-effective in standard implementations, but might
be in this context. (Satellite [
Other implementations of these algorithms, taking advantage of matrix
operations, are conceivable.
The original Davis-Putnam (DP) procedure resolves clauses, variable by
variable [
We are interested in the ground (variable-free) case of completion, where the
operations are associative and commutative [
b := true
A clause is Horn if it has at most one positive literal. A Horn clause p0 ∨ ¬p1 ∨
· · · ∨ ¬pn is equivalent to the binomial equation p0p1 · · · pn = p1 · · · pn; a negative
Horn clause ¬p1 ∨ · · · ∨ ¬pn is equivalent to the monomial equation p1 · · · pn = 0.
See [
Two equations ei and ej are critical iff eiL ∩ ejL 6= ∅. The critical equation
(or critical pair) is eL = eR, where eL := ejL \ eiL ∪ eiR and eR := eiL \ ejL ∪ ejR.
Critical equations may need to be oriented. Knuth-Bendix (KB) completion
(or the analogous Gr¨obner basis construction [
In this manner, completion serves as the inference engine, generating critical
pairs from the equational representation of Horn clauses, as shown in Fig. 4.
A major component of completion is simplification, akin to demodulation [
An oriented equation eL = eR is unitary and can be used to simplify in any of the following three cases: – Positive Unit. If eR = ∅, then the equation signifies eL = 1 (since we agreed in Sect. 2 to interpret ∅ as truth). It follows that pi = 1 for every pi ∈ eL. Apply eR = ∅ to a monomial m by removing the (superfluous) positive bits: m := m \ eR. – Negative Unit. If keLk = 1 and eR[0] = 1, then pk = 0 for the pk ∈ eL.
Apply pk = 0 by zeroing any monomial in which it appears: if m[k] then m[0] := 1. – Unit Equivalence. If keLk = keRk = 1 and eL[0] = eR[0] = 0, then pk = pj for the pk ∈ eL and pj ∈ eR. Apply pk = pj by replacing occurrences of pk with pj : if m[k] then m[j] := 1. i := 1 k := 1 while k ≤ v ∧ i ≤ n do m := i while m ≤ n ∧ ¬cm[k] do m := m + 1 if m ≤ n then cm :=: ci for j := 1, . . . , i − 1, m + 1, . . . , n do
if cj[k] then cj := cj ⊕ ci i := i + 1 k := k + 1 The results of such unit simplifications can propagate as in resolution.
More generally, an equation eL = eR can be used to simplify a monomial m provided all the variables in eL appear in m, that is, when eL ⊆ m. The rewrite step is the assignment m := m \ eL ∪ eR. If we use the 0-bit to signify the term 0, as explained above, then reducing products to 0 works as expected.
The lexicographic ordering of monomials is ordinary bit-string inequality. An equation c needs to reoriented if eR > eL, which may transpire after reducing a left side. Other orderings are possible.
To inter-reduce a system C of equations, applying all equations to all
equations, as much as possible, first sort C in ascending order according to
hkeRk − keLk, eL, e1i and then apply the algorithm in Fig. 5. The idea is that
reducing with a “rewrite rule” ℓ → r decreases the binary value of the string
it is applied to by kℓk − krk, and, long range, one wants to maximize the
decreases obtained with each reduction, so as to converge as quickly as possible.
This na¨ıve program can presumably still require exponentially many vector
operations, but hopefully much better algorithms for inter-reduction can be devised
(compare the non-commutative case [
We represent an equation P = 0 as a bit vector c of length v+1, where c[k] = 1 iff pk is a summand in P and p0 is the constant 1. Adding (or subtracting) a linear equation c to d is just d := d ⊕ c. A standard quadratic (vn vector operations) Gaussian elimination procedure is given in Fig. 6.
When (after elimination, say) kck ≤ 2, the equation c is unitary and is of one of the following three forms: pk = 0, pk = 1, or pk = pj, for some k ≥ 1 and 1 ≤ j 6= k.
LOAD 0, ci1 OR 0, cj1 LOAD 2, ci1 AND 2, cj0 DIFF 0, 2
STORE 0, c0
For non-Horn clauses, one needs also to incorporate negation in some form.
The BinLin representation of propositional formulae, proposed in [
Most of the bit-vector operations used in the above sections are readily available on digital computers. Some processors, even way back to the IBM Stretch, provide a hardware instruction for the number of ones in a machine word; in any case, computing kck requires only a few machine instructions [2, No. 169]. Most operations are also available in many software languages (e.g. C). They are all easy to implement in general-purpose or special-purpose hardware.
For example, resolving two single-word (or double-word – for machines with double-word operations) clauses requires approximately 12 machine instructions. Thus v variables require 12⌈v/w⌉ instructions on a w-bit machine. For example, if w = 64 and v = 1000, fewer than 200 machine instructions are needed. See Fig. 7. This should be contrasted with the large number of machine operations used in a pointer-based implementation.
For large (but presumably sparse) vectors, (iterated) summary bits should
prove helpful. (The summary bit for a subvector x is 0 iff x = 0.) Column
operations, such as erasing all occurrences of a true propositional variable, may
be sped up by also maintaining transpose matrices [
Industrial-strength problems can easily involve hundreds of thousands of variables and millions of clauses. The storage requirements for a bit matrix of that size is in the hundreds-of-gigabyte range. Given enough storage, full-fledged n lg n subsumption would take a few minutes on a 5000 MIPS 64-bit machine.
Davis-Putnam resolution is a saturation-based methods for checking propositional satisfiability. The original set of clauses is satisfiable if and only if resolution terminates without having derived the empty clause. Similarly, KnuthBendix completion derives the contradiction 1 = 0 if and only if the input clauses are unsatisfiable. Thus, both methods (Figs. 3 and 4) repeatedly add rows to the matrices of formulae.
Saturation is often considered too costly in practice. Instead, a backtrack
search [
Similarly, a recursive-learning intersection-based method [
The algorithms given here are readily adaptable to highly parallel vector or array architectures. Experiments with simulations are needed to evaluate their practical feasibility.
I thank Guan-Shieng Huang for many ideas, discussions and vegetarian meals.