3
$\begingroup$

It's already known that size doesn't matter always (for SAT problems).

But is there evidence (from real data from: benchmarks or real cases) on how many clauses an average SAT solver can handle nowadays?

Another issue that derives is that once they find a solution, most don't stress the fact about finding alternative solution. Is there a reason?

$\endgroup$
  • 1
    $\begingroup$ The reason is that for a decision problem, a "yes" or "no" answer is all that is needed. If, say, you wanted the number of truth assignments that satisfied the given expressions, that is a different question (worth studying, as well. $\endgroup$ – Rick Decker Apr 27 '17 at 17:07
  • $\begingroup$ Welcome to CS.SE! Normally on this site the expectation is that you ask one question per post. $\endgroup$ – D.W. Apr 27 '17 at 17:21
5
$\begingroup$

You're asking two questions. I'll answer your first question.

There's no simple answer. It depends on the structure of the problem. There are problems with millions of clauses that can be handled by a SAT solver. There are also problems with only tens of thousands of clauses (perhaps fewer) that can't be handled by SAT solvers.

The number of clauses isn't a great predictor of whether a SAT solver will be able to solve the problem in a reasonable amount of time.

Rick Decker has answered your other question.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ So, a problem with as little as 50,000 - 200,000 clauses (and a reasonable amount of literals) is destined to fail on a modern SAT solver? $\endgroup$ – Anna K. Apr 27 '17 at 19:34
  • 1
    $\begingroup$ @AnnaK., no. That's pretty much the opposite of what I wrote. On the contrary, you can't tell whether the SAT solver is destined to fail from just the number of clauses or literals. The most reliable way to find out is to try it. $\endgroup$ – D.W. Apr 27 '17 at 19:57
  • $\begingroup$ @AnnaK.: In typical real-world problems, some fairly simple heuristics will allow many clauses to be consolidated or eliminated. If a problem starts with 500,000 clauses but they're inter-related in ways that allow 498,000 of them to be eliminated easily, that problem may be much easier than a problem with 10,000 clauses whose relationships are not amenable to simplification. $\endgroup$ – supercat Apr 27 '17 at 20:12
  • $\begingroup$ @D.W. A classmate of mine was insisting that he tried a (relatively) small problem in a program called Z3 but he says program doesn't end. I tried telling him that something is his formulation (from a programming aspect) might be wrong but he insists that it's the problem itself. Even if that's the case, won't Z3 try to perform some kind of exhaustive analysis (since it doesn't timeout)? (TLDR: doesn't exhaustive analysis provide a solid "yes/no" even to hard problems that are small in size? $\endgroup$ – Anna K. Apr 27 '17 at 20:23
  • $\begingroup$ @AnnaK., this site isn't the right place for back-and-forth discussions or follow-up questions. Our format is a question-and-answer site: post a single question, and get a single answer. If you have a specific follow-up question, you can post it separately using the 'Ask Question' button (though I'm not sure the specific one you mention is fleshed out enough to be answerable). You can take a look at our tour and look at other questions on this site to get a better feeling for how this site works. $\endgroup$ – D.W. Apr 27 '17 at 21:22

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.