From e63edcbaf96daf803147b374173b181f84179bf5 Mon Sep 17 00:00:00 2001 From: Alice Date: Tue, 19 Sep 2023 16:02:34 +0100 Subject: [PATCH] vault backup: 2023-09-19 16:02:34 --- .obsidian/workspace.json | 32 ++++------ Notes/MFES/T - Aula 2 - 18 Setembro 2023.md | 26 +++++++-- Notes/MFES/TP - Aula 1 - 18 Setembro.md | 65 +++++++++++++++++++++ 3 files changed, 97 insertions(+), 26 deletions(-) create mode 100644 Notes/MFES/TP - Aula 1 - 18 Setembro.md diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 116b188..41f5375 100644 --- a/.obsidian/workspace.json +++ b/.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", diff --git a/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md b/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md index c857c7a..96bc7f1 100644 --- a/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md +++ b/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$ - -### 1.2.1 Basic Equivalences +- Formula G is a strict subformula of F if G is a subformula of $F$ and $G \neg = F$ + + +**Basic Equivalences:** 1. $\neg \neg A \equiv A$ 2. $A \lor A \equiv A$ 3. $A \land A \equiv A$ @@ -100,4 +107,15 @@ 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. diff --git a/Notes/MFES/TP - Aula 1 - 18 Setembro.md b/Notes/MFES/TP - Aula 1 - 18 Setembro.md new file mode 100644 index 0000000..e14e845 --- /dev/null +++ b/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$ +> > +