vault backup: 2023-09-19 16:02:34

.obsidian/workspace.json

@@ -8,31 +8,18 @@
         "type": "tabs",
         "children": [
           {
-            "id": "201fe1705c33e116",
+            "id": "c8fbb024ba6347ad",
             "type": "leaf",
             "state": {
               "type": "markdown",
               "state": {
-                "file": "Notes/MFES/T - Aula 2 - 18 Setembro 2023.md",
-                "mode": "source",
-                "source": false
-              }
-            }
-          },
-          {
-            "id": "33ee032389b5d04b",
-            "type": "leaf",
-            "state": {
-              "type": "markdown",
-              "state": {
-                "file": "Notes/CP/T - Aula 2 - 19 Setembro.md",
+                "file": "Notes/MFES/TP - Aula 1 - 18 Setembro.md",
                 "mode": "source",
                 "source": false
               }
             }
           }
-        ],
-        "currentTab": 1
+        ]
       }
     ],
     "direction": "vertical"
@@ -61,7 +48,7 @@
             "state": {
               "type": "search",
               "state": {
-                "query": "tag:#excalidraw",
+                "query": "",
                 "matchingCase": false,
                 "explainSearch": false,
                 "collapseAll": false,
@@ -98,7 +85,7 @@
             "state": {
               "type": "backlink",
               "state": {
-                "file": "Notes/CP/T - Aula 2 - 19 Setembro.md",
+                "file": "Notes/MFES/TP - Aula 1 - 18 Setembro.md",
                 "collapseAll": false,
                 "extraContext": false,
                 "sortOrder": "alphabetical",
@@ -115,7 +102,7 @@
             "state": {
               "type": "outgoing-link",
               "state": {
-                "file": "Notes/CP/T - Aula 2 - 19 Setembro.md",
+                "file": "Notes/MFES/TP - Aula 1 - 18 Setembro.md",
                 "linksCollapsed": false,
                 "unlinkedCollapsed": true
               }
@@ -138,7 +125,7 @@
             "state": {
               "type": "outline",
               "state": {
-                "file": "Notes/CP/T - Aula 2 - 19 Setembro.md"
+                "file": "Notes/MFES/TP - Aula 1 - 18 Setembro.md"
               }
             }
           }
@@ -162,13 +149,14 @@
       "obsidian-excalidraw-plugin:Create new drawing": false
     }
   },
-  "active": "33ee032389b5d04b",
+  "active": "c8fbb024ba6347ad",
   "lastOpenFiles": [
     "Notes/MFES/T - Aula 2 - 18 Setembro 2023.md",
+    "Notes/MFES/TP - Aula 1 - 18 Setembro.md",
+    "Notes/MFES/MFES - UC Details.md",
     "Notes/CP/T - Aula 2 - 19 Setembro.md",
     "Notes/CP",
     "README.md",
-    "Notes/MFES/MFES - UC Details.md",
     "2023-09-18.md",
     "MFES/T - Aula 2 - 18 Setembro 2023.md",
     "Notes/RAS/T - Aula 2 - 19 Setembro 2023.md",

Notes/MFES/T - Aula 2 - 18 Setembro 2023.md

@@ -1,3 +1,9 @@
+# Conteúdo
+1. [[T - Aula 2 - 18 Setembro 2023#1. Intro|Intro]]
+	1. [[T - Aula 2 - 18 Setembro 2023#1.1 SAT|SAT]]
+	2. [[T - Aula 2 - 18 Setembro 2023#1.2 Proposicional Logic (PL)|Lógica Proposicional]]
+3. [[T - Aula 2 - 18 Setembro 2023#SAT Solvers|SAT Solvers]]
+
 # 1. Intro
 *Formal modeling* - formally represent the system and its properties in the syntactic conventions that the tool understands and can process. 
 
@@ -76,9 +82,10 @@ A formula $F$ is:
    >  - $\Gamma \models F$ iff $\Gamma, \neg F \models \bot$
 
 - Formula $G$ is a subformula of formula F if it occurs syntactically within F
-- Formula G is a strict subformula of F if G is a subformula of $F$ and $G \neg \equals F$
+- Formula G is a strict subformula of F if G is a subformula of $F$ and $G \neg = F$
 
-### 1.2.1 Basic Equivalences 
+
+**Basic Equivalences:**
 1. $\neg \neg A \equiv A$
 2. $A \lor A \equiv A$
 3. $A \land A \equiv A$
@@ -101,3 +108,14 @@ A formula $F$ is:
 
 
 
+# 2. SAT Solvers
+- There are several techniques and algorithms for SAT solving.
+- Usually SAT solvers receive as input a formula in a specific syntatical format.
+- SAT solvers deal with formulas in **conjunctive normal form (CNF)**.
+
+- Most current state-of-the-art SAT solvers are based on the **Davis-Putnam-Logemann-Loveland (DPLL) framework**.
+
+## 2.1 DPLL Framework
+The idea is to **incrementally construct an assignment compatible with a CNF**, propagating the implications of the decisions made that are easy to detect and simplifying the clauses.
+
+A CNF is satisfied by an assignment if all its clauses are satisfied. And a clause is satisfied if at least one of its literals is satisfied.

Notes/MFES/TP - Aula 1 - 18 Setembro.md

@@ -0,0 +1,65 @@
+## Ficha 1
+
+> [!help]+ Ex 1 (Configuração de produtos)
+> Certos produtos, como é o caso dos automóveis, são altamente personalizáveis, mas podem haver dependências entre as configurações. Os clientes podem não estar cientes de todas essas dependências, e poderão escolher opções de configuração inconsistentes.
+> Como são muitas configurações e muitas dependências, podemos usar um SAT solver para verificar se o cliente escolhe opções de configuração consistentes. Para isso, podemos seguir os seguintes passos:
+> 
+> 1. Codificar as dependências entre configurações como uma formula proposicional $\psi$
+> 2. Codificar as opções selecionadas pelo cliente como uma fórmula proposicional $\phi$.
+> 3. Usar o SAT solver para verificar se $\psi \land \phi$ não é contraditório.
+> 
+> Considere agora a seguinte dependência entre as configurações disponíveis para a personalização de um automóvel:
+> 
+> *"O ar condicionado Thermotronic comfort requer uma bateria de alta capacidade, exceto quando combinado com motores a gasolina de 3,2 litros."*
+> 
+> Será que um cliente pode escolher o ar condicionado Thermotronic comfort, uma bateria de pequena capacidade e não escolher o motor de 3,2 litros? Como poderia responder a esta pergunta com a ajuda de um SAT solver?
+> 
+>  > [!tip]- Resolução
+>  > Legenda de variáveis utilizadas:
+>  > A - ar condicionado
+>  > B - bateria alta capacidade
+>  > C - motor 3,2 L
+>  >
+>  >$A \land \neg B \implies G \equiv \neg (A \land \neg B) \lor G \equiv \neg A \lor B \lor G$
+>  >
+>  >$(\neg A \lor B \lor G) \land A \land \neg B \land \neg G$       ----- SAT?
+>  >
+>  
+
+
+> [!help]+ Ex 3 (Configuração de computadores)
+> Uma loja de eletrónica permite aos seus clientes personalizar o seu computador, escolhendo entre dois modelos de motherboards e dois modelos de monitor. Cada computador tem que ter obrigatoriamente uma única motherboard, um único CPU, uma única placa gráfica e uma única memória RAM. O computador poderá ou não ter um monitor. A personalização do computador deverá obedecer às regras:
+> 1. A motherboard MB1 quando combinada com a placa gráfica PG1, obriga à utilização da RAM1;
+> 2. A placa gráfica PG1 precisa do CPU1, exceto quando combinada com a memória RAM2;
+> 3.  O CPU2 só pode estar instalado na motherboard MB2;
+> 4.  O monitor MON1 para poder funcionar precisa da placa gráfca PG1 e da memória RAM2.
+>
+>Codifique este problema em lógica proposicional. Assinale claramente o que denota cada variável proposicional que introduzir e escreva um conjunto de fórmulas proposicionais adequado à sua modelação.
+>   
+>  > [!hint]- Resolução
+>  > Legenda de variáveis utilizadas:
+>  > $CPU_1; CPU_2; RAM_1; RAM_2; MB_1; MB_2; PG_1; PG_2; MON_1; MON_2$
+>  > 
+>  > Problema modelado:
+>  > 1. $CPU_1 \lor CPU_2$
+>  > 2. $CPU_1 \implies \neg CPU_2$
+>  > 3. $RAM_1 \lor RAM_2$
+>  > 4. $RAM_1 \implies \neg RAM_2$
+>  > 5. $MB_1 \lor MB_2$
+>  > 6. $MB_1 \implies \neg MB_2$
+>  > 7. $PG_1 \lor PG_2$
+>  > 8. $PG_1 \implies \neg PG_2$
+>  >    
+>  > 9. $MB_1 \land PG_1 \implies RAM_1$
+>  > 10. $PG_1 \implies CPU_1 \lor RAM_2 \equiv PG_1 \land \neg RAM_2 \implies CPU_1$
+>  > 11. $CPU_2 \implies MB_2$
+>  > 12. $MON_1 \implies PG_1 \land RAM_2$
+>  
+>  Indique, apenas por palavras, como poderia usar um SAT solver para testar as consistências deste conjunto de regras.
+>  
+>  Indique, apenas por palavras, como usaria um SAT solver para se pronuncias quanto à velocidade das seguintes afirmações:
+>  (a) O monitor MON1 só poderá ser usado com uma motherboard MB1.
+> > [!hint]- Resolução
+> > ??? $\tau \models MON_1 \implies MB_1$
+> > 
+