Background: Recently, I obtained the following equivalent problem to SAT. We are given as input a CNF formula with $n$ variables and $m$ clauses. Suppose we have an $n$-dimensional hyper-cube centered at the origin. We perform the following cut-and-color operation $m$ times, each time for a clause.
Let’s say there are $k$ literals in this clause. For the $i$th literal with variable numbered $x$ and sign $s$, we cut the hyper-cube or what is remaining with the hyper-plane perpendicular to $x$th axis and keep the $s$-signed half. After $k$ times cutting, color the remaining part red.
If, after all clauses have been processed this way, the entire hyper-cube is red, announce UNSAT. Otherwise announce SAT.
This is the problem. Basically an uncolored part corresponds to an assignment whose reverse is satisfiable, because no clause covers this assignment or, in other words, this assignment does not contain any clause when both assignments and clauses are viewed as sets.
Phrased this way, SAT is really a geometric representation problem, and the key is to keep track of colored parts with only polynomial-sized storage.
Question: What is known about high-dimensional geometry of a hyper-cube, especially related to this problem? My current difficulty is with visualization.
Difficult example: Consider the following simple CNF formula: $$(x_1\lor x_2)\land(x_3\lor x_4)\land\cdots\land(x_{2k-1}\lor x_{2k}),$$ or in DIMACS format
1 2
3 4
...
2k-1 2k
where $k>0$. The challenge is to represent the colored parts by (preferably polynomially many) non-overlapping clauses only. Below is the best I can do:
- $k=1$:
1 2
- $k=2$:
1 2
-1 3 4
1 -2 3 4
- $k=3$:
1 2
-1 3 4
1 -2 3 4
-1 -3 5 6
-1 3 -4 5 6
1 -2 -3 5 6
1 -2 3 -4 5 6
- $k=4$:
1 2
-1 3 4
1 -2 3 4
-1 -3 5 6
-1 3 -4 5 6
1 -2 -3 5 6
1 -2 3 -4 5 6
-1 -3 -5 7 8
-1 -3 5 -6 7 8
-1 3 -4 -5 7 8
-1 3 -4 5 -6 7 8
1 -2 -3 -5 7 8
1 -2 -3 5 -6 7 8
1 -2 3 -4 -5 7 8
1 -2 3 -4 5 -6 7 8
As you can see, it's growing exponentially.
Partial question: Do you have a way to do this example (not the general problem) using only polynomially many clauses? This is the difficulty I can't handle right now. It's easy to see that the interactions among the original clauses grow exponentially with $k$. So if you can prove that this example is impossible to do, then this non-overlapping-clauses approach won't work and we need to find something else.
Code: I posted my code here. My approach was implemented but it’s still exponential without the partial problem above solved. You can observe that.
One potential weakness is that any algorithm implementing my idea can actually count the number of satisfying assignments, solving a #P-complete problem. Not only that, it remembers in memory exactly which assignments are not satisfying (one simple way to do this is to just remember the initial clauses) and it can enumerate these without much overhead, because the final clauses are non-overlapping. Is that something enough to prove my idea is always exponential-time?
