Propositional logic is the main ingredient used to build up SAT solvers which have gradually become powerful tools to solve a variety of important and complicated problems such as planning, scheduling, and verifications. However further uses of these solvers are subject to the resulting complexity of transforming counting constraints into conjunctive normal form (CNF). This transformation leads, generally, to a substantial increase in the number of variables and clauses, due to the limitation of the expressive power of propositional logic. To overcome this drawback, this work extends the alphabet of propositional logic by including the natural numbers as a means of counting and adjusts the underlying language accordingly. The resulting representational formalism, called pseudo-propositional logic, can be viewed as a generalization of propositional logic where counting constraints are naturally formulated, and the generalized inference rules can be as easily applied and implemented as arithmetic.
2
Azizi-Sultan Definition 1. Let P = {p, q, · · · } be a finite or countably infinite set of propositional symbols andN be the natural numbers. The alphabet A underlying the language of pseudo-propositional formulas is defined as A = P ∪ N ∪ {¬, +, (, )}, where {¬, +, (, )} resemble the negation, addition, opening and closing punctuation symbols, respectively.
Definition 2. The language or formulas of pseudo-propositional logic, symbolized by F , is defined recursively as follows: • If p ∈ P and n ∈ N then np ∈ F , called prime formula. • If α, β ∈ F , then (α + β ), ¬α ∈ F .
• Propositional variables or symbols will be denoted by p, q, . . . , formulas by α, β , ϕ, . . . , set of formulas by F, G, . . . , and set of queries, which will be defined in section 4, by F , G, . . . , where these letters may also be indexed.
• As in arithmetical terms, parenthesis are omitted whenever it is possible. 3
A proposition can have only one of the truth values, true or false. Conveniently to the context of this
work, these values are represented by (
Definition 3. An interpretation I is a subset of P represented by the mapping φ : P → {(
I = {p ∈ P | φ (p) = (
Thus, the interpretation I is the subset of P containing only those propositional symbols that are mapped
to (
Recursively, the mapping φ can be extended to become from the set of formulas F to M = Z2
which is the meaning set in the context of pseudo-propositional logic. In order to do so the following
two functions are prerequisites:
(
1This addition is easily distinguished from the addition of formulas in definition 1. 1) Recursion base. Recall that if ϕ is an atom then ϕ = n p for some n ∈ N and p ∈ P. Consequently the recursion base reads
I(ϕ) = I(n p) = n φ (p). 2) Recursion steps.
I(α) = (¬∗(I(β ))
I(β1) + I(β2) if α is of the form ¬β , if α is of the form β1 + β2.
Definition 4. Two formulas α and β are equivalent, in symbols α ≡ β , iff I(α) = I(β ) for every interpretation I.
Example 1. For any α, β ∈ F , it is obvious that α + β ≡ β + α and ¬¬α ≡ α.
Proposition 1. For any α, β ∈ F , the equivalence ¬(α + β ) ≡ ¬α + ¬β holds.
Proof. Given an interpretation I suppose that I(α) = (n, l) and I(β ) = (m, k).
I(¬(α + β )) = ¬∗ I(α + β ) = ¬∗(I(α) + I(β )) = ¬∗((n, l) + (m, k))
= ¬∗(n + m, l + k) = (l + k, n + m).
I(¬α + ¬β ) = I(¬α) + I(¬β ) = ¬∗I(α) + ¬∗I(β )) = ¬∗(n, l) + ¬∗(m, k) = (l, n) + (k, m) = (l + k, n + m).
Thus I(¬(α + β )) = I(¬α + ¬β ) for any given interpretation I. Proposition 2. If p ∈ P and n, m ∈ N then (n p + m p) ≡ (n + m)p.
I(np + mp) = I(np) + I(mp) = nφ (p) + mφ (p) = (n + m)φ (p) = I((n + m)p).
α1, α2, β1, β2 ∈ F ,
α1 ≡ α2, β1 ≡ β2 ⇒ ¬α1 ≡ ¬α2, α1 + β1 ≡ α2 + β2.
For this reason the replacement theorem holds. It enables one to substitute a subformula β , of a formula
α, by an equivalent one without altering the meaning of α. If we let α [β1/β2] denote the formula that
is obtained from α by substituting every occurrence of β1 by β2, the replacement theorem becomes as
follows:
Theorem 1. If the formulas β1 and β2 are equivalent, so are α and α [β1/β2].
(
α = (α1 + α2) ≡ α1 [β1/β2] + α2 [β1/β2] = α [β1/β2] .
by Proposition 1, the replacement theorem transforms every formula into an equivalent one which is a normal form. This is actually interesting from an implementational point of view, as efficiency might be gained by restricting the inference rules to the mentioned normal form.
4
Definition 5. For a given formula ϕ ∈ F and an n ∈ N, in pseudo-propositional logic we are interested in finding an answer to the query: is there an interpretationI such that I(ϕ) = (m, l) where m ≥ n. Every formula ϕ combined with a natural number n forms a query ϕ(n). The set of all possible queries is denoted by Q. That is Q = {ϕ(n) : ϕ ∈ F , n ∈ N}.
Definition 6. It is said that an interpretation I is a model for a query ϕ(n), in symbols I |= ϕ(n), iff I(ϕ) = ( n¯, l) with n¯ ≥ n. Considering a set of queries Q, it is said that I is a model for Q, and symbolised by I |= Q, iff I |= ϕ(n) for every query ϕ(n) ∈ Q.
Proposition 3. Let α(n), ϕ(m) ∈ Q. If I is an interpretation such that I |= α(n) and I |= ϕ(m), then I |= (α + ϕ)(n+m).
Proof. Since I |= α(n) and I |= ϕ(m), this implies that I(α) = ( n¯, l), n¯ ≥ n and I(ϕ) = ( m¯, k), m¯ ≥ m.
I(α + ϕ) = I(α) + I(ϕ) = ( n¯, l) + ( m¯, k) = ( n¯ + m¯, l + k). Since n¯ + m¯ ≥ n + m we conclude that I |= (α + ϕ)(n+m).
• It is said that ϕ(n) (resp. Q) is satisfiable iff there exists an interpretation I such that I |= ϕ(n) (resp. I |= Q). • It is said that ϕ(n) (resp. Q) is unsatisfiable iff for every interpretation I we have I 6|= ϕ(n) (resp.
I 6|= Q).
4 Azizi-Sultan 5
Definition 7. Q is a logical consequence of F , written F |= Q, if I |= Q for every interpretation I that is a model for F . In short, I |= F ⇒ I |= Q for all interpretations I.
Definition 8. If F |= Q and Q |= F then we say F and Q are semantically equivalent. We denote this by F ≡ Q.
In this work, F |= α(n) (resp. α(n) |= F ) will mean F |= {α(n)} (resp. {α(n)} |= F ). More generally, we write F |= α(n1), α2(n2), . . . , αk(nk) (resp. α(n1), α2(n2), . . . , αk(nk) |= F ) instead of F |= 1 1 {α1(n1), α2(n2), . . . , αk(nk)} (resp. {α1(n1), α2(n2), . . . , αk(nk)} |= F ), and more briefly we write F , α(n) |= ϕ(m) instead of F ∪ {α(n)} |= ϕ(m). Analogous notation will be used regarding semantic equivalence. Note 1. Proposition 3 can be rewritten as follows:
α(n), ϕ(m) |= (α + ϕ)(n+m).
Example 2. Let Q = {ϕ(i) : i = 1, 2, . . . , n − 1}. Moreover suppose that I |= ϕ(n). This means that I(ϕ) = ( n¯, l) where n¯ ≥ n > i. Consequently, I |= ϕ(i) for all i < n. Thus ϕ(n) |= Q. Lemma 1. Let ϕ be a formula and n > 1 then (ϕ + p + ¬p)(n) |= ϕ(n−1).
Proof. Suppose I |= (ϕ + p + ¬p)(n). This means that I(ϕ + p + ¬p) = I(ϕ) + (
Theorem 2. If ϕ ∈ F and n > m¯ ≥ m, then the following consequence holds: (ϕ + m¯p + ¬(mp))(n) |= (ϕ + ( m¯ − m)p)(n−m).
Theorem 3. If the formulas β1 and β2 are equivalent, so are the queries α(n) and (α [β1/β2])(n) for every n ∈ N.
Proof. Suppose that I |= α(n). This means that I(α) = ( n¯, l) where n¯ ≥ n. Since β1 ≡ β2, from Theorem 1 it follows that α ≡ α [β1/β2]. Thus I(α) = I(α [β1/β2]) = ( n¯, l) where n¯ ≥ n. Thus I |= (α [β1/β2])(n). We conclude that α(n) |= (α [β1/β2])(n). Taking into account that (α [β1/β2]) [β2/β1] = α, the consequence (α [β1/β2])(n) |= α(n) follows analogously.
any query into an equivalent one which is a normal form. Thus to solve the satisfiability problem in pseudo-proposition logic it suffices to consider only the sets of queries that are normal form.
Theorem 4. If F |= Q and for every interpretation I which models Q we have I 6|= F , then F is unsatisfiable. Proof. Suppose that F is satisfiable. This means that there exists an interpretation I such that I |= F . Consequently, I |= Q since F |= Q. This contradicts the theorem’s hypothesis.
one to use proper inference rules to find a simpler set of queriesQ such that F |= Q. Now it is enough to look for a solution for F among only those solutions that solve Q.
solve the SAT problem of propositional logic. Actually pseudo-propositional logic can be viewed as a generalization of propositional logic. This is justified by the fact that every formula or sentence S in propositional logic can be represented equivalently by a set of queries Q in pseudo-propositional logic. To see this let P = {p1, p2, p3, · · · } be our set of propositional symbols and let the literal li be either pi or its negation. Moreover, suppose that converting the sentence S into its CNF results in the set of clauses {Ci : i = 1, 2, . . . , n} where each clause Ci is the disjunctions of a set of literals {l j : j ∈ Ji ⊂ N}.
can be equivalently represented in pseudo-propositional logic by the query
n n SCNF = ^ Ci = ^ i=1 i=1 j∈Ji
! _ l j .
Ci = _ l j
j∈Ji
Qi =
∑ l j
j∈Ji
!(
If we let Q = {Qi : i = 1, 2, . . . , n} then the sentence S, which is equivalent to SCNF , is satisfiable iffQ is satisfiable. Moreover, an interpretationI is a model for Q iff I is a model for S. A detailed example is presented in the sequel. 6
This section is not meant to present an algorithm that competes with the current SAT solvers. It just gives
an idea of how one can make use of pseudo-propositional logic to solve problems such as SAT. This is
actually done in three steps. Intuitively, the first step involves transforming the given SAT instance into
the corresponding set of queries F in pseudo-propositional logic. The second step reprocesses the set F
using inference rules to generate a proper compact set of queries Q such that F |= Q. Finally, apply a
backtracking procedure to find a solution forQ and check if it satisfies the original SAT instance. The
final step is repeated until a solution is found or the problem is unsatisfiable otherwise.
Example 3. Consider the following CNF instance:
This can be equivalently represented by a set of queries in pseudo-propositional logic as follows:
F = {
(x1 + x2 + x3)(
Taking into account Proposition 2 while adding each consecutive homogeneous2 couple of queries in F results in
F 1 = {
(2x1 + 2x2 + x3 + x4)(
(¬x2 + ¬2x3 + ¬x4)(
One can easily conceive that F ≡ F 1 which shows how encoding in pseudo-propositional logic is much more compact than it is in CNF. Although it is not always the case that F ≡ F 1 but we, at least, know from Proposition 3 that F |= F 1. If we add again and again each consecutive homogeneous couple of queries in F 1, we finally get
F 2 = {(3x1 + 3x2 + 3x3 + 3x4)(
I1 = {x1, x2}, I2 = {x1, x3}, I3 = {x1, x4},
I4 = {x2, x3}, I5 = {x2, x4}, I6 = {x3, x4}.
Since non of these interpretations model F , according to Theorem 4 F and consequently the original SAT instance are unsatisfiable. 7
This work has introduced pseudo-propositional logic, a generalization of propositional logic with considerable extension of its expressive power. This enables the resulting representational formalism to encode counting constraints as well as SAT instances naturally, and much more compact than the encoding using CNF. The inference rules of the resulting pseudo-propositional logic, besides their Boolean nature, have arithmetical flavour allowing for easy implementation. Moreover, as it was seen in Example 3, applying backtracking on the final entailed set of queries may yield simultaneous multi-variables guesses, eliminating considerable parts of the search tree that have not been yet explored and hence allowing for potential improvement in terms of time complexity. Another promising improvement is subject to a further investigation on how to construct a compact proper final entailed set of queries which maximizes the eliminated part of the search tree and at the same time captures all possible solutions of the original problem. 8
I would like to thank Prof. Steffen Ho¨lldobler, Director of the International Center for Computational Logic, Dresden, Germany. I have learned from him how to rationalise logically rather than just thinking mathematically. Without his influence this work would not have been established.
2containing literals of the same polarity