Some of it also doubles as basic set theory, negation (¬, ¬) becoming complements, conjunction (∧, AND, ∧) becoming the union, disjunction (∨, OR, ∨) becoming the intersection.

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)

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

- A and (B or C) = (A and B) or (A and C)
- A or (B and C) = (A or B) and (A or C)

A | B | A → B |
---|---|---|

0 | 0 | 1 |

0 | 1 | 1 |

1 | 0 | 0 |

1 | 1 | 1 |

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)*.

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)*.

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

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

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

- Move NOTs inwards, with repeated De Morgan's laws and eliminating double negatives (
`¬¬X = X`

); - Distribute ORs inwards, by turning
`X or (Y and Z)`

into`(X or Y) and (X or Z)`

An example transformation:

- Initial formula:
**(A and B) or (A and C) or (B and ¬C)**. All NOTs are as inwards as they can be. - Parenthesize, so we only deal with clauses of two: (A and B) or
**(**(A and C) or (B and ¬C)**)**. - 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)**]**. - Shuffle the order around: (A and B) or
**[**(B or (A and C)) and (¬C or (A and C))**]**. - Apply the same rule again to the subclauses "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). Interestingly "(C or ¬C)" is a tautology: it cannot be false.

**[**(**(A or B) and (B or C)**) and (**(A or ¬C) and (C or ¬C)**)**]** - We can drop some extra parentheses within the right subclause, 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)]
- Now, to deal with the other side. So we don't get mixed up, let's sweep the right subclause 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). - Distribute again: D or (A and B) becomes (D or A) and (D or B).
- 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). - Left subclause: A or [(A or B) and (B or C) and (A or ¬C) and (C or ¬C)].
- Let's do this mechanically. Deep parenthesization first: A or ((A or B) and ((B or C) and ((A or ¬C) and (C or ¬C)))).
- (A or (A or B)) and (A or (((B or C) and ((A or ¬C) and (C or ¬C)))))
- (A or (A or B)) and ((A or (B or C)) and (A or (((A or ¬C) and (C or ¬C)))))
- (A or (A or B)) and ((A or (B or C)) and ((A or (A or ¬C)) and (A or (C or ¬C))))
- 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)
- 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)

- Right subclause: B or [(A or B) and (B or C) and (A or ¬C) and (C or ¬C)].
- We could do the same deep parenthesization thing as with the left subclause... or, since we're humans, we can skip ahead.
- 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 Я).
- Therefore, B or [(A or B) and (B or C) and (A or ¬C) and (C or ¬C)] becomes...
- (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...
- (A or B) and (B or C) and (B or A or ¬C) and (B or C or ¬C)

- 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)). - 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).
- 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).
- 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)**. - 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.

- After eliminating the useless clauses, we are left with
**(A or B) and (B or C) and (A or ¬C)**. - 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

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

`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