Title: Theory / Unimportant / CS / Algo / Decision Procedures - Kroening Strichman V2 / 1 Introduction;
Tags: fromAlgorithm fromImplementation fromImplication hasNotNewEffectReturnsMeaning complexity examplesSwitchExample1 hasSeenConjDef typToBinary typToWtd
On every note of this deck, unless a note says otherwise:
Chapter: 1

Question: Proof-theoretic approch of validity/satisfiability
Answer: use a deductive mechanism of reasoning, based on axioms and inference rules, which together are called an inference system.
Page: 3
Chapter: 1

Question: Model-theoretic approch of validity/satisfiability
Answer: Enumerate possible solutions from a finite number of candidates.
Page: 3
Chapter: 1

Name: An assigment of \(\phi\) from a domain \(D\)
Definition: A map from \(\phi's\) variables to elements of \(D\)
Page: 3
Section: 2
Variables: \(D\) a domain,
\(\phi\) a formula
Kind: Def

Name: A full assigment of \(\phi\) from a domain \(D\)
Definition: An assignment whose domains is every variables of \(\phi\)
Page: 3
Section: 2
Variables: \(D\) a domain,
\(\phi\) a formula
Kind: Def

Name: A partial assigment of \(\phi\) from a domain \(D\)
Definition: An assignment which is not full
Page: 3
Section: 2
Variables: \(D\) a domain,
\(\phi\) a formula
Kind: Def

Name: A satisfiable formula
Definition: A formula such that there exists an assignment of its variables under which the formula evaluates to TRUE
Page: 3
Section: 2
Kind: Def

Name: A formula which is a contradiction
Definition: A not satisfiable formula
Page: 3
Section: 2
Kind: Def

Name: A valid formula
Definition: A formula which evaluates to TRUE for each assignemnts
Page: 3
Section: 2
Kind: Def

Name: SMT solver
Definition: Software solving the SMT problem
Page: 6
Section: 2

Smaller0: \(\phi\) is valid
Greater0: \(\neg\phi\) is a contradiction
Page: 6
Chapter: 1
Section: 2
Variables: \(\phi\) a formula
Smaller to greater: iff

Name: Decision problem for formulas
Definition: Given a formula, determining whether it is valid.
Page: 6
Section: 2
Index: 4
Kind: Def

Question: Difference between procedure and algorithm ?
Answer: Only algorithms should terminates. (Decision procedure are algorithms however)
Page: 7
Chapter: 1
Section: 2
Index: 3
Kind: footnote

Name: A sound procedure
Definition: A procedure such that, when it returns “Valid”, the input formula is valid.
Page: 7
Section: 2
Index: 5
Kind: Def
Extra: correct?

Name: A complete procedure
Definition: always terminates, and
Page: 7
Section: 2
Index: 6
Kind: Def
Definition2: returns “Valid” when the input formula is valid.
Conjdef: A procedure which

Name: A decision procedure for \(T\)
Definition: A procedure which is sound and complete with respect to every formula of T .
Page: 7
Section: 2
Kind: Def

Name: A decidable theory
Definition: A theory which admits a decision procedure
Page: 7
Section: 2
Kind: Def

Name: Equisatisfiable formulae
Definition: Formulas which are both satisfiable or both unsatisfiable
Page: 8
Section: 3
Index: 9
Kind: Def

Name: A formula in Negation normal form
Definition: A positive boolean combinations of literals
Page: 8
Section: 3
Notation: A formula in NNF
Index: 10
Kind: Def

Name: A literal
Definition: either a positive or a negative literal
Page: 8
Section: 3
Index: 11
Kind: Def

Name: A negative literal
Definition: the negation of an atom
Page: 8
Section: 3
Index: 11
Kind: Def

Name: A positive literal
Page: 8
Section: 3
Context: propositional logic
Index: 11
Kind: Def
Name2: An atom

Name: A satisfied literal
Definition: Either a positive literal whose atom is assigned to TRUE,
or a negative literal whose atom is assigned to FALSE
Page: 9
Section: 3
Index: 12
Kind: Def

Name: A pure literal of \(\phi\)
Definition: A litteral occurring with the same positivity in all of \(\phi\)
Page: 9
Section: 3
Variables: \(\phi\) a formula
Index: 13
Kind: Def

Name: An occurence of a literal whose polarity is positive in \(\phi\)
Definition: An ocurence of a literal which occurs below an even number of negation/left side of implications
Page: 9
Section: 3
Variables: \(\phi\) a formula
Index: 12
Kind: Def

Name: An occurence of a literal whose polarity is negative in \(\phi\)
Definition: An ocurence of a literal which occurs below an odd number of negation/left side of implications
Page: 9
Section: 3
Variables: \(\phi\) a formula
Index: 12
Kind: Def

Name: The positive set of \(\alpha\) with respect to \(\phi\)
Definition: the literals that are satisfied by \(\alpha\)
Page: 9
Section: 3
Variables: \(\phi\) a formula,
\(\alpha\) an assignment of its variables
Index: 14
Kind: Theo
Abbreviation: \(pos(\alpha,\phi)\)
Assuming: \(\phi\) in NNF

Smaller0: \(\subseteq\)
Greater0: \(\implies\)
Page: 9
Chapter: 1
Section: 3
Variables: \(\phi\) a formula,
\(\alpha,\alpha'\) assignment of its variables
Index: 14
Kind: Theo
Prefix Greater: \(\alpha\models\phi\)
Assuming: \(\phi\) in NNF
Prefix Smaller: \(pos(\alpha,\phi)\)
Suffix Greater: \(\alpha'\models\phi\)
Suffix Smaller: \(pos(\alpha',\phi)\)

Name: A formula in disjunctive normal form
Definition: A disjunction of conjunctions of literals
Page: 10
Section: 3
Index: 16
Kind: Def
Abbreviation: A formula in DNF
Denoted by: \[\bigvee_i\left(\bigwedge_jl_{ij}\right)\]

Name: Its \(i\)-th term
Definition: \(\bigwedge _j l_{ij}\)
Page: 10
Section: 3
Variables: \[\bigvee_i\left(\bigwedge_jl_{ij}\right)\] a formula in disjunctive normal form
Index: 16
Kind: Def

Name: A formula in conjunctive normal form
Definition: A conjunction of disjunctions of literals
Page: 12
Section: 3
Context: formula
Index: 20
Kind: Def
Abbreviation: CNF
Denoted by: \[\bigwedge_i\left(\bigvee_jl_{ij}\right)\]

Name: Its \(i\)-th term
Definition: \(\bigvee_j l_{ij}\)
Page: 12
Section: 3
Variables: \[\bigwedge_i\left(\bigvee_jl_{ij}\right)\] a formula in conjunctive normal form
Index: 20
Kind: Def

Page: 11
Implementation: Computing NNF first.
Recursively, transform \(\bigwedge_i\left(\bigvee_jl_{ij}\right)\lor \bigwedge_{i'}\left(\bigvee_{j'}l'_{i'j'}\right)\) into \(\bigwedge_{i,i'}\left(\bigvee_{j}l_{ij}\lor\bigvee_{j'}l'_{i'j'}\right)\)
Section: 3
Chapter: 1
Effect: Computing an equivalent formula in CNF
Variables: \(\phi\) a formula
Time complexity: Exponential
Index: 18
Kind: Ex

Page: 12
Implementation: Computing NNF first.
Recursively, transform \(\bigvee\left(\bigwedge_jl_{ij}\right)\land \bigvee_{i'}\left(\bigwedge_{j'}l'_{i'j'}\right)\) into \(\bigvee_{i,i'}\left(\bigwedge_{j}l_{ij}\land\bigwedge_{j'}l'_{i'j'}\right)\)
Section: 3
Chapter: 1
Effect: Computing an equivalent formula in DNF
Variables: \(\phi\) a formula
Time complexity: Exponential

Name: Tseitin's encoding of conjunction.
Definition: \((a\vee\bigvee_i \neg x_i)\land\bigwedge_i(\neg a\lor x_i)\)
Page: 13, 14
Section: 3
Variables: \((x_i)\) atomic variables,
\(a\) representing \(\bigwedge_ix_i\)
Index: 21
Kind: Ex

Name: Tseitin's encoding of disjunction.
Definition: \((\neg a\lor\bigvee_i x_i)\land\bigwedge_i(a\lor \neg x_i)\)
Page: 13
Section: 3
Variables: \((x_i)\) atomic variables,
\(a\) representing \(\bigvee x_i\)
Index: 21
Kind: Ex

Name: Tseitin's encoding of negation.
Definition: \((\neg a\lor \neg x)\land(a\lor x)\)
Page: 13
Section: 3
Variables: \(x,y\) atomic variables,
\(a\) representing \(\neg x\)
Index: 21
Kind: Ex

Name: Tseitin's algorithm
Definition: Introducing a symbol \(a_\psi\) for each subformula \(\psi\) of \(\phi\).
\(a_\phi\land\bigwedge_\psi T_\psi\) where \(T_\psi\) is the encoding of \(\psi\)
Page: 13
Section: 3
Variables: \(\phi\) a formula
Index: 21
Kind: Ex

Name: Tseitin's encoding of atom
Definition: \((\neg a\lor x)\land(a\lor \neg x)\)
Page: 13
Section: 3
Variables: \(x\) atomic variable
\(a\) representing \(x\)
Index: 21
Kind: Ex

Name: A signature
Definition: A set of nonlogical symbols
Page: 16
Section: 4
Denoted by: \(\Sigma\)

Name: First-order logic
Definition: A set of variables
Page: 14 15
Section: 4
Definition2: A set of logical symbols: \(\land,\neg,\lor,\exists,\forall\)
Conjdef: All of
Definition3: A set of nonogical symbols: functions, predicate and constants
Name2: Predicate logic
Definition4: Syntax

Name: A free variable of \(\phi\)
Definition: A variable with a non-bound occurrence
Page: 16
Section: 4
Variables: \(\phi\) a FO formula

Name: A sentence
Definition: A formula without free variables
Page: 16
Section: 4

Name: A first-order \(\Sigma\)-theory
Definition: A set of \(\Sigma\)-sentences
Page: 16
Section: 4
Variables: \(\Sigma\) a signature
Denoted by: \(T\)

Name: A \(\Sigma\)-formula
Definition: A formula whose non-logical symbols belong to \(\Sigma\)
Page: 16
Section: 4
Variables: \(\Sigma\) a signature

Name: A \(T\)-satisfiable \(\Sigma\)-formula
Definition: A formula such that there exists a structure satisfying it and \(T\).
Page: 16
Section: 4
Variables: \(\Sigma\) a signature,
\(T\) a theory

Name: A fragment of a logic
Definition: A restriction of a logic concerning its logical symbols
Page: 16
Section: 4

Name: Equality logic
Definition: Quantifier-free fragment of the theory of equivalence relation over signature \(\Sigma=\{=\}\).
Page: 16
Section: 4

Name: Presburger arithmetic
Definition: The theory with signature \(\Sigma=\{0,1,+,=\}\) and usual axioms for integers
Page: 17
Section: 4

Name: Peano arithmetic
Definition: The theory with signature \(\Sigma=\{0,1,+,\times,=\}\) and usual axioms for integers
Page: 17
Section: 4

Question: We are mainly concerned with:
Answer: the satisfiability problem of the quantifier-free fragment of various first-order theories
Page: 17
Chapter: 1
Section: 4.1

Name: Ground formula
Definition: a formula whose variables are all free
Page: 17
Section: 4.1
Name2: Quantifier-free formula
Extra: statement

Name: Constraint satisfaction problem
Definition: Finding an assigment that satisfies a set of unquantified constraints
Page: 17
Section: 4.1
Abbreviation: CSP

Name: The language defined by \(T\)
Definition: The set of assignments which satisfy this theory
Page: 18
Section: 5
Variables: \(T\) a theory

Name: \(T'\) is more expressive than \(T\)
Definition: The set of languages which can be defined by \(T'\) formulas is a strict subset of the set of languages which can be defined by \(T\)-formulas
Page: 19
Section: 5
Variables: \(T,T'\) theories
Notation: \(T\prec T'\)
Example: 2CNF\(\prec\) propositional logic
Typ: transitive relation

Definition: CNF with restriction to clauses with 2 literals
Page: 19
Section: 5
Notation: 2-CNF

Name: Satisfiability Modulo Theories
Definition: The satisfiability problem for an arbitrary theory or combinations thereof
Page: 6
Section: 2
Abbreviation: SMT

Page: 17
Section: 4
Chapter: 1
Time complexity: Undecidable
Returns: Whether the sentence is true
Input: A Peano sentence

Page: 17
Implementation: Quantifier elimination
Time complexity: TimeAlternations(2^2^n^O(1), n) complete
Returns: Whether the sentence is True
Input: A Presburger sentence