patternMinor
What's the average number of clauses modern SAT solvers can handle?
Viewed 0 times
satcannumberthewhatsolvershandleaveragemodernclauses
Problem
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?
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#74616, answer score: 5
Revisions (0)
No revisions yet.