CNF syntax: clauses joined by ∧ or &, literals joined by ∨ or |, negation ¬ or !. Maximum 20 variables.
—
Λ STRUCTURAL LOAD
—
SOLUTION COMPRESSION
—
SOLUTION-SPACE PHASE
Λ·P ≤ C = ln(10)
0
—
SEARCH TREE — ● visited× pruned● incumbent● optimum
0
VISITED NODES
0
EVALUATED ASSIGN.
0
PRUNED ASSIGN.
—
INCUMBENT
BRUTE FORCE
—
complete assignments evaluated
BRANCH & BOUND
—
complete assignments evaluated
① MaxSAT / SAT
VARIABLES
CLAUSES — green: SAT, amber: OPEN, red: DEAD
Exact reduction. Create one vertex for every literal occurrence. Join vertices from different clauses unless they are contradictory. One true literal chosen from each currently satisfied clause forms a clique; the same vertices form an independent set in the complement; all remaining vertices form a vertex cover. Thus OPTMaxSAT = ω(G) = α(Ḡ), and τ(Ḡ) = |V| − OPTMaxSAT.
② MAX CLIQUE
③ MAX INDEPENDENT SET
④ MIN VERTEX COVER
⑤ VERTEX 3-COLORING
T colorF colorB color
⑥ DIRECTED HAMILTONIAN CYCLE
⑦ EXACT SUBSET SUM
Variable items choose T/F once. Clause slack items complete every satisfied clause digit to the exact target; an unsatisfied clause cannot reach the target.
⑧ 0/1 KNAPSACK
Subset Sum → Knapsack: every item has weight = value, capacity = target T, required value = T. Feasibility forces exact equality.
Full chain. ①–④ share exact MaxSAT objective identities. ⑤ uses the standard T/F/B clause gadget for 3-CNF. ⑥ displays the directed variable-chain Hamiltonian certificate induced by the current assignment. ⑦–⑧ use an exact no-carry digit encoding with clause slack items.