=Paper=
{{Paper
|id=Vol-2095/paper1
|storemode=property
|title=Pseudo-Propositional Logic
|pdfUrl=https://ceur-ws.org/Vol-2095/paper1.pdf
|volume=Vol-2095
|authors=Ahmad-Saher Azizi-Sultan
|dblpUrl=https://dblp.org/rec/conf/cade/Azizi-Sultan18
}}
==Pseudo-Propositional Logic==
https://ceur-ws.org/Vol-2095/paper1.pdf
Pseudo-Propositional Logic
Ahmad-Saher Azizi-Sultan
Taibah University, Medinah Munawwarah, Saudi Arabia
sultansaher@hotmail.com
Abstract
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 com-
plexity of transforming counting constraints into conjunctive normal form (CNF). This transforma-
tion 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 ex-
tends 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.
1 Introduction
During the last few decades SAT solvers have gained considerable advances and become a tool suitable
for attacking more and more practical problems arising in different areas such as formal verification
[1, 2, 12], planning [9, 11], scheduling [8], etc. Most of these solvers, if not all, are a variety of Davis-
Putnam-Logemann-Loveland (DPLL) algorithm [4, 5] which is based on blind branch and backtrack
techniques that explore the search space exhaustively until a solution is found. As SAT is one of the
canonical NP-complete problems [3], generally any exhaustive search algorithm results in impractical
excessive time complexity.
In order to reduce the size of the search tree, modern SAT solvers such as Chaff, BerkMin, and
MiniSAT have equipped the DPLL algorithm with pruning techniques known as backjumping, conflict-
driven lemma learning, and restarts [6, 7, 10]. Although these techniques were able to reduce the search
space, the major drawback of having blind control over the search process remains.
To mine solutions efficiently, there is a need for a tool that could scan over the search field and detect
the spots that potentially contain solutions. Unfortunately, the limited expressive power of propositional
logic does not allow for such a tool to be built-in. Furthermore, the input of SAT solvers is, usually,
a formula in its CNF. However, many applications contain counting constraints and transforming these
constraints into CNF generally leads to a substantial increase in the number of variables and clauses.
This is again due to the lack of expressive tools in the underlying propositional language.
This work takes the liberty to extend the alphabet of propositional logic by including the natural
numbers as a means of counting and adjusts the underlying language accordingly. The resulting rep-
resentational formalism, which we can conveniently agree to call pseudo-propositional logic, may be
viewed as a generalization of propositional logic, where counting constraints are naturally formulated
and at the same time the Boolean nature of the propositional variables is kept preserved. This allows
for encoding counting constraints as well as SAT instances much more compact than if it is encoded
using CNF. Furthermore, the generalized inference rules are as easily applied and implemented as arith-
metic. In such a case, equipping backtracking procedures with some combinatorial techniques allows
for assigning truth values to a variety of propositional variables simultaneously. This leads to easily
detecting the branches of the search tree that possibly contain solutions, or at least prune the useless
ones, allowing for possible improvement in terms of calculation complexity.
ARQNL 2018 26 CEUR-WS.org/Vol-2095
Pseudo-Propositional Logic Azizi-Sultan
2 Language
Definition 1. Let P = {p, q, · · · } be a finite or countably infinite set of propositional symbols and N
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 .
A prime formula or its negation is called a literal. A formula which is a literal or an addition of two
or more literals is said to be in normal form. A subformula of a formula α is a substring occurring in α,
which is itself a formula.
Before proceeding further, let us agree upon the following two conventions to ease readability:
• 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 Semantics
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 (1, 0) for true and (0, 1) for false. More formally, this is rephrased
by the definition of interpretation.
Definition 3. An interpretation I is a subset of P represented by the mapping φ : P → {(1, 0), (0, 1)}
which is defined as follows: (
(1, 0) if p ∈ I,
φ (p) =
(0, 1) if p ∈
/ I.
Thus, the interpretation I is the subset of P containing only those propositional symbols that are mapped
to (1, 0) under φ . That is
I = {p ∈ P | φ (p) = (1, 0)}. (1)
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:
• Negation ¬∗ : M → M where ¬∗ (n, m) = (m, n).
• Addition1 + : M × M → M , where +((n, m), (k, l)) = (n + k, m + l).
Yet every interpretation I defines recursively its own mapping I : F → M as follows:
1 This addition is easily distinguished from the addition of formulas in definition 1.
2
27
Pseudo-Propositional Logic Azizi-Sultan
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(β )) if α is of the form ¬β ,
I(α) =
I(β1 ) + I(β2 ) if α is of the form β1 + β2 .
After assigning meanings to formulas, one can investigate how formulas are related to each other
according to their meanings.
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).
On the other hand,
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.
Proof. Let I be an interpretation then,
I(np + mp) = I(np) + I(mp) = nφ (p) + mφ (p) = (n + m)φ (p) = I((n + m)p).
Obviously, ≡ is an equivalence relation. Moreover, it is a congruence relation on F , i.e., for all
α1 , α2 , β1 , β2 ∈ F ,
α1 ≡ α2 , β1 ≡ β2 ⇒ ¬α1 ≡ ¬α2 , α1 + β1 ≡ α2 + β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 ].
3
28
Pseudo-Propositional Logic Azizi-Sultan
Proof by induction on α. Suppose α is a prime formula. Then, for both cases α = β1 and α 6= β1
we clearly have α ≡ α [β1 /β2 ]. Now let α = α1 + α2 . If α = β1 then trivially α ≡ α [β1 /β2 ] holds.
Otherwise α [β1 /β2 ] = α1 [β1 /β2 ] + α2 [β1 /β2 ]. By the induction hypothesis we have α1 ≡ α1 [β1 /β2 ]
and α2 ≡ α2 [β1 /β2 ]. According to the congruence property 2 one concludes that
α = (α1 + α2 ) ≡ α1 [β1 /β2 ] + α2 [β1 /β2 ] = α [β1 /β2 ] .
The induction steps for ¬ follows analogously.
Taking into account that one can eliminate all negation signs except those in front of prime formulas
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.
After assigning meaning to formulas and seeing how they are related, it is time to consider counting
constraints which are represented by queries defined in the upcoming section.
4 Queries and Models
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 interpretation I 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}.
Having defined queries, modelling becomes straightforward. Simply, it defines relations between
interpretations and queries.
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 .
It is time now to start reasoning which is as easy as arithmetic. The coming proposition is an ideal
example of reasoning in pseudo-propositional logic.
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.
Thus
I(α + ϕ) = I(α) + I(ϕ) = (n̄, l) + (m̄, k) = (n̄ + m̄, l + k).
Since n̄ + m̄ ≥ n + m we conclude that I |= (α + ϕ)(n+m) .
One can easily conceive that satisfiability in pseudo-propositional logic concerns queries rather than
formulas.
• 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 ).
Consequently the equivalence relation is lifted to the level of queries as demonstrated below.
4
29
Pseudo-Propositional Logic Azizi-Sultan
5 Consequence and Equivalence
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
(n ) (n ) (n ) (n ) (n ) (n )
generally, we write F |= α1 1 , α2 2 , . . . , αk k (resp. α1 1 , α2 2 , . . . , αk k |= F ) instead of F |=
(n ) (n ) (n ) (n ) (n ) (n )
{α1 1 , α2 2 , . . . , αk k } (resp. {α1 1 , α2 2 , . . . , αk k } |= 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(ϕ) + (1, 1) = (n̄, l) where
n̄ ≥ n and l ≥ 1. Since (Z2 , +) is an abelian group we conclude that I(ϕ) = (n̄ − 1, l − 1). That is
I |= ϕ (n−1) .
An obvious generalization and a direct consequence of lemma 1 is the resolution theorem which
reads:
Theorem 2. If ϕ ∈ F and n > m̄ ≥ m, then the following consequence holds:
(ϕ + m̄p + ¬(mp))(n) |= (ϕ + (m̄ − m)p)(n−m) .
To keep things from being complicated before going any further, the following theorem must be
proven.
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 conse-
quence (α [β1 /β2 ])(n) |= α (n) follows analogously.
If we call a query with a normal form formula a normal form query, then theorems 1 and 3 transform
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.
Finally, to start applying pseudo-propositional logic to solve real-world problems, such as SAT for
example, one more theorem is needed.
Theorem 4. If F |= Q and for every interpretation I which models Q we have I 6|= F , then F is unsat-
isfiable.
5
30
Pseudo-Propositional Logic Azizi-Sultan
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.
Informally speaking, before solving a SAT problem for a given set of queries F , Theorem 4 tempts
one to use proper inference rules to find a simpler set of queries Q such that F |= Q . Now it is enough
to look for a solution for F among only those solutions that solve Q.
Furthermore any algorithm that solves SAT problem in pseudo-propositional logic can be used to
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}.
If we denote to S in its CNF by SCNF we conclude that
!
n
^ n
^ _
SCNF = Ci = lj .
i=1 i=1 j∈Ji
Clearly each clause Ci which has the form
_
Ci = lj
j∈Ji
can be equivalently represented in pseudo-propositional logic by the query
!(1)
Qi = ∑ lj .
j∈Ji
If we let Q = {Qi : i = 1, 2, . . . , n} then the sentence S, which is equivalent to SCNF , is satisfiable iff Q
is satisfiable. Moreover, an interpretation I is a model for Q iff I is a model for S. A detailed example is
presented in the sequel.
6 Application on SAT
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 for Q 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:
x1 ∨ x2 ∨ x3 , ¬x1 ∨ ¬x2 , ¬x1 ∨ ¬x3 , ¬x2 ∨ ¬x3 ,
x1 ∨ x2 ∨ x4 , ¬x1 ∨ ¬x2 , ¬x1 ∨ ¬x4 , ¬x2 ∨ ¬x4 ,
x1 ∨ x3 ∨ x4 , ¬x1 ∨ ¬x3 , ¬x1 ∨ ¬x4 , ¬x3 ∨ ¬x4 ,
x2 ∨ x3 ∨ x4 , ¬x2 ∨ ¬x3 , ¬x2 ∨ ¬x4 , ¬x3 ∨ ¬x4 .
6
31
Pseudo-Propositional Logic Azizi-Sultan
This can be equivalently represented by a set of queries in pseudo-propositional logic as follows:
F ={ (x1 + x2 + x3 )(1) , (¬x1 + ¬x2 )(1) , (¬x1 + ¬x3 )(1) , (¬x2 + ¬x3 )(1) ,
(x1 + x2 + x4 )(1) , (¬x1 + ¬x2 )(1) , (¬x1 + ¬x4 )(1) , (¬x2 + ¬x4 )(1) ,
(x1 + x3 + x4 )(1) , (¬x1 + ¬x3 )(1) , (¬x1 + ¬x4 )(1) , (¬x3 + ¬x4 )(1) ,
(x2 + x3 + x4 )(1) , (¬x2 + ¬x3 )(1) , (¬x2 + ¬x4 )(1) , (¬x3 + ¬x4 )(1) }.
Taking into account Proposition 2 while adding each consecutive homogeneous2 couple of queries in F
results in
F1 = { (2x1 + 2x2 + x3 + x4 )(2) , (¬2x1 + ¬x2 + ¬x3 )(2) , (¬x1 + ¬2x2 + ¬x3 )(2) ,
(¬x1 + ¬x2 + ¬2x4 )(2) , (x1 + x2 + 2x3 + 2x4 )(2) , (¬2x1 + ¬x3 + ¬x4 )(2) ,
(¬x2 + ¬2x3 + ¬x4 )(2) , (¬x2 + ¬x3 + ¬2x4 )(2) }.
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 )(4) , (¬6x1 + ¬6x2 + ¬6x3 + ¬6x4 )(12) },
as a logical consequence of F 1 . By backtracking and propagation, F 2 has only the following six inter-
pretations:
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 Conclusion and Further Work
This work has introduced pseudo-propositional logic, a generalization of propositional logic with con-
siderable extension of its expressive power. This enables the resulting representational formalism to en-
code 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, ap-
plying 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 Acknowledgments
I would like to thank Prof. Steffen Hö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.
2 containing literals of the same polarity
7
32
Pseudo-Propositional Logic Azizi-Sultan
References
[1] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using sat procedures
instead of bdds. In Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, DAC ’99,
pages 317–320, New York, NY, USA, 1999. ACM.
[2] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without
bdds. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and
Analysis of Systems, TACAS ’99, pages 193–207, London, UK, UK, 1999. Springer-Verlag.
[3] Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd Annual ACM
Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151–158, 1971.
[4] Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Com-
mun. ACM, 5(7):394–397, 1962.
[5] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201–215,
1960.
[6] Niklas Eén and Niklas Sörensson. An extensible sat-solver. In Theory and Applications of Satisfiability
Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected
Revised Papers, pages 502–518, 2003.
[7] Eugene Goldberg and Yakov Novikov. Berkmin: A fast and robust sat-solver. Discrete Applied Mathematics,
155(12):1549 – 1561, 2007. SAT 2001, the Fourth International Symposium on the Theory and Applications
of Satisfiability Testing.
[8] Carla P. Gomes, Bart Selman, Ken McAloon, and Carol Tretkoff. Randomization in backtrack search: Ex-
ploiting heavy-tailed profiles for solving hard scheduling problems. In Proceedings of the Fourth International
Conference on Artificial Intelligence Planning Systems, Pittsburgh, Pennsylvania, USA, 1998, pages 208–213,
1998.
[9] Henry Kautz and Bart Selman. Pushing the envelope: Planning, propositional logic, and stochastic search.
In Proceedings of the Thirteenth National Conference on Artificial Intelligence - Volume 2, AAAI’96, pages
1194–1201. AAAI Press, 1996.
[10] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering
an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas,
NV, USA, June 18-22, 2001, pages 530–535, 2001.
[11] Stuart J. Russell and Peter Norvig. Artificial intelligence - a modern approach, 2nd Edition. Prentice Hall
series in artificial intelligence. Prentice Hall, 2003.
[12] Miroslav N Velev and Randal E Bryant. Effective use of boolean satisfiability procedures in the formal
verification of superscalar and vliw microprocessors. Journal of Symbolic Computation, 35(2):73 – 106,
2003.
8
33