WEBVTT

1
00:00:00.000 --> 00:00:02.400
This overview explains how matrices,

2
00:00:02.400 --> 00:00:09.733
evaluators, decision diagrams, solvers, counters,
and simplifiers serve different requests.

3
00:00:09.733 --> 00:00:16.333
Choosing a tool before naming the output can leave
the caller with the wrong artifact or the wrong count.

4
00:00:16.633 --> 00:00:20.467
A direct evaluator answers a specified point.

5
00:00:20.467 --> 00:00:25.333
A satisfying-assignment procedure finds an input making F true.

6
00:00:25.333 --> 00:00:31.133
An equivalence procedure establishes that F and the displayed De Morgan expression agree

7
00:00:31.133 --> 00:00:33.233
over the full universe.

8
00:00:33.233 --> 00:00:38.667
These are different services, even when they use the same Boolean rule.

9
00:00:38.667 --> 00:00:42.833
A decision diagram for or can test A first.

10
00:00:42.833 --> 00:00:48.867
If A is one, the answer is already one; otherwise it follows a B test.

11
00:00:48.867 --> 00:00:52.833
This compact path structure can answer a point query without writing

12
00:00:52.833 --> 00:00:55.233
all four truth outputs.

13
00:00:55.233 --> 00:01:00.333
Other tasks require additional traversal or bookkeeping.

14
00:01:00.333 --> 00:01:04.400
A full-vector method delivers every output in order.

15
00:01:04.400 --> 00:01:10.000
A counting method can return three without enumerating a public list of every witness.

16
00:01:10.000 --> 00:01:13.133
The caller's required output determines whether either is an

17
00:01:13.133 --> 00:01:17.067
acceptable replacement for the other.

18
00:01:17.389 --> 00:01:22.129
SAT asks whether there is any input that makes a Boolean rule true.

19
00:01:22.129 --> 00:01:24.803
A satisfying input is a witness.

20
00:01:24.803 --> 00:01:30.632
That question differs from evaluating one input chosen in advance.

21
00:01:30.932 --> 00:01:38.343
BDD means binary decision diagram: yes-or-no variable tests form paths that can share later branches.

22
00:01:38.343 --> 00:01:45.437
A miter is the exclusive-or of two outputs; it is one exactly where they disagree.

23
00:01:45.737 --> 00:01:49.003
A logic cover lists accepting terms.

24
00:01:49.003 --> 00:01:54.765
For A or the conjunction of B and C, the two terms are A, and B and C.

25
00:01:54.765 --> 00:01:59.041
Logic minimization seeks a simpler equivalent description.

26
00:01:59.041 --> 00:02:04.011
The required output determines which tool is suitable.

27
00:02:04.022 --> 00:02:07.355
A complete truth layout, a reusable evaluator,

28
00:02:07.355 --> 00:02:14.222
a decision diagram, a witness, a count and a
simplified expression are different outputs.

29
00:02:14.222 --> 00:02:17.589
Start by naming the deliverable.

30
00:02:17.589 --> 00:02:24.022
For a feature rule, a point-validity query
can evaluate one complete selection.

31
00:02:24.022 --> 00:02:31.522
SAT can seek a satisfying selection; an equivalence
miter can seek a counterexample to agreement.

32
00:02:31.522 --> 00:02:37.822
A BDD represents the function under
an ordering and supports further operations.

33
00:02:37.822 --> 00:02:43.189
Espresso-style minimization asks for a reduced logic cover.

34
00:02:43.189 --> 00:02:48.222
Symbolic algebra asks for a symbolic transformation.

35
00:02:48.222 --> 00:02:53.589
Packed evaluation can enumerate a complete ordered truth vector.

36
00:02:53.589 --> 00:02:58.989
Scalar counting and projected counting deserve their own branches.

37
00:02:58.989 --> 00:03:04.055
If auxiliary inputs give several witnesses for one selected feature choice,

38
00:03:04.055 --> 00:03:09.022
a full-assignment count and a distinct projected count differ.

39
00:03:09.022 --> 00:03:17.289
This is an interface map, not a claim that every
optional backend is installed or universally fastest.

40
00:03:17.589 --> 00:03:21.755
For or, there are three complete satisfying assignments.

41
00:03:21.755 --> 00:03:24.789
Each specifies both A and B.

42
00:03:24.789 --> 00:03:28.422
Counting these full assignments gives three.

43
00:03:28.422 --> 00:03:31.389
Project each full assignment onto A.

44
00:03:31.389 --> 00:03:36.489
The two assignments with A one become the same selected answer, so deduplication leaves

45
00:03:36.489 --> 00:03:38.222
zero and one.

46
00:03:38.222 --> 00:03:41.322
The projected count is two.

47
00:03:41.322 --> 00:03:46.855
A tool returning the full-model count has not automatically returned the projected count.

48
00:03:46.855 --> 00:03:50.689
Similarly, one witness is not all witnesses.

49
00:03:50.689 --> 00:03:55.955
The toolbox becomes easier to use when its entries are described by artifacts and exact

50
00:03:55.955 --> 00:04:01.955
contracts rather than broad claims of solving Boolean problems.

51
00:04:01.955 --> 00:04:01.968
Start with the caller's required artifact.

52
00:04:01.968 --> 00:04:05.855
Start with the caller's required artifact.

53
00:04:05.855 --> 00:04:15.009
For projected counting, count each selected assignment
once even when it has several auxiliary witnesses.