my_digital_garden/4a1s/MFES/T - Aula 2.md

18 Setembro 2023 - #MFES

Conteúdo

1. MFES/T - Aula 2#1. Intro
   1. MFES/T - Aula 2#1.1 SAT
   2. MFES/T - Aula 2#1.2 Proposicional Logic (PL)
2. MFES/T - Aula 2#SAT Solvers

1. Intro

Formal modeling - formally represent the system and its properties in the syntactic conventions that the tool understands and can process.

Formal Logic = logical language (logical symbols + non-logical symbols) + semantics +proof system

1.1 SAT

The Boolean satisfiability (SAT) problem:

Find an assignment to the propositional variables of the formula such that the formula evaluates to TRUE, or prove that no such assignment exists.

• SAT is an NP-complete decision problem.
  • SAT was the first problem to be shown NP-complete.
  • There are no known polynomial time algorithms for SAT.

Usually SAT solvers deal with formulas in conjunctive normal form (CNF)

• literal: propositional variable or its negation A, ¬A, B, ¬B, C, ¬C
• clause: disjuntion of literals. (A _ ¬B _ C)
• conjunctive normal form: conjuction of clauses. (A _ ¬B _ C) ^ (B _ ¬A) ^ ¬C

[!info]+ Cook's theorem(1971) SAT is NP-complete

1.2 Proposicional Logic (PL)

[!note] Nota Esta secção basicamente só contém revisão de conceitos. Aconselha-se a ver a coisa rapidamente, porque é só a formalidade de lógica escrita por extenso.

Let A be an assignment and let F be a formula. If A(F) = 1, then we say F holds under assignment, or A models F. We write A \models F iff A(F)=1, and A \not \models F iff A(F) = 0.

An assignment is a function A : V_{prop} \implies {0,1} , that assigns to every propositional variable a truth value. An assignment A naturally extends to all formulas, A : Form \implies {0,1}. The truth value of a formula is computed using truth tables:

F	A	B	\neg A	A \land B	A \lor B	A \implies B	A \iff B	\bot	\top
A_1 (F)	0	1	1	0	1	1	0	0	1
A_2 (F)	0	0	1	0	0	1	1	0	1
A_3 (F)	1	1	0	1	1	1	1	0	1
A_4 (F)	1	0	0	0	1	0	0	0	1

A formula F is:

1. valid iff it holds under every assignment. We write \models F. A valid formula is called a tautology.
2. satisfiable iff it folds (true) under some assignment.
3. unsatisfiable iff it holds under no assignment. An unsatisfiable formula is called a contradiction.
4. refutable iff it is not valid.

[!tip]+ Proposition F is valid iff \neg F is unsatisfiable.

• F \models G iff for every assignment A, if A \models F then A \models G. We say G is a consequence of F.

• F \equiv G iff F \models G and G \models F. We say F and G are equivalent.

• Let \Gamma = { F_1, F_2, F_3,... } be a set of formulas.

  • A \models \Gamma iff A \models F_i for each formula F_i in \Gamma. We say A models \Gamma.
  • \Gamma \models G iff A \models \Gamma implies A \models G for every assignment A. We say G is a consequence of \Gamma.

  [!tip]+ Proposition

  • F \models G iff \models F \implies G.
  • \Gamma \models G and \Gamma finite iff \models \land \Gamma \implies G.

  • \Gamma is consistent or satisfiable iff there is an assignment that models \Gamma.
  • We say that \Gamma is inconsistent or unsatisfiable iff there is not consistent and denote this by \Gamma \models \bot.

  [!tip]+ Proposition

  • {$F, \neg F$} \models \bot
  • If \Gamma \models \bot and \Gamma \subseteq \Gamma ', then \Gamma ' \models \bot
  • \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 = F

Basic Equivalences:

1. \neg \neg A \equiv A
2. A \lor A \equiv A
3. A \land A \equiv A
4. A \land \neg A \equiv \bot
5. A \lor \neg A \equiv \top
6. A \lor B \equiv B \lor A
7. A \land B \equiv B \land A
8. A \land \top \equiv A
9. A \lor \top \equiv \top
10. A \land \bot \equiv \bot
11. A \lor \bot \equiv A
12. A \land (B \lor A) \equiv A
13. A \land (B \lor C) \equiv (A \land B) \lor (A \land C)
14. A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)
15. \neg (A \lor B) \equiv \neg A \land \neg B
16. \neg (A \land B) \equiv \neg A \lor \neg B
17. A \implies B \equiv \neg A \lor B
18. A \iff B \equiv (A \implies B) \land (B \implies A)

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.