Reduce the SAT problem to the SET SPLITTING problem. These problems are defined as follows:

• SAT: given a boolean formula $F$ in conjunctive normal form, is $F$ satisfiable?
  More formally, this problem can be defined as the following set:
  $$\{ F=C_1\wedge\ldots\wedge C_n \mid F\text{ satisfiable} \}$$
• SET SPLITTING: given a collection of finite sets $S_1,\ldots,S_n$, is there a partition of $S_1\cup\ldots\cup S_n$ into two sets $A$ and $B$ such that no $S_i$ is entirely contained in $A$ or in $B$?
  More formally, this problem can be defined as the following set:
  $$\{ \langle S_1,\ldots,S_n\rangle \mid S_1,\ldots,S_n\text{ finite sets}\;\wedge\;\exists A,B: (A\cup B=(S_1\cup\ldots\cup S_n)\;\wedge\;A\cap B=\emptyset\;\wedge\;\forall i\in\{1,\ldots,n\}: (S_i\cap A\neq\emptyset\;\wedge\;S_i\cap B\neq\emptyset))\}$$

The input and output of the reduction conform to the following data types:

• in: struct {
        numvars: int
        clauses: array of array of int
      }
  

  The input is a boolean formula in conjunctive normal form: in.numvars specifies the number of variables occurring in the formula, and in.clauses is the list of clauses. Each clause is a list of literals, and each literal is a positive or negative integer: a positive integer $x$ represents the $x$’th variable, and a negative integer $-x$ represents the negation of the $x$’th variable. Such an $x$ takes values between $1$ and in.numvars.
  
  
  Note: The input has at least one clause, every clause has at least one literal, and there are no repeated literals in a clause. Thus, in.numvars is at least $1$.

• out: array of array of string
  

  The output is a list of sets. The elements of the sets are integers or strings.
  
  
  Note: If the output is an empty list, then the partition trivially exists. If the list has an empty set, then no partition exists.