3
$\begingroup$

For a 3SAT formula with $n$ variables and $m$ clauses, I am interested in counting the number of isomorphic formulas (isomorphic in the sense that they are logically equivalent and have the same number of variables and clauses). I assume that we can invert the sense of any variable (swap all $x_i$ with $\lnot x_i$) and permute any of the variables. The first should give $2^n$ and the second should give $n!$.

Is this all of the isomorphisms, or am I overlooking anything?

If this is correct, then I assume that the number of distinct 3SAT formulas with $n$ variables and "distinct clauses" is equal to $\frac{2^m}{2^nn!}$, where $m$ is the number of 3-clauses over $n$ variables in which all variables are distinct. I assume that $m=2n(2n-2)(2n-4)$. Does that sound right?

EDIT 1

The formula above isn't correct, because it overcounts permutations. There are formulas which only contain $n'<n$ variables, even though $n$ are available. The number of permutations must be computed on the basis of actual variables rather than "potential variables" for each formula. :( I guess that means the actual formula is very complicated, and I'll have to think about it some more. Would be very happy if a smarter person could spot a nice, short expression for it before I do. ;)

EDIT 2

Since my question has created more confusion than I anticipated, allow me to motivate it a bit more. What I really want to do is explore the structure of the 3SAT formula space by generating the set of all formulas for a given number of variables (like, 4, to start out with, since I think there are already > 1 million of these). However, I realize that many of the formulas are "trivially equivalent", in the sense that you can transform one directly into the other by permuting variables, inverting them, etc. Since there are $m=8n^3$ 3-clauses of $n$ variables, and $2^m$ formulas over these clauses, my time is not well-served by looking at what are effectively "duplicate formulas". So, I would like to identify all the "easy dupes" ahead of time, and avoid generating them at all. As a check that I have done this correctly, and not eliminated actually interesting formulas, I would like to at least have a confident count of how many "basically unique" formulas are left after removing "rotations" and "reflections".

The reason I called this "sameness property" "isomorphism" is because I was thinking in terms of the graph representations that are sometimes used to analyze SAT. I feel that what I am looking for is precisely the set of formulas which produce isomorphic graphs under any "reasonable" 1-1 mapping from formula->graph. I understand that SAT is only interested in logical equivalence, and that extraneous clauses are irrelevant, for the most part. However, the problem of getting the satisfiable answer for a given formula depends exactly on its set of clauses, and so they are significant for me. Part of my program is to figure out which "structural differences" are irrelevant so that a given formula can be categorized into a particular logical equivalence class in the first place! Thus, defining "equivalence" in terms of logical equivalence is putting the cart before the horse in terms of what I'm trying to accomplish.

What I have discovered so far is that the formula space is "nested" in the sense that naively generating all $2^{8n^3}$ formulas over $n$ variables will also generate all the formulas over $0..n-1$ variables. Thus, I should analyze the formulas incrementally, as a kind of recurrence relation. As far as removing chaff, the first and most obvious rule to apply is that a variable can only occur in a base clause at most once. This excludes degenerate 2-clauses and units, as well as tautologies. I hope we can agree that tautologies are not interesting and that unit clauses make the problem significantly easier. I don't want to focus on those, because such formulas are equivalent to a "harder" formula in which the given unit must instead be derived, all other clauses being equal. Analyzing the harder formula essentially gives the unit-containing formula for free.

My idea to eliminate rotations is to enforce a constraint. Let $count(x)=$ number of times that the literal $x$ occurs in the formula. Then we can make the variables "distinct" by requiring that $\forall i>0, count(x_i)\leq count(x_i-1)$. This just means that the "earliest" variables occur "most often". Or equivalently, that the variables are sorted in order of cardinality. Within a clause, we can also sort variables by demanding that for $(x_i, x_j, x_k), i<j<k$. To remove "reflections", we can similarly constrain "signs" by imposing the constraint $\forall i,count(\lnot x_i)\leq count(x_i)$. This means that we will force the "positive" literals to dominate the "negative" ones. I believe that these constraints will allow me to generate the set of formulas which contain no "trivial duplicates", but I may have missed some opportunities.

In the end, I expect the formula space to have some kind of [disconnected?] fractal border between the satisfiable and unsatisfiable regions. If this border is very complicated and detailed (which I suppose most computer scientists assume), then that lends weight to the idea that there are truly "exponentially hard" regions within the space. If, on the other hand, there are surprisingly uniform regions across the whole space, then obviously a method which compresses this space would yield a more efficient algorithm.

I hope this sheds light on what I am trying to achieve with my notion of "equivalence" or "isomorphism". I welcome a better term to describe this property, if one is available.

$\endgroup$
  • 1
    $\begingroup$ Please define (your version of) "3SAT formula". Does it allow less than 3 variables in a clause? Does it allow duplicate variables in a clause? $\endgroup$ – Apass.Jack May 29 at 22:12
  • 1
    $\begingroup$ Please define "logically equivalence" of 3SAT formulas. Are $(x_1\lor x_2\lor x_3)\land(x_1\lor x_2\lor x_4)$ and $(x_1\lor x_2\lor x_4)\land(x_1\lor x_2\lor x_3)$ logically equivalent? Are two unsatisfiable formulas with the same number of clauses equivalent? $\endgroup$ – Apass.Jack May 29 at 22:15
  • $\begingroup$ Is "$\frac{2^m}{2^nn!}$" always an integer? $\endgroup$ – Apass.Jack May 29 at 22:19
  • $\begingroup$ 1) I would like to disallow "short" clauses or duplicate variables. That's what I meant by "distinct clause" (although I see the wording is ambiguous). 2) Yes, because you just permuted $x3$ and $x4$, so all solutions to the first are solutions to the second with those two variables swapped. 3) Usually no. If we convert the formula to a graph, using one of the typical transforms, the graphs should be isomorphic. 4) Good question! I don't think it is, which is why I think I'm missing something, but I'm not sure what. $\endgroup$ – Lawnmower Man May 29 at 22:53
  • $\begingroup$ Suppose $s_1$ and $s_2$ are two 3-SAT formulas. Can you specify an algorithm that returns true iff they are logically equivalent? Or can you define "logically equivalence" of 3SAT formulas? Or will you consider an answer that defines "logically equivalence" of 3SAT formulas on behalf of you? $\endgroup$ – Apass.Jack May 30 at 4:06

Your Answer

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

Browse other questions tagged or ask your own question.