k-SAT to SQL Compiler

This website generates a SQL statement that you can use to solve k-SAT.
Given a k-CNF expression, a SQL statement is generated in 2^(N/2) time.
You can run the SQL statement in a standards-compliant database.
It will tell you whether the k-CNF is satisfiable.
The SQL expression contains a NOT IN expression on inputs of cardinality 2^(N/2).
If your database can run that NOT IN expression faster than quadratic time,
your database is the world's fastest SAT solver.

Waiting for input
Example: (x1 | !x2 | x3) & (!x1 | x4 | x2)
Generated by compileKcnfToSql(cnf)

Compiler Input


        

        

          
Accepted Input

          

            Clauses go in parentheses, joined with &. Literals inside clauses are joined
            with |. Negation can be written as !, ~, or -.
            Variables should be named x1, x2, x3, and so on.