From 3a0b9e7260364bb46b71c45bfdf1d6a5afca953a Mon Sep 17 00:00:00 2001 From: Alberto Paganelli Date: Tue, 5 Sep 2023 19:43:41 +0200 Subject: [PATCH] doc: add tseitin tranformations table to implementation doc --- doc/report/5-implementation.md | 119 ++++++++++++++++++++++----------- doc/report/img/AndCircuit.svg | 4 ++ doc/report/img/NotCircuit.svg | 5 ++ doc/report/img/OrCircuit.svg | 4 ++ 4 files changed, 92 insertions(+), 40 deletions(-) create mode 100644 doc/report/img/AndCircuit.svg create mode 100644 doc/report/img/NotCircuit.svg create mode 100644 doc/report/img/OrCircuit.svg diff --git a/doc/report/5-implementation.md b/doc/report/5-implementation.md index 984aef59..776b4c83 100644 --- a/doc/report/5-implementation.md +++ b/doc/report/5-implementation.md @@ -32,9 +32,9 @@ branch. In the literature exist a bunch of more heuristics and optimizations. Once I understood the problem, I implemented the decision tree data structure that will be used by the DPLL algorithm to find the possible assignments. ```DecisionTree``` is a binary tree where each node implicitly represent the decision and the state of the algorithm e.g. the current ```PartialModel``` and ```CNF```. -In order to exploit at most the functional programming paradigm they've been implemented using case classes and ```Enum```(s) with the ultimate goal of facilitating the use of match cases. +In order to exploit at most the functional programming paradigm they've been implemented using case classes and ```Enum```(s) with the ultimate goal of facilitating the use of match cases. -Before implementing all DPLL subparts individually, I tested the data structure implementing an exhaustive search of all the possible assignments to the partial model. +Before implementing all DPLL subparts individually, I tested the data structure implementing an exhaustive search of all the possible assignments to the partial model. ### CNF simplification @@ -44,64 +44,64 @@ In fact, if the CNF expression is completely simplified s.t. it is equal to a `` The expression in CNF is simplified according to the specific logical operator: - ```Or``` - - When a Literal inside an ```Or``` is set to ```True``` s.t. `V = true` or `Not(V) = True` then the CNF must be simplified on the uppermost `Or` of a sequence of consecutive `Or`s. + - When a Literal inside an ```Or``` is set to ```True``` s.t. `V = true` or `Not(V) = True` then the CNF must be simplified on the uppermost `Or` of a sequence of consecutive `Or`s. - Examples: - - Literal `A` in positive form. Constraint `A = True`: + Examples: + - Literal `A` in positive form. Constraint `A = True`: -

- -

- - - Literal `B` is negated. Constraint `B = False` to set the literal `True`: +

+ +

-

- -

+ - Literal `B` is negated. Constraint `B = False` to set the literal `True`: + +

+ +

- A more complex CNF expression. Constraint `A = True`:

- +

- Simplify the `Or` only when the variable occurs inside its sub-CNF. Constraint `B = False`:

- +

- - When a Literal in an ```Or``` branch is set to ```False``` s.t. `V = False` or `Not(V) = False` the CNF must be simplified substituting the `Or` with the other branch. - - Examples: +- When a Literal in an ```Or``` branch is set to ```False``` s.t. `V = False` or `Not(V) = False` the CNF must be simplified substituting the `Or` with the other branch. + + Examples: - Literal `A` in positive form. Constraint `A = False`:

- +

- A more complex example. Constraint `A = False`:

- +

- `And` - - An expression in CNF should be simplified when an `And` contains at least a `True` Literal: + - An expression in CNF should be simplified when an `And` contains at least a `True` Literal: - Examples: + Examples: - - Constraint `B = True`: -

- -

+ - Constraint `B = True`: +

+ +

+ + - A more complex example. Constraint `A = True`: +

+ +

- - A more complex example. Constraint `A = True`: -

- -

- ## Mattia Matteini @@ -125,12 +125,12 @@ object Main extends App with MVU ## Alberto Paganelli -My first task was to analyze in depth the Tseitin transformation algorithm and before the implementation defining the data structures collaborating with the team. +My first task was to analyze in depth the Tseitin transformation algorithm and before the implementation defining the data structures collaborating with the team. After the definition of a data structure I started to define the algorithm's phases. The first defined data structure was the Enumeration `Expression` that represents the expression of the formula in the enumeration form. -Looking to the algoritm's phases I started writing some utils method for the `Expression` object that can be used from all. -In particular to zip the subexpressions with new variables I made use of generic type to make the code more reusable. +Looking to the algoritm's phases I started writing some utils method for the `Expression` object that can be used from all. +In particular to zip the subexpressions with new variables I made use of generic type to make the code more reusable. After the definition of these methods, where I have made great use of Pattern Matching, it was possible to start implementing the algorithm's phases. @@ -141,7 +141,7 @@ I followed the TDD approach for the core of the algorithm and for the utils meth ## Tseitin Algorithm -The Tseitin algorithm is a method for converting a formula in propositional logic into a CNF formula. +The Tseitin algorithm converts a formula in propositional logic into a CNF formula. CNF is a specific form of representing logical formulas as a conjunction of clauses, where each clause is a disjunction of literals (variables or their negations). @@ -156,13 +156,52 @@ The Tseitin transformation follows these steps: 1. Assign a unique identifier to each subformula in the original formula. 2. Replace each subformula with an auxiliary variable representing its truth value. +

+(a ∧ (b ∨ c)) -> (¬c ∧ d)
+TSTN4 <--> ¬c
+TSTN3 <--> b ∨ c
+TSTN2 <--> TSTN4 ∧ d
+TSTN1 <--> a ∧ TSTN3
+TSTN0 <--> TSTN1 --> TSTN2 +

3. Express the truth conditions of the subformulas in CNF using the auxiliary variables and standard logical - connectives (AND, OR, NOT). -4. Combine the CNF representations of the subformulas to obtain the CNF representation of the entire formula. - -The resulting CNF formula is equi-satisfiable with the original formula, meaning they have the same set of satisfying + connectives (AND, OR, NOT) following the transformations listed in the table below. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
OperatorCircuitExpressionConverted
ANDAnd CircuitX = A ∧ B(¬A ∨ ¬B ∨ X) ∧ (A ∨ ¬X) ∧ (B ∨ ¬X)
OROr CircuitX = A ∨ B(A ∨ B ∨ ¬X) ∧ (¬A ∨ X) ∧ (¬B ∨ X)
NOTNot CircuitX = ¬A(¬A ∨ ¬X) ∧ (A ∨ X)
+ +4. Combine the representations of the subformulas to obtain the CNF representation of the entire formula. + +The resulting formula is equi-satisfiable with the original formula, meaning they have the same set of satisfying assignments. This transformation enables the use of various CNF-based algorithms and tools to analyze and reason about -the original logical formula efficiently +the original logical formula efficiently. --- diff --git a/doc/report/img/AndCircuit.svg b/doc/report/img/AndCircuit.svg new file mode 100644 index 00000000..48e523e6 --- /dev/null +++ b/doc/report/img/AndCircuit.svg @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/doc/report/img/NotCircuit.svg b/doc/report/img/NotCircuit.svg new file mode 100644 index 00000000..ffc4d636 --- /dev/null +++ b/doc/report/img/NotCircuit.svg @@ -0,0 +1,5 @@ + + + + + diff --git a/doc/report/img/OrCircuit.svg b/doc/report/img/OrCircuit.svg new file mode 100644 index 00000000..dac62d29 --- /dev/null +++ b/doc/report/img/OrCircuit.svg @@ -0,0 +1,4 @@ + + + +