Linear resolution strategy
Front
Active users
6
All-time users
7
Favorites
0
Last updated
4 years ago
Date created
Sep 30, 2020
Week 1
(9 cards)
Linear resolution strategy
Resolve two nodes only if one of them is root or an ancestor of the other
Propositional logic sentence completeness
A sentence is complete iff it is true at exactly one world
Propositional logic sentence consistency
A sentence is consistent iff there is at least one world at which it is true
Boole's expansion theorem, often referred to as the Shannon expansion
Deduction theorem
If is a sentence that doesn't mention , then iff what?
Propositional logic sentence validity
A sentence is valid iff it is true at every world
Existential quantification
AKA:
If is a sentence that does not mention , then
Refutation theorem
Week 2
(12 cards)
Directed resolution
With variable ordering :
Refutation complete for any variable ordering.
SATII algorithm
Variables named
SATII(Δ, d = 0: depth):
if Δ={}: return {}
if Δ={{}}: return FAIL
if L=SATII(Δ|Pd+1,d+1)≠FAIL:
return L∪{Pd+1}
if L=SATII(Δ|¬Pd+1,d+1)≠FAIL:
return L∪{¬Pd+1}
return FAIL
Assertion level
Second highest level in the asserting clause or if it doesn't exist
Asserting clause
Negation of conflict set leading to conflict-driven clause with one variable setting at the last decision level
First UIP
UIP closest to contradiction
Decision tree algorithm for ordered buckets
genDecTree(Γi, …, Γj; term: α = true):
if Γi|α, …, Γj|α are all empty:
return node labelled true
if Γj|Pj∧α contain empty clause:
H ← false
else
H ← genDecTree(Γi, …, Γj-1; Pj∧α)
if Γj|¬Pj∧α contain empty clause:
L ← false
else
L ← genDecTree(Γi, …, Γj-1; ¬Pj∧α)
return node Pj, high/low children H/L
Conflict set
Collection of variable settings that can be blamed for a contradiction
Empowering clause
Clause entailed by knowledge base, when added to knowledge base empowers unit resolution to discover a contradiction after setting a particular variable
DPLL+ algorithm
DPLL+(Δ):
D←() {empty decision sequence}
Γ←{} {empty learned clauses}
while true do:
if unit res contradict in (Δ,Γ,D):
if D=(): return false
else
α←asserting clause
m←assertion level clause α
D←first m+1 decisions in D
add clause α to Γ
else
if liters l and ¬l not implied
by unit res from (Δ,Γ,D):
D←D;l
else
return true
DPLL algorithm
DPLL(Δ: clausal form):
(I,Γ)=UNIT-RESOLUTION(Δ)
if Γ={}: return I
if {}∈Γ: return FAIL
choose a literal l in Γ
if L=DPLL(Γ∪{{l}})≠FAIL: return L∪I
if L=DPLL(Γ∪{{¬l}})≠FAIL: return L∪I
return FAIL
SATI algorithm
Variables named
SATI(Δ, d = 0: depth, n: num vars):
if d=n and Δ={}: return {}
if d=n and Δ={{}}: return FAIL
if L=SATI(Δ|Pd+1,d+1,n)≠FAIL:
return L∪{Pd+1}
if L=SATI(Δ|¬Pd+1,d+1,n)≠FAIL:
return L∪{¬Pd+1}
return FAIL
Unique implication point (UIP)
Variable setting at the highest decision level which lies on every path from the latest decision to the contradiction
Week 3
(8 cards)
Unsatisfiable core
Subset of clauses of original CNF that are unsatisfiable
For each C∈Δ:
Δ'=Δ\C
if Δ' is UNSAT:
Δ=Δ'
Compensation clauses (unweighted)
Adjusts incorrect costs induced by classical resolution. Resolving and yields compensation clauses:
Random K-SAT CNF generation
clauses are randomly generated of length with variables. When is small, is close to 1, when is large, is close to 0, and the transition occurs at .
GSAT local search algorithm
GSAT(Δ,Tm,Tr): {Tm,Tr→moves,restarts}
i←1
while i≤Tr:
i←i+1
w*←random world
c*←num clauses Δ falsified by w*
j←1
while j≤Tm:
j←j+1
if c*=0: return w*
else
w*←rand neighbor falsifying
smallest num clauses Δ
c*←#clauses falsified by w*
return FAIL
Counting DPLL (CDPLL)
Uses exhaustive DPLL
CDPLL(Γ, n: number variables):
if Γ={}: return 2ⁿ
if {}∈Γ: return 0
choose literal l in Γ
(I⁺,Γ⁺)=UNIT-RESOLUTION(Δ∪{{l}})
(I⁻,Γ⁻)=UNIT-RESOLUTION(Δ∪{{¬l}})
return CDPLL(Γ⁺,n-|I⁺|)+CDPLL(Γ⁻,n-|I⁻|)
MaxSAT resolution (weights )
Directed resolution rules and resolve clauses on only if they don't contain complementary literals on . Resolve over by removing original clauses and and adding resolvent and compensation clauses.
With empty clauses as a result, is guaranteed to be the minimal cost and remaining clauses is guaranteed to be satisfiable. Every world satisfying has cost .
Asserting clause learning algorithm in modern SAT solvers for certifying UNSAT
Guaranteed to derive the first UIP asserting clause from the conflict
lc=clause that became empty from UR
while (lc is not asserting):
l=literal in lc falsified last
lc=resolvent of lc∧ ¬l's reason
return lc {learned clause}
2-literal watching scheme
A literal is asserted if it evaluates to true under current variable setting and resolved if it evaluates to false, otherwise free. L₁ and L₂ interchangeable:
For each clause watch literals L₁,L₂
Once L₁→resolved, search unresolved L
If none found, check other literal L₂
If L₂ free, then unit and L₂ implied
If L₂ resolved, all resolved→empty
If L₂ asserted, clause subsumed
Week 4
(32 cards)
Simple-disjunction
Children of each or-node are leaves that share no variables, aka clause
DNNF clausal entailment
Because of refutation theorem, look for inconsistency when conditioning knowledge base on negation of clause and then conjoining negation of clause. Works on partial decomposable NNF too if clause contains variables that didn't allow for full decomposability.
MODS language
DNF of every satisfying model
NNF determinism
For each disjunction , each disjuncts of are logically contradictory
E-MAJ-SAT
Is there an -instantiation under which the majority of -instantiations are satisfying?
Prime implicates (PI)
CNF such that:
Polytime for:
DNNF minimum cardinality
Model counting (#SAT)
How many satisfying assignments?
DNNF language
Decomposable subset of NNF. Polytime for:
f-NNF languages
Flatness, height of each sentence is at most 2. CNF and DNF are examples.
FBDD language
Free BDD subset of BDD and d-DNNF. Has test-once property.
DNNF model enumeration (ME)
Linear in the number of models because CD + CE is linear. Condition on , check consistency, condition on , check consistency, and recurse.
BDD language
Binary decision diagram, subset of d-NNF
MAJ-SAT
Are majority of instantiations satisfying?
s-NNF language
Smooth subset of NNF. No extra polytime capabilities.
NNF decomposability
For each conjunction , the conjuncts of do not share variables
Prime implicants (IP)
DNF such that:
Polytime for:
Structured decomposability
Each and-node has the same distribution of variables among its branches mapped to a sub-tree in a v-tree. Enables conjoining DNNF circuits in polytime.
OBDD language
Ordered BDD subset of FBDD. Polytime for (all 8 queries, 6 inherited):
Weighted model counting (WMC)
Summed weights of satisfying assignments. Each literal (positive and negative variants) gets a weight, multiply weights for each model/assignment.
sd-DNNF minimum cardinality models algorithm
Use DNNF minimum cardinality algorithm and throw out non-minimal cardinality disjuncts
DNNF sub-circuit
Choose one disjunct for each or-node
d-DNNF language
Subset of d-NNF and DNNF. Polytime for:
d-NNF language
Deterministic subset of NNF. No extra polytime capabilities.
DNNF satisfiability
Set all variables to true because SAT can be propagated to leaves:
DNNF existential quantification
AKA projection, replace all variables to be existentially quantified with true for the same reason as satisfiability
NNF decision node
Labeled true, false, or is an or-node having the form , where is a variable and and are decision nodes. denotes the variable .
MAJ-MAJ-SAT
Is there a majority of -instantiations under which the majority of -instantiations are satisfying?
Simple-conjunction
Children of each and-node are leaves that share no variables, aka term
sd-DNNF language
Subset of s-NNF and d-DNNF
DNF language
Subset of f-NNF and DNNF with simple-conjunction
NNF smoothness
For each disjunction , each disjunct of mentions the same variables
Week 5
(10 cards)
Cutset in caching for OBDD
Cutseti is the set of clauses mentioning a variable ≤ vi and a variable > vi
OBDD Apply function
Fxi=1 and Fxi=0 are and , respectively:
Apply(F,G,*):
if F,G are sinks: return F*G
if (F,G) in cache:
return cache[F,G]
else
let xi be 1st var in F,G
h = Apply(Fxi=1,Gxi=1,*)
l = Apply(Fxi=0,Gxi=0,*)
if h = l: return h
n = unique-node(xi,h,l)
cache[F,G] = n
return n
sd-DNNF counting graph with constraints
Set variables to or based on constraints. If a variable constraint is added or removed, multiply the difference from its previous value with its partial derivative and add to previous count.
OBDD transformations
Decision-DNNF language
Subset of d-DNNF where or-nodes are always decision nodes, but not necessarily and-nodes or leaves
Theorem relating number of sub-functions to number of reduced OBDD nodes
The number of distinct sub-functions obtained by fixing to constants and which depend on is the number of reduced OBDD nodes labeled
Reduced OBDD
Canonical OBDD as there is a unique reduced OBDD for fixed variable order. Apply:
sd-DNNF weighted model counting algorithm
Multiply and-gates and add or-gates just like unweighted model counting, but with weights for variables
OBDD conjoin algorithm
Because of Shannon/Boole's expansion, condition OBDD and OBDD on the first variable appearing in either according to the variable order. That variable becomes the decision node with the high child each conditioned on the positive variable and the low child each conditioned on the negative variable. Recursively do the same to those children.
sd-DNNF model counting algorithm
All variable leaves and true has 1 model, false has 0 models, or-nodes add counts of their disjuncts, and and-nodes multiply counts of their conjuncts
Week 6
(4 cards)
SDD apply operation
With -partition of :
and -partition of :
the -partition of :
Therefore, apply is , polytime.
SDD compression
-partition is compressed if no equal subs:
has a unique compressed -partition
Number of vtrees over variables?
Number of dissections over variables of a vtree
Week 7
(21 cards)
System description in model-based diagnosis
Knowledge-base that describes how a system is supposed to behave
Classifier bias
Classifier is biased iff one of its decisions is biased. In other words, one of its decisions has a sufficient reason with at least one protected feature.
IP form
Representation of knowledge-base as a disjunction of its prime implicants
Monotone classifier
Health state
Term over all health variables . It is a diagnosis iff is consistent with .
Classifier robustness
What is expected robustness over all possible inputs?
Computing min-cardinality diagnoses
Represent health condition as a DNNF and do min-cardinality in linear time
Monotone circuit
All occurrences of a variable in a circuit are either always positive or always negative. Existential quantification in linear time.
Positive instance vs negative instance of propositional formulas
Positive instance is a world such that
Negative instance is a world such that
Instance robustness
How many features do we need to flip so that classifier's decision is flipped?
Linear time in OBDD
Implicate implicant duality
is a prime implicate of iff is a prime implicant of
Decision bias
Decision on instance is biased iff it can be different on an instance that disagrees with on protected features only
Decision is biased iff each of its sufficient reasons contains at least one protected feature
Normal in regards to system observations
For system description with components, system observation is normal iff is consistent
Health variable
Variable for each component that captures the state of that component
Complete reason
Disjunction of all sufficient reasons
Health condition
Compute reason circuit from decision-DNNF
Linear time. Equivalent to complete reason. Instance must be positive, otherwise need to work with negation of decision-DNNF.
System observation in model-based diagnosis
Term over non-health variables (variables other than )
Hamming distance between instances
# variables instances disagree on
Minimum cardinality explanation on positive instance
Minimum cardinality in this case means to minimize necessary positive features. Linear time for DNNF (both and DNNF forms required).
Sufficient reasons with PI explanations
Given a positive instance, select compatible prime implicants. Given a negative instance, select compatible prime implicants of negation of boolean function. Example: