3
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ The popular implementation of this idea is branch-and-bound, a technique for solving integer programs. $\endgroup$ – Yuval Filmus Sep 17 at 10:29
  • $\begingroup$ @YuvalFilmus Branch and bound is provably exponential, while I'm trying to use the fact that the number of initial clauses is polynomial and to keep the number of generated clauses small (polynomial). But what has my idea to do with branch and bound? Why are they equivalent? I don't see the link. $\endgroup$ – Zirui Wang Sep 17 at 12:03
  • $\begingroup$ Most people believe in the exponential time hypothesis. $\endgroup$ – Yuval Filmus Sep 17 at 12:05
  • $\begingroup$ @YuvalFilmus I'm fine with whatever belief people may have, but I'm trying to think of ways of attacking the problem mathematically. Like what Hardy said to Ramanujan, mathematicians can't count on what Gods told him and therefore need proofs. The general consensus might be right but at the same time worthless to a mathematician, who is purely rational. Like what Einstein said, it's not necessary to have a thousand people criticizing him, but only one to prove him wrong. My idea is novel; do you object? $\endgroup$ – Zirui Wang Sep 17 at 12:17
0
$\begingroup$

The answer to the partial question is no. It’s impossible to be so efficient by a counting argument. First, there are $2^n$ cells, each of which is either colored or not. So there are $2^{2^n}$ possible configurations, each of which has to be represented in polynomial space. This is impossible.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.