Skip to main content
The 2024 Developer Survey results are live! See the results

Tag Info

Hot answers tagged sat-solvers

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 ...
• 956
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 ...
• 163k
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 ...
• 278k
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,...
• 163k
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. ...
• 163k
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 ...
1 vote

Practical hard 3-sat instances

you could have a look at at Zero-One Designs Produce Small Hard SAT Instances The instances are generated drawing from combinatorial block design and yield instances of up to 100 variables that were ...
• 143

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