18 Setembro 2023 - #MFES

Conteúdo

1. Intro
   1. SAT
   2. Lógica Proposicional
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

1.2 Proposicional Logic (PL)

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⊭F$ iff $A(F)=0$.

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

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.

• $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 $\mathrm{\Gamma }=F_1,F_2,F_3,...$ be a set of formulas.

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

  • $F\models G$ iff $\models F⟹G$.
  • $\mathrm{\Gamma }\models G$ and $\mathrm{\Gamma }$ finite iff $\models \wedge \mathrm{\Gamma }⟹G$.

  • $\mathrm{\Gamma }$ is consistent or satisfiable iff there is an assignment that models $\mathrm{\Gamma }$.
  • We say that $\mathrm{\Gamma }$ is inconsistent or unsatisfiable iff there is not consistent and denote this by $\mathrm{\Gamma }\models \mathrm{\perp }$.
  Proposition

  • {$F,\mathrm{\neg }F$} $\models \mathrm{\perp }$
  • If $\mathrm{\Gamma }\models \mathrm{\perp }$ and $\mathrm{\Gamma }\subseteq {\mathrm{\Gamma }}^{\prime }$, then ${\mathrm{\Gamma }}^{\prime }\models \mathrm{\perp }$
  • $\mathrm{\Gamma }\models F$ iff $\mathrm{\Gamma },\mathrm{\neg }F\models \mathrm{\perp }$

• 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\mathrm{\neg }=F$

Basic Equivalences:

1. $\mathrm{\neg }\mathrm{\neg }A\equiv A$
2. $A\vee A\equiv A$
3. $A\wedge A\equiv A$
4. $A\wedge \mathrm{\neg }A\equiv \mathrm{\perp }$
5. $A\vee \mathrm{\neg }A\equiv \mathrm{\top }$
6. $A\vee B\equiv B\vee A$
7. $A\wedge B\equiv B\wedge A$
8. $A\wedge \mathrm{\top }\equiv A$
9. $A\vee \mathrm{\top }\equiv \mathrm{\top }$
10. $A\wedge \mathrm{\perp }\equiv \mathrm{\perp }$
11. $A\vee \mathrm{\perp }\equiv A$
12. $A\wedge (B\vee A)\equiv A$
13. $A\wedge (B\vee C)\equiv (A\wedge B)\vee (A\wedge C)$
14. $A\vee (B\wedge C)\equiv (A\vee B)\wedge (A\vee C)$
15. $\mathrm{\neg }(A\vee B)\equiv \mathrm{\neg }A\wedge \mathrm{\neg }B$
16. $\mathrm{\neg }(A\wedge B)\equiv \mathrm{\neg }A\vee \mathrm{\neg }B$
17. $A⟹B\equiv \mathrm{\neg }A\vee B$
18. $A⟺B\equiv (A⟹B)\wedge (B⟹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.