Propositional Logic: Tableau Method and Reachability Problem

Author

Your Name

Published

February 5, 2025

Introduction

This lecture continues the discussion on propositional logic, focusing on the tableau method as an alternative algorithm for determining satisfiability. We will explore its practical efficiency compared to traditional methods, such as exhaustive search, and its connection to disjunctive normal form (DNF). Additionally, we will introduce the reachability problem as an application example, demonstrating how to reduce it to a satisfiability problem in propositional logic. The reachability problem will be a recurring theme throughout the course as a way to illustrate the concepts of verification and planning.

Recap of Propositional Logic

Last week, we introduced propositional logic, a basic logic with Boolean connectives and variables. We studied two fundamental problems:

Model Checking (Evaluation Problem): Determines if a formula is true under a given interpretation. This problem is P-complete (polynomial time complete).
Satisfiability Problem (SAT): Determines if there exists an interpretation that makes a formula true. This problem is NP-complete (non-deterministic polynomial time complete). The famous SAT problem is NP-complete.

We also explored normal forms, including:

Negation Normal Form (NNF): Negations are pushed inwards to appear only in front of literals. A literal is a propositional letter or its negation.
Conjunctive Normal Form (CNF): A conjunction of clauses, where each clause is a disjunction of literals. In other words, conjunctions are outside, followed by disjunctions, and then negations.
Disjunctive Normal Form (DNF): A disjunction of clauses, where each clause is a conjunction of literals. In other words, disjunctions are outside, followed by conjunctions, and then negations.

We discussed how any formula (without the double implication operator, which is problematic) can be efficiently transformed into NNF while preserving equivalence. We also saw that a formula can be transformed into CNF in polynomial time while preserving satisfiability (equisatisfiability), potentially introducing new variables. This transformation is known as Tseitin transformation. The existence of this transformation proves that CNF-SAT is also NP-complete.

Disjunctive Normal Form and Satisfiability

Unlike CNF SAT, DNF SAT is in P. This means there exists a polynomial-time algorithm to solve it.

Theorem 1.

DNF SAT is in P.

Proof. Proof. A DNF formula is a disjunction of clauses, where each clause is a conjunction of literals. To check if a DNF formula is satisfiable, we can check each clause separately. A clause is satisfiable if it does not contain a contradiction (e.g., $P$ and $\neg P$). If any clause is satisfiable, the entire DNF formula is satisfiable. This can be done in polynomial time, specifically, in time proportional to the number of clauses times their length. ◻

Because of 1, we cannot have a polynomial reduction from SAT to DNF-SAT that preserves equisatisfiability, unlike the reduction from SAT to CNF-SAT.

Tableau Method

The tableau method is an alternative algorithm for satisfiability that is often more efficient in practice than exhaustive search. It constructs a tree called a tableau, where each node represents a set of formulas. The classical algorithm for satisfiability has complexity $2^n$, where $n$ is the number of propositional letters.

Idea

Instead of guessing an interpretation from the bottom (assigning values to variables), the tableau method guesses pieces of the formula from the top that should be true. It recursively breaks down these pieces until it reaches literals, revealing a satisfying assignment if one exists. The idea is that, instead of making a non-deterministic choice for every variable in the formula, we make a non-deterministic choice for every disjunct in the formula.

Tableau Construction

A tableau is a tree where each node contains a set of formulas. It is important to note that this tree is different from the tree that represents the formula. The root contains the initial formula. The tableau is expanded using the following rules:

Initialization: Start with a single node (root) containing the input formula in NNF.
Expansion:
- Choose a leaf node and a formula $\alpha$ within its set.
- Conjunction Rule: If $\alpha = \beta \land \beta'$, append a new child to the leaf, labeled with the set where $\alpha$ is replaced by $\beta, \beta'$. In other words, the $\land$ is replaced by a comma.
- Disjunction Rule: If $\alpha = \beta \lor \beta'$, add two children to the leaf. One child is labeled with the set where $\alpha$ is replaced by $\beta$, and the other with the set where $\alpha$ is replaced by $\beta'$. This is the only rule that creates branches.

Blocked Leaves

A leaf is blocked if it contains a contradiction (e.g., $P$ and $\neg P$). Blocked leaves are not expanded further.

Termination

The algorithm terminates when all leaves are blocked, or a satisfiable leaf (no contradictions) is found.

If all leaves are blocked, the original formula is unsatisfiable.
If a satisfiable leaf is found, the original formula is satisfiable. A satisfying assignment can be derived from the literals in the leaf by setting each literal to true.

Example

Consider the formula $(P \lor \neg Q) \land \neg P$.

Start with the root: $\{(P \lor \neg Q) \land \neg P\}$.
Apply the conjunction rule: $\{P \lor \neg Q, \neg P\}$.
Apply the disjunction rule:
- Left child: $\{P, \neg P\}$ (blocked)
- Right child: $\{\neg Q, \neg P\}$ (satisfiable)

The tableau has a satisfiable leaf $\{\neg Q, \neg P\}$. Thus, the formula is satisfiable, and a satisfying assignment is $P = \text{false}$, $Q = \text{false}$.

We can represent this as a tree using TikZ:

Tableau for ((P Q) P)

Let’s see another example, this time with the formula $(P \lor \neg Q) \land (\neg P \land Q)$.

Start with the root: $\{(P \lor \neg Q) \land (\neg P \land Q)\}$.
Apply the conjunction rule: $\{P \lor \neg Q, \neg P \land Q\}$.
Apply the disjunction rule to the first formula:
- Left child: $\{P, \neg P \land Q\}$
- Right child: $\{\neg Q, \neg P \land Q\}$
Apply the conjunction rule to the second formula in the left child: $\{P, \neg P, Q\}$ (blocked)
Apply the conjunction rule to the second formula in the right child: $\{\neg Q, \neg P, Q\}$ (blocked)

Tableau for ((P Q) (P Q))

In this case, all leaves are blocked, so the formula is unsatisfiable.

Different choices of expansion may lead to different tableaus, but every tableau gives the same outcome.

Complexity

Deterministic: Roughly $O(n \cdot 2^d)$, where $n$ is the formula size and $d$ is the number of disjunctions. This is because the height of the tableau is at most the size of the formula, and the number of nodes is roughly $2^d$, where $d$ is the number of disjunctions.
Non-deterministic: Polynomial time, proportional to the number of disjunctions.

Connection to DNF

The tableau method implicitly constructs a DNF of the original formula. Each leaf represents a conjunction of literals, and the entire tableau represents a disjunction of these conjunctions. The commas in the leaves can be interpreted as conjunctions.

For example, in the tableau from 1, the right child represents the clause $\neg Q \land \neg P$. The left child is blocked, so it does not contribute to the DNF. Thus, the DNF is simply $\neg Q \land \neg P$.

In the tableau from 2, both children are blocked, so the DNF is simply false.

Reachability Problem

The reachability problem is a fundamental problem in verification and planning. It involves determining if a system can transition from an initial state to a target state. This is the paradigmatic problem we will use to test the algorithms and formalisms we learn in this course.

Formalization

States: Represented by a tuple of $K$ bits.
Initial States: Described by a formula $\phi_{init}(P)$, where $P$ is a tuple of $K$ propositional letters. The models of the formula are precisely the states that we would like to be in our set of initial states.
Target States: Described by a formula $\phi_{target}(P)$. The models of the formula are precisely the states that we would like to be in our set of target states.
Single Step: Described by a formula $\phi_{step}(P, P')$, where $P$ represents the source state and $P'$ represents the target state. The formula describes the transition relation of the system, relating the values of the bits in the source state to the values of the bits in the target state.

Problem Statement

Given $\phi_{init}$, $\phi_{target}$, and $\phi_{step}$, is there a sequence of states $s_0, s_1, \dots, s_n$ such that:

$s_0$ satisfies $\phi_{init}$.
$s_n$ satisfies $\phi_{target}$.
For each $i$, $(s_i, s_{i+1})$ satisfies $\phi_{step}$.

Reduction to Satisfiability

We can reduce the reachability problem to a satisfiability problem.

Theorem 2.

Without loss of generality (w.l.o.g), if there is a path from an initial state to a target state, there is a path of length at most $2^K$.

Proof. Proof. If a path longer than $2^K$ exists, it must visit some state twice (pigeonhole principle). We can remove the loop between the repeated visits, obtaining a shorter path. This is because there are only $2^K$ possible states.

Also, we can add a "no-operation" to the transition relation, allowing the system to stay in the same state. This can be done by adding a model to $\phi_{step}$ where the source and target states are the same. Thus, if a path of length less than $2^K$ exists, we can extend it to a path of length exactly $2^K$ by adding "no-operation" steps. ◻

Reachability Problem

Consider a system with 2 bits, so $K=2$. The states are represented by tuples of 2 bits, e.g., $(0, 0), (0, 1), (1, 0), (1, 1)$.

Let the initial state be $(0, 0)$, so $\phi_{init} = \neg P_1 \land \neg P_2$.

Let the target states be those where the first bit is 1, so $\phi_{target} = P_1$.

Let the single step be defined as follows: from any state, we can either flip the first bit or the second bit, but not both. So $\phi_{step} = (P_1' \leftrightarrow \neg P_1) \land (P_2' \leftrightarrow P_2) \lor (P_1' \leftrightarrow P_1) \land (P_2' \leftrightarrow \neg P_2)$.

The question is: is there a sequence of states $s_0, s_1, \dots, s_n$ such that $s_0$ satisfies $\phi_{init}$, $s_n$ satisfies $\phi_{target}$, and for each $i$, $(s_i, s_{i+1})$ satisfies $\phi_{step}$?

In this case, the answer is yes. For example, the sequence $(0, 0), (1, 0)$ satisfies the conditions.

By 2, we know that if there is a path, there is a path of length at most $2^2 = 4$. In this case, there is a path of length 1.

Conclusion

The tableau method provides a practical and insightful approach to solving the satisfiability problem. It implicitly constructs a DNF, highlighting the connection between the algorithm and the normal form. The reachability problem, a crucial problem in verification, can be effectively reduced to a satisfiability problem, demonstrating the power of propositional logic in solving real-world problems.

Follow-up Questions/Topics for Next Lecture:

How can we construct the propositional formula for the reachability problem of length $2^K$?
How can we use the tableau method to solve the reachability problem?
What are the limitations of propositional logic for modeling complex systems?
What are other logical formalisms that can be used for verification?

--- title: "Propositional Logic: Tableau Method and Reachability Problem" author: "Your Name" date: "2025-02-05" format: html: toc: true # Table of Contents toc-depth: 2 code-tools: true theme: cosmo # Or "journal" for Distill-like minimalism --- # Introduction This lecture continues the discussion on propositional logic, focusing on the **tableau method** as an alternative algorithm for determining satisfiability. We will explore its practical efficiency compared to traditional methods, such as exhaustive search, and its connection to **disjunctive normal form (DNF)**. Additionally, we will introduce the **reachability problem** as an application example, demonstrating how to reduce it to a satisfiability problem in propositional logic. The reachability problem will be a recurring theme throughout the course as a way to illustrate the concepts of verification and planning. # Recap of Propositional Logic Last week, we introduced propositional logic, a basic logic with Boolean connectives and variables. We studied two fundamental problems: - **Model Checking (Evaluation Problem)**: Determines if a formula is true under a given interpretation. This problem is P-complete (polynomial time complete). - **Satisfiability Problem (SAT)**: Determines if there exists an interpretation that makes a formula true. This problem is NP-complete (non-deterministic polynomial time complete). The famous SAT problem is NP-complete. We also explored normal forms, including: - **Negation Normal Form (NNF)**: Negations are pushed inwards to appear only in front of literals. A literal is a propositional letter or its negation. - **Conjunctive Normal Form (CNF)**: A conjunction of clauses, where each clause is a disjunction of literals. In other words, conjunctions are outside, followed by disjunctions, and then negations. - **Disjunctive Normal Form (DNF)**: A disjunction of clauses, where each clause is a conjunction of literals. In other words, disjunctions are outside, followed by conjunctions, and then negations. We discussed how any formula (without the double implication operator, which is problematic) can be efficiently transformed into NNF while preserving equivalence. We also saw that a formula can be transformed into CNF in polynomial time while preserving satisfiability (equisatisfiability), potentially introducing new variables. This transformation is known as **Tseitin transformation**. The existence of this transformation proves that CNF-SAT is also NP-complete. # Disjunctive Normal Form and Satisfiability Unlike CNF SAT, DNF SAT is in P. This means there exists a polynomial-time algorithm to solve it. :::: {.thm:dnf_sat_in_p .theorem} **Theorem 1**. ::: tcolorbox *DNF SAT is in P.* ::: :::: ::: proof *Proof.* A DNF formula is a disjunction of clauses, where each clause is a conjunction of literals. To check if a DNF formula is satisfiable, we can check each clause separately. A clause is satisfiable if it does not contain a contradiction (e.g., $P$ and $\neg P$). If any clause is satisfiable, the entire DNF formula is satisfiable. This can be done in polynomial time, specifically, in time proportional to the number of clauses times their length. ◻ ::: Because of [1](#thm:dnf_sat_in_p){reference-type="ref+Label" reference="thm:dnf_sat_in_p"}, we cannot have a polynomial reduction from SAT to DNF-SAT that preserves equisatisfiability, unlike the reduction from SAT to CNF-SAT. # Tableau Method The tableau method is an alternative algorithm for satisfiability that is often more efficient in practice than exhaustive search. It constructs a tree called a **tableau**, where each node represents a set of formulas. The classical algorithm for satisfiability has complexity $2^n$, where $n$ is the number of propositional letters. ## Idea Instead of guessing an interpretation from the bottom (assigning values to variables), the tableau method guesses pieces of the formula from the top that should be true. It recursively breaks down these pieces until it reaches literals, revealing a satisfying assignment if one exists. The idea is that, instead of making a non-deterministic choice for every variable in the formula, we make a non-deterministic choice for every disjunct in the formula. ## Tableau Construction A tableau is a tree where each node contains a set of formulas. It is important to note that this tree is different from the tree that represents the formula. The root contains the initial formula. The tableau is expanded using the following rules: 1. **Initialization**: Start with a single node (root) containing the input formula in NNF. 2. **Expansion**: - Choose a leaf node and a formula $\alpha$ within its set. - **Conjunction Rule**: If $\alpha = \beta \land \beta'$, append a new child to the leaf, labeled with the set where $\alpha$ is replaced by $\beta, \beta'$. In other words, the $\land$ is replaced by a comma. - **Disjunction Rule**: If $\alpha = \beta \lor \beta'$, add two children to the leaf. One child is labeled with the set where $\alpha$ is replaced by $\beta$, and the other with the set where $\alpha$ is replaced by $\beta'$. This is the only rule that creates branches. ## Blocked Leaves A leaf is **blocked** if it contains a contradiction (e.g., $P$ and $\neg P$). Blocked leaves are not expanded further. ## Termination The algorithm terminates when all leaves are blocked, or a satisfiable leaf (no contradictions) is found. - If all leaves are blocked, the original formula is unsatisfiable. - If a satisfiable leaf is found, the original formula is satisfiable. A satisfying assignment can be derived from the literals in the leaf by setting each literal to true. ## Example Consider the formula $(P \lor \neg Q) \land \neg P$. 1. Start with the root: $\{(P \lor \neg Q) \land \neg P\}$. 2. Apply the conjunction rule: $\{P \lor \neg Q, \neg P\}$. 3. Apply the disjunction rule: - Left child: $\{P, \neg P\}$ (blocked) - Right child: $\{\neg Q, \neg P\}$ (satisfiable) The tableau has a satisfiable leaf $\{\neg Q, \neg P\}$. Thus, the formula is satisfiable, and a satisfying assignment is $P = \text{false}$, $Q = \text{false}$. We can represent this as a tree using TikZ: <figure id="fig:tableau_example_1"> <figcaption>Tableau for <span class="math inline">$(P \lor \neg Q) \land \neg P$</span></figcaption> </figure> Let's see another example, this time with the formula $(P \lor \neg Q) \land (\neg P \land Q)$. 1. Start with the root: $\{(P \lor \neg Q) \land (\neg P \land Q)\}$. 2. Apply the conjunction rule: $\{P \lor \neg Q, \neg P \land Q\}$. 3. Apply the disjunction rule to the first formula: - Left child: $\{P, \neg P \land Q\}$ - Right child: $\{\neg Q, \neg P \land Q\}$ 4. Apply the conjunction rule to the second formula in the left child: $\{P, \neg P, Q\}$ (blocked) 5. Apply the conjunction rule to the second formula in the right child: $\{\neg Q, \neg P, Q\}$ (blocked) <figure id="fig:tableau_example_2"> <figcaption>Tableau for <span class="math inline">$(P \lor \neg Q) \land (\neg P \land Q)$</span></figcaption> </figure> In this case, all leaves are blocked, so the formula is unsatisfiable. ::: mdframed Different choices of expansion may lead to different tableaus, but every tableau gives the same outcome. ::: ## Complexity - **Deterministic**: Roughly $O(n \cdot 2^d)$, where $n$ is the formula size and $d$ is the number of disjunctions. This is because the height of the tableau is at most the size of the formula, and the number of nodes is roughly $2^d$, where $d$ is the number of disjunctions. - **Non-deterministic**: Polynomial time, proportional to the number of disjunctions. ## Connection to DNF The tableau method implicitly constructs a DNF of the original formula. Each leaf represents a conjunction of literals, and the entire tableau represents a disjunction of these conjunctions. The commas in the leaves can be interpreted as conjunctions. For example, in the tableau from [1](#fig:tableau_example_1){reference-type="ref+Label" reference="fig:tableau_example_1"}, the right child represents the clause $\neg Q \land \neg P$. The left child is blocked, so it does not contribute to the DNF. Thus, the DNF is simply $\neg Q \land \neg P$. In the tableau from [2](#fig:tableau_example_2){reference-type="ref+Label" reference="fig:tableau_example_2"}, both children are blocked, so the DNF is simply false. # Reachability Problem The reachability problem is a fundamental problem in verification and planning. It involves determining if a system can transition from an initial state to a target state. This is the paradigmatic problem we will use to test the algorithms and formalisms we learn in this course. ## Formalization - **States**: Represented by a tuple of $K$ bits. - **Initial States**: Described by a formula $\phi_{init}(P)$, where $P$ is a tuple of $K$ propositional letters. The models of the formula are precisely the states that we would like to be in our set of initial states. - **Target States**: Described by a formula $\phi_{target}(P)$. The models of the formula are precisely the states that we would like to be in our set of target states. - **Single Step**: Described by a formula $\phi_{step}(P, P')$, where $P$ represents the source state and $P'$ represents the target state. The formula describes the transition relation of the system, relating the values of the bits in the source state to the values of the bits in the target state. ## Problem Statement Given $\phi_{init}$, $\phi_{target}$, and $\phi_{step}$, is there a sequence of states $s_0, s_1, \dots, s_n$ such that: - $s_0$ satisfies $\phi_{init}$. - $s_n$ satisfies $\phi_{target}$. - For each $i$, $(s_i, s_{i+1})$ satisfies $\phi_{step}$. ## Reduction to Satisfiability We can reduce the reachability problem to a satisfiability problem. :::: {.thm:reachability_bound .theorem} **Theorem 2**. ::: tcolorbox *Without loss of generality (w.l.o.g), if there is a path from an initial state to a target state, there is a path of length at most $2^K$.* ::: :::: ::: proof *Proof.* If a path longer than $2^K$ exists, it must visit some state twice (pigeonhole principle). We can remove the loop between the repeated visits, obtaining a shorter path. This is because there are only $2^K$ possible states. Also, we can add a \"no-operation\" to the transition relation, allowing the system to stay in the same state. This can be done by adding a model to $\phi_{step}$ where the source and target states are the same. Thus, if a path of length less than $2^K$ exists, we can extend it to a path of length exactly $2^K$ by adding \"no-operation\" steps. ◻ ::: ::: tcolorbox **Reachability Problem** Consider a system with 2 bits, so $K=2$. The states are represented by tuples of 2 bits, e.g., $(0, 0), (0, 1), (1, 0), (1, 1)$. Let the initial state be $(0, 0)$, so $\phi_{init} = \neg P_1 \land \neg P_2$. Let the target states be those where the first bit is 1, so $\phi_{target} = P_1$. Let the single step be defined as follows: from any state, we can either flip the first bit or the second bit, but not both. So $\phi_{step} = (P_1' \leftrightarrow \neg P_1) \land (P_2' \leftrightarrow P_2) \lor (P_1' \leftrightarrow P_1) \land (P_2' \leftrightarrow \neg P_2)$. The question is: is there a sequence of states $s_0, s_1, \dots, s_n$ such that $s_0$ satisfies $\phi_{init}$, $s_n$ satisfies $\phi_{target}$, and for each $i$, $(s_i, s_{i+1})$ satisfies $\phi_{step}$? In this case, the answer is yes. For example, the sequence $(0, 0), (1, 0)$ satisfies the conditions. By [2](#thm:reachability_bound){reference-type="ref+Label" reference="thm:reachability_bound"}, we know that if there is a path, there is a path of length at most $2^2 = 4$. In this case, there is a path of length 1. ::: # Conclusion The tableau method provides a practical and insightful approach to solving the satisfiability problem. It implicitly constructs a DNF, highlighting the connection between the algorithm and the normal form. The reachability problem, a crucial problem in verification, can be effectively reduced to a satisfiability problem, demonstrating the power of propositional logic in solving real-world problems. **Follow-up Questions/Topics for Next Lecture:** - How can we construct the propositional formula for the reachability problem of length $2^K$? - How can we use the tableau method to solve the reachability problem? - What are the limitations of propositional logic for modeling complex systems? - What are other logical formalisms that can be used for verification?