0
$\begingroup$

Are there any SAT solver algorithms which break up a 3SAT sequence of $m$ clauses into $n$ parts, solve these $n$ parts in parallel and then combine the solutions from each part into a final solution for the original problem?

I am interested in algorithms/heuristics for finding a solution when each of the $n$ parts can have up to $t$ solutions each. Specifically if we can prevent the algorithm from devolving into a $t^n$ worst case search?

I tried searching on google but couldn't find anything useful to my query.

$\endgroup$
  • 2
    $\begingroup$ I would think that the problem with such an approach is that the $n$ parts could be coupled, possibly making one part's solution incompatible with another part's solution. $\endgroup$ – Adrian Keister Feb 19 '18 at 20:15
  • $\begingroup$ The parts can be selected such that if all solutions of 1 part are not compatible with another part, then the system can be shown to be unsatisfiable. That means for satisfiable systems all parts will have one solution that is compatible with all other parts. This would mean finding all solutions for a part, which is feasible if the parts are small enough. I haven't been able to work out how to select parts such that they have a maximum of $T$ solutions, where $T$ is small enough so that a $T^n$ search is feasible. $\endgroup$ – gautam Feb 19 '18 at 20:22
  • $\begingroup$ That sounds like a very computationally expensive parts selection process. Parallelization could be a great way to generate solution candidates, but the problem is that there's no way to know if the solutions are compatible a priori. I suppose you could try to find $n$ parts that are "as decoupled as possible", using some metric of coupling. Unfortunately, I don't have any references for you. The 3SAT problem is really tough, because an almost-good solution might not be any better than a horrible one. You have no nice, continuous, cost function telling you how good your solution is. $\endgroup$ – Adrian Keister Feb 19 '18 at 20:29
  • 2
    $\begingroup$ Is this what you have in mind? $\endgroup$ – Fabio Somenzi Feb 19 '18 at 20:38
  • $\begingroup$ @FabioSomenzi That is interesting. Thanks for sharing. $\endgroup$ – GoodDeeds Feb 19 '18 at 20:49
0
$\begingroup$

This is a method I have been playing with. It has $T^x$ behavior, but this may not be as bad as you think.

My solver works for monotone, linear Exactly 1 in 3 SAT, ml-X3SAT. Monotone means all variables are positive and linear means no two clauses have more than one variable in common. ml-X3SAT is NP-Complete. I also assume we can apply the Two Singleton reduction rule. A singleton is a variable that appears exactly once in the instance. We can remove any clause with two singletons, like $(a, s_1, s_2)$, and assume $s1=NOT(a), s_2=False$. This rule allows us to assume no clause has more than one singleton. If no variable occurs in more than two clauses then ml-X3SAT reduces to a Perfect Matching instance solvable in polynomial time.

Choose a variable that appears in $k\geq 3$ clauses. I call these $k$ clauses an index. $k$ clauses that share a variable have $2k+1$ variables and $2^k+1$ satisfying assignments. It turns out the worst case is $k=3$ so assume the first index has three clauses. Remove all clauses that share a variable with one of the three clauses in the first index. Now choose a variable in the remaining instance that appears in three or more clauses. Make clauses with this variable the second index. Continue this process of selecting indices until no variable appears in more than two of the remaining clauses.

By construction, no index shares a variable with any other index. If we choose one satisfying assignment from each index then we will either find a contradition or the remaining clauses reduce to a Perfect Matching instance. Because no clause has more than one singleton, any satisfying assignment of the $k$ clauses in an index will also reduce another $k$ clauses. Each clause in an index must share a variable with a non-index clause. If $m$ is the number of clauses in the original instance then we will not need more than $m/2k$ indices.

If we assume $k=3$ for every index then we can solve an instance in $O(9^{m/6})$ or $O(2^{.53m})$. This isn't nearly as good as the best known, but it is not bad for a simple analysis. It shows you want to choose a small number of indices where each index has a large number of clauses and variables and a small number of satisfying assignments. The number of satisfying assignments, $T$, is not as important as the number of indices, $x$, in $T^x$. Any method of reducing the number of indices is good. For example, after choosing an index we can apply reduction rules to the remaining clauses to minimize the remaining instance.


Answer to question:

$m$ is the number of clauses in the entire $ml-X3SAT$ instance. $k$ is the number of clauses in each index. We assume all of these clauses in an index share a variable in common. Because we assume the instance is "linear", these clauses can't share more than one variable. We also assume $k \geq 3$ because if no variable is in more than two clauses then the instance reduces to perfect matching and is solvable in polynomial time.

$k$ clauses with a variable in common have $2^k+1$ satisfying assignments. There is one solution where the shared variable is true and all of the other variables are false. All of the other solutions have the shared variable false and one of the other two variables in each clause is true. This gives us $2^k$ more solutions.

Because no clause has more than one singleton, we know each clause in the index shares a variable with at least one non-index clause. Each satisfying assignment of the index clauses removes at least $2k$ clauses. This means we need no more than $m/2k$ indexes to "cover" the entire instance. We will need to examine no more than $(2^k+1)^{m/2k}$ assignments to find any solution.

When we convert this to base 2 the exponent will have $log(2^k+1) \approx k$ giving us $2^{mk/2k} = 2^{m/2}$ for large $k$. $k=3$ is the worst case because the "$1$" in $2^k+1$ is large compared to $2^3$. For example for $k=10$ we get $1025^{m/20} = 2^{.50007m}$.

$\endgroup$
  • $\begingroup$ I am not clear when you say in the third paragraph that $k = 3$ is the worst case for the number of clauses in the first index. Wouldn't having more clauses mean $m$ is larger thus $O(2^{.53m})$ be larger also, $m$ being the number of clauses in the first index? $\endgroup$ – gautam Mar 9 '18 at 20:42

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.