1
$\begingroup$

Suppose a generalized version of k-SAT where the usual clauses (disjunctions of literals) are generalized to arbitrary Boolean functions of k variables. (For example, $(x \oplus (y \land z)), ((x \land z) \lor (y \land z))$ and $(x \implies z)$ could be generalized clauses for k = 3.)(Just a note: there are $2^{2^k}$ Boolean functions of k variables, and only $3^k$ of them are disjunctions of literals.)

My question is how fast can we solve the satisfiability for such formulas? Would you Provide an research paper that gives an algorithm for this problem and also gives us proof an upper bound on its running time . If, we can use randomness, (i) for example, k = 3, (ii) any arbitrary k.

$\endgroup$
8
  • $\begingroup$ "there are $2^{2^k}$ Boolean functions of k variables, and only $3^k$ of them are disjunctions of literals." Not sure why that's relevant: even when you make it an arbitrary circuit instead of a formula, you need exponentially large circuits to express an arbitrary boolean formula over n variables. Basically, you can't express an arbitrary element of a double exponentially sized set using only a polynomial amount of bits. $\endgroup$
    – rus9384
    Jan 26 at 9:16
  • 1
    $\begingroup$ As for the problem itself, this seems like a weaker variant of circuit-SAT which is in NP. Using the Tseytin transform on instances of your problem would produce SAT instances of $O(n\log n)$ size, so there is a trivial upper bound from SAT algorithms. $\endgroup$
    – rus9384
    Jan 26 at 9:32
  • $\begingroup$ For constant $k$, you can just replace each “generalized clause” with an equivalent CNF. This might increase the size of the input by a factor of $2^k$ (which is still a constant!), but it will preserve the number of variables $n$; since the running times of $k$-SAT algorithms (such as PPSZ) are normally expressed in terms of $n$ rather than the number of clauses, they will apply unmodified to your problem. $\endgroup$ Jan 26 at 10:29
  • $\begingroup$ @rus9384 it is much weaker: k is a constant, and the "generalized clauses" are connected by AND. Tseytin transform introduces new variables, you may get something even worse than (the indeed trivial bound) 2^n this way. $\endgroup$
    – A. H.
    Jan 26 at 13:39
  • $\begingroup$ I can’t elaborate if you don’t tell me what specifically is not clear to you. $\endgroup$ Jan 27 at 19:37

1 Answer 1

3
+50
$\begingroup$

Worst-case bounds on running time are usually not very informative for SAT solvers. In particular, on problem instances that arise in practice, often SAT solvers run a lot faster than the bounds would suggest. And the bounds are not very informative at helping us choose between two solvers or two algorithms, or identify which improvements are likely to help the most in practice.

In practice, the pragmatic approach is probably going to be to convert each "generalized clause" (i.e., each formula of k variables) to CNF using the Tseytin transform, then form a CNF formula $\varphi$ via the conjunction of all of the formulas obtained in this way, and solve $\varphi$ with an off-the-shelf SAT solver. This allows you to take advantage of all of the engineering in SAT solvers, which often make a big difference in practice, rather than starting from scratch.


If you care about worst-case running time bounds, a natural approach is to apply the method suggested by Emil Jeřábek. Specifically, convert each "generalized clause" to a CNF formula without introducing any new variables, then consider the conjunction $\varphi$ of those formula, and apply any existing SAT algorithm with worst-case running time bound to $\varphi$. This way, any worst-case running time bounds for SAT transfer immediately to your problem, too. Each "generalized clause" $C$ on $k$ variables can be converted to a CNF $\psi_C$ containing at most $2^k$ clauses. Each of those clauses has at most $k$ variables in it. Therefore, $\varphi = \land_C \psi_C$ is a $k$-CNF formula with $n$ variables, and can be solved with any algorithm for $k$-SAT.

For instance, 3SAT can be solved in $O^*(1.308^n)$ expected time using the PPSZ algorithm, so for $k=3$ it follows that your problem can be solved in $O^*(1.308^n)$ time, too. See

3-SAT faster and simpler---Unique-SAT bounds for PPSZ hold in general. Timon Hertli. SIAM J. Computing, vol 43 no 2, pp.718-729.

$\endgroup$
2
  • $\begingroup$ Thank you very much for your elaborative answer. Your mentioned paper given algorithm for k=3. Is there any paper in where there exists any algorithm for k=arbitrary? $\endgroup$
    – A. H.
    Feb 8 at 21:57
  • $\begingroup$ @user19121278, if you do a literature search starting from that paper, you will discover the answer to your own question. $\endgroup$
    – D.W.
    Feb 8 at 22:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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