Title: Theory / Unimportant / CS / Algo / Decision Procedures - Kroening Strichman V2 / 2 Propositional logic
Tags: examplesSwitchExample1 fromAlgorithm hasNotNewEffectReturnsMeaning oldAlgoNewName hasSeenConjDef
On every note of this deck, unless a note says otherwise:
Chapter: 2

Question: Syntax of propositional logic.
Answer: formula : formula ∧ formula | ¬formula | (formula) | atom
atom : Boolean-identifier | true | false
Page: 27
Chapter: 2
Section: 1

Name: Propositional formula
Page: 29
Section: 2.1
Denoted by: \(\mathcal B\)

Name: stochastic search for SAT
Definition: the solver guesses a full assignment, and then, if the formula is evaluated to false under this assignment, starts to flip values of variables according to some (greedy) heuristic.
Page: 30
Section: 2.1

Question: How to solve randomly generated satisfiable CNF ?
Answer: stochastic search
Page: 30
Chapter: 2
Section: 2.1

Name: A decision level
Definition: The depth of a decision in the binary decision tree
Page: 31
Section: 2.2
Variables: In CDCL

Name: Ground level
Definition: Level 0 of the decision binary tree
Page: 32
Section: 2.2
Variables: In CDCL

Question: The level of assignments implied regardless of the current assignments ?
Answer: Ground level
Page: 32
Chapter: 2
Section: 2.2
Context: in CDCL

Name: A satisfied clause
Definition: A clause with at least one satisfied literal
Page: 32
Section: 2.2
Variables: \(A\) an assignment of variables
Index: 3
Kind: Def
Example: \((\neg x_1\lor x_2)\)
Applied to: For assignment \(\{x_1\mapsto 0\}\)

Name: A conflicting clause
Definition: A clause whose literals are assigned but not satisfied
Page: 32
Section: 2.2
Variables: \(A\) an assignment of variables
Index: 3
Kind: Def
Example: For assignment \(\{x_1\mapsto 0,x_2\mapsto1\}\):
\((x_1\lor \neg x_2)\)

Name: A unit clause
Definition: A clause with a unique unasigned literal
Page: 32
Section: 2.2
Variables: \(A\) an assignment of variables
Index: 3
Kind: Def
Example: For assignment \(\{x_1\mapsto 0\}\):
\((x_1\lor x_2)\)

Name: An unresolved clause
Definition: A clause wich is neither satisfied, nor conflicting, nor unit
Page: 32
Section: 2.2
Variables: \(A\) an assignment of variables
Index: 3
Kind: Def
Example: For assignment \(\{x_1\mapsto 0\}\):
\((x_1\lor x_2\lor\neg x_3)\)

Name: \(C\) is an antecedant clause of \(l\)
Definition: \(C\) is a unit clause with only unassigned litteral \(l\)
Page: 32
Section: 2.2
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
\(A\) an assignment,
\(C\) a clause,
\(l\) a literal
Name2: \(l\) is implied by \(C\)

Definition: A unit clause with only unassigned litteral \(l\), used by an algorithm to assign's \(l\) value
Page: 32
Section: 2.2
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
\(A\) an assignment,
\(l\) a literal
Notation: \(Antecedent(l)\)

Page: 30
Implementation: Traversing and backtracking on a binary tree, in which internal nodes represent partial assignments, and the leaves represent full assignments.
Section: 2.1
Chapter: 2
Name: Conflict-Driven Clause Learning

Page: 33-34
Implementation: DECIDE() choose an unassigned variable
BCP(): whether a conflict is encountered
Analyze-Conflict(): A decision level which the solver should bactrack to, or -1
BackTrack(dl): erase decisions taken after level dl
Section: 2.3
Chapter: 2
Name: CDCL-SAT
Returns: Decide whether a Boolean formula is satisfiable

Definition: \(x_i\) is assigned the value True at decision level \(dl\)
Page: 33
Section: 2.3
Variables: \(x_i\) a variable
\(dl\) a decision level
Notation: \(x_i\verb+@+dl\)

Definition: \(x_i\) is assigned the value False at decision level \(dl\)
Page: 33
Section: 2.3
Variables: \(x_i\) a variable
\(dl\) a decision level
Notation: \(\neg x_i\verb+@+dl\)

Name: An implication graph
Definition: Each node is labeled with the literal that it represents and the decision level at which it entered the partial assignment.
Page: 33-34
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
Definition2: There is an edge \((v_i,v_j)\) if \(\neg v_i\in Antecedent(v_j)\), labeled with \(Antecedent(v_j)\)
Conjdef: A labeled directed acyclic graph
Definition3: Plus potentially a conflict node, \(\kappa\) An edge from conflicting clauses to the conflicting node.
Intuition: A partial assignment at some moment of the algorithm

Question: A root node of an implication graph corresponds to
Answer: decisions,
Page: 35
Chapter: 2
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),

Question: An internal node of an implication graph corresponds to
Answer: implications through BCP
Page: 35
Chapter: 2
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),

Name: A conflict graph
Definition: An implication graph with a conflict node
Page: 35
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),

Name: Learning
Definition: Adding conflict clause to a set of constraint.
Page: 35
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
Context: Propositional logic

Name: A conflict clause
Definition: A clause which is implied by \(\mathcal B\)
Page: 35
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
Context: Propositional logic

Name: An asserting clause
Definition: A clause which force an immediate implication after backtracking
Page: 36
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
Context: Propositional logic

Name: A separating cut in \(G\)
Definition: A minimal set of edges whose removal breaks all paths from the root nodes to the conflict node
Page: 37
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
\(G\) a conflict graph
Context: Propositional logic
Index: 7
Kind: Def

Name: The reason side
Definition: The side of the cut that includes all the roots
Page: 37
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
\(G\) a conflict graph
\(C\) a separating cut in \(G\)
Context: Propositional logic
Index: 7
Kind: Def

Name: The conflict side
Definition: The side of the cut that includes no roots
Page: 37
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
\(G\) a conflict graph
\(C\) a separating cut in \(G\)
Context: Propositional logic
Index: 7
Kind: Def

Question: When the solver enters decision level dl for the \(n\)-th time
Answer: the partial assignment is distinct from the \(n-1\) first times it entered this level
Page: 38
Chapter: 2
Section: 2.3
Variables: \(\mathcal B=\bigwedge_i\bigvee_jl_{ij}\),
\(G\) a conflict graph
\(C\) a separating cut in \(G\)
Index: 8
Kind: Theo