3 votes
Accepted

SAT solvers for counting the number of solutions

Yes, they are known as #SAT solvers. Some of them are exact, some of them are approximate. Some of them are based on a version of DPLL that exhaustively find every solution in a factorized way. Some ...
holf's user avatar
  • 936
3 votes
Accepted

How fast can we make generalized k-SAT?

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 ...
D.W.'s user avatar
  • 159k
2 votes

Showing SAT is auto-reducible

Autoreducibility was introduced in Buhrman, Fortnow and Torenvliet, Using autoreducibility to separate complexity classes. Here is the (informal) definition (page 520): A set $L$ is autoreducible if ...
Yuval Filmus's user avatar
2 votes
Accepted

Specialized SAT solver (?)

The best solution I know of is to use a SAT solver. I don't know whether there is a better solution. I don't see any proof that an arbitrary 3SAT problem can be reduced to it. (OK, strictly speaking,...
D.W.'s user avatar
  • 159k
2 votes

Could SAT solvers be significantly more efficient if they allowed for non-CNF formula?

That's a natural idea. However, to the best of my knowledge, despite attempts, no one has succeeded in making such an approach do better than just converting to CNF and using an existing SAT solver. ...
D.W.'s user avatar
  • 159k
2 votes

Can an optimization algorithm be "universal"?

Even if there were, remember that there is no free lunch in search and optimization. An optimization algorithm necessarily trades proficiency in one class of problems for inefficiency in another class ...
ubadub's user avatar
  • 315
1 vote

How to find the learned clause from a UIP cut

First, some observations: Setting all literals in a reason set to true leads to a conflict through unit propagation. One can replace a non-decision literal from a reason set with its in-neighbors in ...
Tim Vermeulen's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible