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.

From this, you can derive:

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 →

ABA → B
001
011
100
111

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)": 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:
  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).
    ABC(A or B)(A or ¬C)(B or C)target
    1111 1 1 1
    1101 1 1 1
    1011 1 1 1
    1001 1 0 0
    0111 0 1 0
    0101 1 1 1
    0010 0 1 0
    0000 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 xi and a negative number −i referring to the negated variable ¬xi. 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