Summarized Boolean logic: rules and transformations

Some of it also doubles as basic set theory, negation (¬, ¬) becoming com­plements, con­junction (∧, AND, ∧) becoming the union, dis­junction (∨, OR, ∨) becoming the inter­section.

De Morgan's laws

Turn ANDs into ORs and back again, as long as you have NOTs.

• ¬(A or B) = ¬A and ¬B
• ¬(A and B) = ¬A or ¬B

From this, you can derive:

• A or B = ¬(¬A and ¬B)
• A and B = ¬(¬A or ¬B)

Boolean distri­bu­tivity

There are two rules of replacement. These are very handy when transforming into and between different normal forms.

1. A and (B or C) = (A and B) or (A and C)
2. A or (B and C) = (A or B) and (A or C)

Implication →

Wikipedia calls this the material conditional. (The truth table for this is the one I always forget; it has one false, but where?)

a → b is equivalent to, and CNF-encoded as, (¬a ∨ b). By extension, a → (b ∨ c) becomes (¬a ∨ b ∨ c), and a → (b ∧ c) becomes (¬a ∨ b) ∧ (¬a ∨ c).

Equivalence

Or, as Wikipedia calls it, the logical biconditional. ↔'s HTML entity is ↔.

CNF-encoding a ↔ b: equivalent to (a → b) ∧ (b → a), therefore equivalent to (¬a ∨ b) ∧ (a ∨ ¬b).

XOR, or the exclusive disjunction

Symbols: ⊻ (⊻, ⊻), ⊕ (⊕).

CNF-encoding a ⊻ b: equivalent to (¬a ∨ ¬b) ∧ (a ∨ b).

Conjunctive normal form

CNF is an AND of OR clauses. Given a clause that already consists only of ANDs and ORs (and NOTs, of course), but hap­hazardly organized, trans­forming into CNF goes thusly:

1. Move NOTs inwards, with repeated De Morgan's laws and eliminating double negatives (¬¬X = X);
2. Distribute ORs inwards, by turning X or (Y and Z) into (X or Y) and (X or Z)

An example trans­formation:

1. Initial formula: (A and B) or (A and C) or (B and ¬C). All NOTs are as inwards as they can be.
2. Parenthesize, so we only deal with clauses of two: (A and B) or ((A and C) or (B and ¬C)).
3. Distribute the OR of the inner formula, with X=(A or C), Y=B and Z=¬C: (A and B) or [ ((A and C) or B) and ((A and C) or ¬C) ].
4. Shuffle the order around: (A and B) or [(B or (A and C)) and (¬C or (A and C))].
5. Apply the same rule again to the sub­clauses "B or (A and C)" and "¬C or (A and C)":
   • B or (A and C) is turned into (A or B) and (B or C), with "B or A" reordered into "A or B";
   • ¬C or (A and C) is turned into (A or ¬C) and (C or ¬C). Interes­tingly "(C or ¬C)" is a tauto­logy: it cannot be false.
   Pop the trans­formed sub­clauses back into the main formula: (A and B) or [((A or B) and (B or C)) and ((A or ¬C) and (C or ¬C))]
6. We can drop some extra paren­theses within the right sub­clause, since it's in CNF now: (A and B) or [(A or B) and (B or C) and (A or ¬C) and (C or ¬C)]
7. Now, to deal with the other side. So we don't get mixed up, let's sweep the right sub­clause under the symbol D: D=[(A or B) and (B or C) and (A or ¬C) and (C or ¬C)], and our formula is (A and B) or D = D or (A and B).
8. Distribute again: D or (A and B) becomes (D or A) and (D or B).
9. Expand D. The previous formula becomes ([(A or B) and (B or C) and (A or ¬C) and (C or ¬C)] or A) and ([(A or B) and (B or C) and (A or ¬C) and (C or ¬C)] or B).
10. Left subclause: A or [(A or B) and (B or C) and (A or ¬C) and (C or ¬C)].
    1. Let's do this mechanically. Deep paren­thesi­zation first: A or ((A or B) and ((B or C) and ((A or ¬C) and (C or ¬C)))).
    2. (A or (A or B)) and (A or (((B or C) and ((A or ¬C) and (C or ¬C)))))
    3. (A or (A or B)) and ((A or (B or C)) and (A or (((A or ¬C) and (C or ¬C)))))
    4. (A or (A or B)) and ((A or (B or C)) and ((A or (A or ¬C)) and (A or (C or ¬C))))
    5. Collapse parentheses, because "(X or (Y or Z)) = X or Y or Z": (A or A or B) and (A or B or C) and (A or A or ¬C) and (A or C or ¬C)
    6. Remove redundancies, because "X or X" is just X: (A or B) and (A or B or C) and (A or ¬C) and (A or C or ¬C)
11. Right subclause: B or [(A or B) and (B or C) and (A or ¬C) and (C or ¬C)].
    1. We could do the same deep paren­thesi­zation thing as with the left subclause... or, since we're humans, we can skip ahead.
    2. The rule, a bit informally, is that X or (Y and Z and W and ... and Я) = (X or Y) and (X or Z) and (X or W) and ... and (X or Я).
    3. Therefore, B or [(A or B) and (B or C) and (A or ¬C) and (C or ¬C)] becomes...
    4. (B or A or B) and (B or B or C) and (B or A or ¬C) and (B or C or ¬C), which is equivalent to...
    5. (A or B) and (B or C) and (B or A or ¬C) and (B or C or ¬C)
12. Pop the left and right subclause back into the formula: ((A or B) and (A or B or C) and (A or ¬C) and (A or C or ¬C)) and ((A or B) and (B or C) and (B or A or ¬C) and (B or C or ¬C)).
13. Drop parentheses: (A or B) and (A or B or C) and (A or ¬C) and (A or C or ¬C) and (A or B) and (B or C) and (B or A or ¬C) and (B or C or ¬C).
14. Reorder: (A or B) and (A or B) and (A or B or C) and (A or B or ¬C) and (A or ¬C) and (A or C or ¬C) and (B or C) and (B or C or ¬C).
15. Drop the extra (A or B), because it's redundant. Solution: (A or B) and (A or B or C) and (A or B or ¬C) and (A or ¬C) and (A or C or ¬C) and (B or C) and (B or C or ¬C).
16. This still isn't in its most minimal form, though. Optimizations we can make:
    • ((A or B) and (A or B or C)) is equivalent to (A or B). This is clear if one writes out their truth tables. (A or B) is true 6 our of 8 times, while (A or B or C) is true 7 out of 8 times – the same six that (A or B) is true, and also the A=0, B=0, C=1 case. When ANDed together, that one case drops out and we are left with the six cases of (A or B).
    • For the same reason, ((A or B) and (A or B or ¬C)) is equivalent to (A or B).
    • (A or C or ¬C) is always true, because (C or ¬C) is always true. Having an always-true clause in a CNF formula is pointless, because CNF formulas essentially work by defining where falsehoods must be, and an always-true clause doesn't help with that; x and 1 equals x.
    • (A or C or ¬C) is likewise always true, and thus pointless in the formula.
17. After eliminating the useless clauses, we are left with (A or B) and (B or C) and (A or ¬C).
18. One further optimization becomes apparent if we write out truth tables: we can get rid of (A or B) and just have (B or C) and (A or ¬C) as the formula. All of the falsehoods we need are found in (A or ¬C) and (B or C).

    A	B	C	(A or B)	(A or ¬C)	(B or C)	target
    1	1	1	1	1	1	1
    1	1	0	1	1	1	1
    1	0	1	1	1	1	1
    1	0	0	1	1	0	0
    0	1	1	1	0	1	0
    0	1	0	1	1	1	1
    0	0	1	0	0	1	0
    0	0	0	0	1	0	0

Applications: DIMACS and WCNF file formats

These are standard text-based file formats used to pass CNF and weighted-CNF formulas to SAT and MaxSAT solvers.

DIMACS consists of lines of ASCII text. A line starting with c is a comment and ignored. The mandatory preamble line has the form p cnf [num-variables] [num-clauses]. The lines after that provide clauses, a clause being a series of (base-10) numbers, a positive number i referring to the variable x_i and a negative number −i referring to the negated variable ¬x_i. Each clause is terminated by a single 0.

DIMACS WCNF is very similar, but gives weights to each clause. The preamble is changed to p wcnf [num-vars] [num-clauses] [top-weight], and every clause has a number – the weight of the clause – prepended to it. The top-weight is the weight that is to be regarded as "infinite", used to mark hard clauses that must be satisfied. For example, p wcnf 5040 59049 9999 is the preamble of a MaxSAT instance with 5040 variables, 59049 clauses, and with hard clauses having a weight of 9999, with any clause with a weight less than 9999 being soft, i.e. optional.

oatcookies.neocities.org | last edit: 2021-05-15, created on or before 2021-03-07 | index