### Problem introduction

Convert Circuit SAT to $k$-SAT, so it will only include clauses with 1 to $k$ variables with signs $\in \left\{\lor,\lnot\right\}$ between them. And all the clauses will be separated by $\land$ sign.### Solution using De Morgan's laws

In the nested expressions, for each operation $(y \star z)$, where $y,z$ are *variables*, and $\star$ is some operation, you create a new variable, and replace the $(y \star z)$ with the new variable and adding the clauses from**De Morgan's laws**equation to the final solution.

#### Example: Let it be a Circuit SAT $a \oplus b \oplus c$.

- Step one: Replace $a \oplus b$ with new variable $v1$. $v1 \equiv a \oplus b$
- Step two: Add
**De Morgan's laws**equation to the final solution. $(v1 \lor a \lor b) \land (a \lor \lnot b)$ - Step three: Repeat it with the remaining variables $v1 \oplus c$ and you will get the final result: $(v1 \lor a \lor b) \land (a \lor \lnot b) \land (v2 \lor v1 \lor c) \land (v1 \lor \lnot c)$

### Better way:

This could be solved using the truth table. It will take $2^n$ to build it, and while it seems like a lot, this is actually a very fast way. I show you how with our previous example.Lets build a truth table for $a \oplus b \oplus c$

a b c resultNow lets take all the false cases and convert them to true by adding not to the entire expression, the result will be $k$

0 0 0 |0

0 0 1 |1

0 1 0 |1

0 1 1 |0

1 0 0 |1

1 0 1 |0

1 1 0 |0

1 1 1 |1

**-SAT**,

**3-SAT**in this case:

$ (a \lor b \lor c) \land (a \lor \lnot b \lor \lnot c) \land (\lnot a \lor b \lor \lnot c) \land (\lnot a \lor \lnot b \lor c) $

Now lets try something more complicated: $(a \oplus b \oplus c) \lor \lnot(e \oplus f)$

To solve this lets first replace the expression $(a \oplus b \oplus c)$ with new variable $v1$. To do this lets build a truth table for $v1 \equiv (a \oplus b \oplus c)$

a b c v1|solutionNow we can add the not of this table to the final result:

0 0 0 0 |1

0 0 0 1 |0

0 0 1 0 |0

0 0 1 1 |1

0 1 0 0 |0

0 1 0 1 |1

0 1 1 0 |1

0 1 1 1 |0

1 0 0 0 |0

1 0 0 1 |1

1 0 1 0 |1

1 0 1 1 |0

1 1 0 0 |1

1 1 0 1 |0

1 1 1 0 |0

1 1 1 1 |1

$(a \lor b \lor c \lor \lnot v1 \land) \land (a \lor b \lor \lnot c \lor v1) \land (a \lor \lnot b \lor c \lor v1) \land (a \lor \lnot b \lor \lnot c \lor \lnot v1) \land (\lnot a \lor b \lor c \lor v1) \land (\lnot a \lor b \lor \lnot c \lor \lnot v1) \land (\lnot a \lor \lnot b \lor c \lor \lnot v1) \land (\lnot a \lor \lnot b \lor \lnot c \lor v1)$

And now we are left with: $v1 \lor \lnot(e \oplus f)$ Lets create a truth table for it

e f v1|result

0 0 0 | 1

0 0 1 | 1

0 1 0 | 0

0 1 1 | 1

1 0 0 | 0

1 0 1 | 1

1 1 0 | 1

1 1 1 | 1

And add the not to the finale equation we will get this final result:

$(e \lor \lnot f \lor v1) \land (\lnot e \lor f \lor v1) \land (a \lor b \lor c \lor \lnot v1 \land) \land (a \lor b \lor \lnot c \lor v1) \land (a \lor \lnot b \lor c \lor v1) \land (a \lor \lnot b \lor \lnot c \lor \lnot v1) \land (\lnot a \lor b \lor c \lor v1) \land (\lnot a \lor b \lor \lnot c \lor \lnot v1) \land (\lnot a \lor \lnot b \lor c \lor \lnot v1) \land (\lnot a \lor \lnot b \lor \lnot c \lor v1)$

This idea is easy to implement in to code. Converting Circuit

**SAT**to

**K-SAT**will be $O(2^CN)$ and it will produce less clauses and variables then using

**De Morgan's laws**