Questions regarding solver programs for the boolean satisfiability problem.

learn more… | top users | synonyms

10
votes
3answers
139 views

Multicore SAT Solver

I am trying to solve a 25k clauses 5k variables SAT problem. As it has been running for an hour (precosat) and I'd like to solve bigger ones afterwards, I'm looking for a multi-core SAT-Solver. As ...
4
votes
2answers
122 views

Convert $\sum x_i = y$ to 3-sat

I have a simple looking question. What is the most efficient conversion of $\sum_{i=1}^n x_i = y$ to 3-sat? Here $x_i$ is either $1$ or $0$ and $y$ is some positive integer. Can you do better than ...
2
votes
0answers
59 views

Why Is Alloy not an Answer Set Programming system?

Alloy's front page doesn't mention ASP, but the description sounds like ASP (finding solutions consistent with a logical spec). And Alloy isn't listed in the Wikipedia ASP article. Yet ASP systems ...
9
votes
1answer
288 views

Encoding 1-out-of-n constraint for SAT solvers

I'm using a SAT solver to encode a problem, and as part of the SAT instance, I have boolean variables $x_1,x_2,\dots,x_n$ where it is intended that exactly one of these should be true and the rest ...
5
votes
1answer
140 views

When to use SAT vs Constraint Satisfaction?

If I have a hard problem, one standard approach is to express it as a SAT instance and try running a SAT solver on it. Another standard approach is to express it as a constraint satisfaction problem, ...
1
vote
2answers
507 views

Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
6
votes
2answers
115 views

Complexity of GF(2) and applications to cryptography

If I have a system of N polynomial equations with N unknowns in GF(2): What are some good methods to solve them? What are some software packages or libraries that implement this? What's the highest ...
9
votes
1answer
157 views

Unification vs. SAT solver

I read on Wikipedia that unification is a process of solving the satisfability problem. At the same time, I know that such solvers are called "SAT solvers" or "SMT solvers". So, are they different ...
7
votes
2answers
201 views

Introduction into first order logic verification

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
5
votes
1answer
138 views

Running time of CDCL compared to DPLL

What's the complexity of Conflict-Driven Clause Learning SAT solvers, compared to DPLL solvers? Was it proven that CDCL is faster in general? Are there instances of SAT that are hard for CDCL but easy ...
10
votes
1answer
186 views

Can top SAT-solvers factor easy numbers?

Modern SAT-solvers are very good at solving many real-world examples of SAT instances. However, we know how to generate hard ones: for instance use a reduction from factoring to SAT and give the RSA ...
4
votes
1answer
177 views

Resolution complexity versus a constrained SAT algorithm

EDIT: ad hoc speed-ups are excluded. We have the result that propositional resolution requires exponential time. The resolution result uses the proof of the pigeonhole principle as an example of a ...
3
votes
1answer
585 views

Forward checking vs arc consistency on 3-SAT

If I were to let the variables be the propositions and, constraint be all clauses being satisfied, which technique would be more effective in solving 3-SAT? Forward checking or arc consistency? From ...
7
votes
1answer
636 views

CNF to DNF — conversion is NP Hard

How can i prove that the conversion from CNF to DNF is NP-Hard. I'm not asking for an answer, just some suggestions about how to go about proving it.