Automated Reasoning

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

$$(P \land \Delta|P) \lor (\lnot P \land \Delta|\lnot P)$$

Deduction theorem

\(\alpha\text{ implies }\beta, \alpha \models \beta,\text{ iff }\alpha \Rightarrow \beta \text{ is valid}\)

If \(\alpha\) is a sentence that doesn't mention \(P\), then \(\Delta \models \alpha\) iff what?

$$\Delta \models \alpha\text{ iff }\exists P \Delta \models \alpha$$

Propositional logic sentence validity

A sentence is valid iff it is true at every world

Existential quantification

$$\exists P \Delta = (\Delta|P) \lor (\Delta|\lnot P)$$

AKA:

• Forgetting \(P\) from \(\Delta\)
• Projecting \(\Delta\) on all variables but \(P\)

$$\Delta \models \exists P \Delta$$

If \(\alpha\) is a sentence that does not mention \(P\), then \(\Delta \models \alpha\text{ iff }\exists P \Delta \models \alpha\)

Refutation theorem

\(\alpha\text{ implies }\beta, \alpha \models \beta,\text{ iff }\alpha \land \neg \beta \text{ is inconsistent}\)

Directed resolution

With variable ordering \(P_1, P_2, \ldots, P_n\):

1. \(P_j\)-resolvents should be generated only after all \(P_i\)-resolvents have been generated, \(j > i\)
2. The generation of \(P_j\)-resolvents cannot involve clauses that mention variables \(P_i\), \(j > i\)

Refutation complete for any variable ordering.

SATII algorithm

Variables named \(P_1, \ldots, P_n\)

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 \(-1\) 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 \(P_1, \ldots, P_n\)

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

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 \(x \lor C_1 = (l_1, \ldots, l_m)\) and \(\lnot x \lor C_2 = (o_1, \ldots, o_n)\) yields compensation clauses:

$$x \lor C_1 \lor \lnot o_1\\x \lor C_1 \lor o_1 \lor \lnot o_2\\\vdots\\x \lor C_1 \lor o_1 \lor o_2 \lor \cdots \lor \lnot o_n\\\lnot x \lor C_2 \lor \lnot l_1\\\lnot x \lor C_2 \lor l_1 \lor \lnot l_2\\\vdots\\\lnot x \lor C_2 \lor l_1 \lor l_2 \lor \cdots \lor \lnot l_m$$

Random K-SAT CNF generation

\(m\) clauses are randomly generated of length \(k\) with \(n\) variables. When \(\frac{m}{n}\) is small, \(P(\text{SAT})\) is close to 1, when \(\frac{m}{n}\) is large, \(P(\text{SAT})\) is close to 0, and the \(P(\text{SAT}) = 0.5\) transition occurs at \(\frac{m}{n} \approx 4.24\).

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 \(1\))

Directed resolution rules and resolve clauses on \(x_i\) only if they don't contain complementary literals on \(x_j \neq x_i\). Resolve over \(x\) by removing original clauses \(x \lor C_1=(l_1,\ldots,l_m)\) and \(\lnot x \lor C_2=(o_1,\ldots,o_n)\) and adding resolvent and compensation clauses.

With \(k\) empty clauses as a result, \(k\) is guaranteed to be the minimal cost and remaining clauses \(\Gamma\) is guaranteed to be satisfiable. Every world satisfying \(\Gamma\) has cost \(k\).

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

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 \(C\), each \(2\) disjuncts of \(C\) are logically contradictory

E-MAJ-SAT

Is there an \(\mathbf{X}\)-instantiation under which the majority of \(\mathbf{Y}\)-instantiations are satisfying?

Prime implicates (PI)

CNF such that:

• No clause subsumes another
• If a clause is implied by the CNF, it must be implied by a clause in the CNF

Polytime for:

• CO
• CE
• ME
• VA
• IP
• SE
• EQ

DNNF minimum cardinality

1. Assign cardinality 1 to negative variables and 0 to positive variables
2. or-nodes ← minimum cardinality of disjuncts
3. and-nodes ← sum cardinality of conjuncts

Model counting (#SAT)

How many satisfying assignments?

DNNF language

Decomposable subset of NNF. Polytime for:

• CO (linear)
• CE
• ME

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 \(X\), check consistency, condition on \(\lnot X\), 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 \(C\), the conjuncts of \(C\) do not share variables

Prime implicants (IP)

DNF such that:

• No term subsumes another
• If a term implies the DNF, it must imply a term in the DNF

Polytime for:

• VA
• IP
• SE
• EQ

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):

• SE
• EQ

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:

• VA
• IP
• CT
• EQ?

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:

• SAT(A ∨ B) iff SAT(A) or SAT(B)
• SAT(A ∧ B) iff SAT(A) and SAT(B) (because decomposability)
• SAT(X) = true
• SAT(¬X) = true
• SAT(true) = true
• SAT(false) = false

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 \((X \land \alpha) \lor (\lnot X \land \beta)\), where \(X\) is a variable and \(\alpha\) and \(\beta\) are decision nodes. \(\text{dVar}(\text{decision node})\) denotes the variable \(X\).

MAJ-MAJ-SAT

Is there a majority of \(\mathbf{X}\)-instantiations under which the majority of \(\mathbf{Y}\)-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 \(C\), each disjunct of \(C\) mentions the same variables

Cutset in caching for OBDD

Cutset_i is the set of clauses mentioning a variable ≤ v_i and a variable > v_i

OBDD Apply function

Fxi=1 and Fxi=0 are \(F|x_i\) and \(F|\lnot x_i\), 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 \(1\) or \(0\) 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

• CD
• SFO
• ∧B
• ∨B
• ¬

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 \(x_1, \ldots, x_{j-1}\) to constants and which depend on \(x_j\) is the number of reduced OBDD nodes labeled \(x_j\)

Reduced OBDD

Canonical OBDD as there is a unique reduced OBDD for fixed variable order. Apply:

• Deletion rule: {Z₁, Z₂} → X →⤑ Y ⇒ {Z₁, Z₂} → Y
• Merge rule: {A, B} → X → sinks, {C, D} → X → sinks ⇒ {A, B, C, D} → X → sinks

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 \(f\) and OBDD \(g\) on the first variable appearing in either according to the variable order. That variable becomes the decision node with the high child \(f \land g\) each conditioned on the positive variable and the low child \(f \land g\) 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

SDD apply operation

With \((\mathbf{X}, \mathbf{Y})\)-partition of \(f\):

$$(p_1, q_1) \ldots (p_n, q_n)$$

and \((\mathbf{X}, \mathbf{Y})\)-partition of \(g\):

$$(r_1, s_1) \ldots (r_m, s_m),$$

the \((\mathbf{X}, \mathbf{Y})\)-partition of \(f \circ g\):

$$\forall i,j: (p_i \land r_j, q_i \circ s_j)\ |\ p_i \land r_j \neq \text{false}.$$

Therefore, apply is \(O(m \times n)\), polytime.

SDD compression

\((\mathbf{X}, \mathbf{Y})\)-partition is compressed if no equal subs:

$$f = (g_1, h_1) \ldots (g_n, h_n)\\h_i \neq h_j\text{ for all }i \neq j$$

\(f(\mathbf{X}, \mathbf{Y})\) has a unique compressed \((\mathbf{X}, \mathbf{Y})\)-partition

Number of vtrees over \(n\) variables?

$$\begin{aligned}n! \times C_{n-1} &= n! \times \frac{(2(n-1))!}{n!(n-1)!}\\&= \frac{(2(n-1))!}{(n-1)!}\end{aligned}$$

Number of dissections over \(n\) variables of a vtree

$$C_{n-1} = \frac{(2(n-1))!}{n!(n-1)!}$$

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

• Positive instance remains positive if some features flipped from \(-\) to \(+\)
  • \((+, -, -, +) \Rightarrow (+, -, +, +), (+, +, -, +), (+, +, +, +)\)
• Negative instance remains negative if some features flipped from \(+\) to \(-\)
  • \((+, -, -, +) \Rightarrow (+, -, -, -), (-, -, -, +), (-, -, -, -)\)
• Example is Susan's correct answers include Jack's correct answers
  • Susan should pass if Jack passed

Health state \(\psi\)

Term over all health variables \(ok_1, \ldots, ok_n\). It is a diagnosis iff \(\psi\) is consistent with \(\Delta \land \alpha\).

Classifier robustness

What is expected robustness over all possible inputs?

$$\text{model-robustness}(f) = \frac1{2^n} \sum_\mathbf{x} \text{robustness}_f(\mathbf{x})$$

Computing min-cardinality diagnoses

Represent health condition \(\text{health}(\Delta, \alpha)\) 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 \(w\) such that \(w \models \Delta\)

Negative instance is a world \(w\) such that \(w \models \lnot \Delta\)

Instance robustness

How many features do we need to flip so that classifier's decision is flipped?

$$\text{robustness}_f(\mathbf{x}) = \min_{\mathbf{x}': f(\mathbf{x}') \ne f(\mathbf{x})} d(\mathbf{x}, \mathbf{x}')$$

Linear time in OBDD

Implicate implicant duality

\(\alpha\) is a prime implicate of \(\Delta\) iff \(\lnot\alpha\) is a prime implicant of \(\lnot\Delta\)

Decision bias

Decision on instance \(X\) is biased iff it can be different on an instance \(Y\) that disagrees with \(X\) 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 \(\Delta\) with \(n\) components, system observation \(\alpha\) is normal iff \(\Delta \land \alpha \land ok_1 \land \ldots \land ok_n\) is consistent

Health variable

Variable for each component that captures the state of that component

Complete reason

Disjunction of all sufficient reasons

Health condition \(\text{health}(\Delta, \alpha)\)

$$\exists X_1, \ldots, X_m (\Delta \land \alpha)$$

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.

1. Add consensus nodes to each or-node
   1. \((\lnot A \land \alpha) \lor (A \land \beta) \Rightarrow (\alpha \land \beta)\)
2. Kill each and-\(\alpha\) incompatible with instance

System observation in model-based diagnosis

Term over non-health variables (variables other than \(ok_i\))

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 \(\Delta\) and \(\lnot\Delta\) DNNF forms required).

1. Condition on negative features
2. Assign \(\infty\) to false, \(1\) to positive literals, and \(0\) to negative literals and true
3. Compute minimum cardinality
4. Kill disjuncts with non-minimal values
5. Enumerate

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:

• Boolean function \((A\!+\!\overline{C})(B\!+\!C)(A\!+\!B)\)
• Prime implicants \(AB, AC,B\overline{C}\)
• Instance \(AB\overline{C}\), Decision \(1\)
• Sufficient reasons \(AB, B\overline{C}\)

• Prime implicants of negation \(\overline{A}C, \overline{B}\overline{C},A\overline{B}\)
• Instance \(\overline{A}BC\), Decision \(0\)
• Sufficient reasons \(\overline{A}C\)