Questions regarding solver programs for the boolean satisfiability problem.

learn more… | top users | synonyms

8
votes
3answers
78 views

Recipe book for SAT encodings?

SAT solvers are getting more and more efficient in solving large instances and are being used as back-ends in various contexts. Every time one wants to use them to solve a problem in a specific ...
4
votes
3answers
122 views

Detection of redundant boolean constraints

I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin ...
3
votes
0answers
36 views

Introduction to bounded model checking that describes model generation

Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
2
votes
1answer
80 views

Solving SAT using tableau calculus

I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the ...
1
vote
1answer
83 views

Fast Consequence FInders

I have been struggling in the search for a modern fast "consequence finder". That is, an implementation based on state-of-the-art theory; things of the ilk of Z3, Prover9, OTTER, etc. To describe ...
10
votes
3answers
154 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
129 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
68 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 ...
10
votes
1answer
436 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 ...
6
votes
1answer
179 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, ...
2
votes
2answers
639 views

Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
6
votes
2answers
128 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
188 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
222 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
152 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
227 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
226 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
750 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 ...
8
votes
1answer
745 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.