Questions regarding solver programs for the boolean satisfiability problem.
-4
votes
0answers
19 views
how to run minisat+ sat solver [closed]
I downloaded the minisat+zip file
I extracted the zip.According to install file i run
make rx
but i have the following result:
...
3
votes
1answer
45 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
91 views
Understanding DPLL algorithm
I'm trying to understand DPLL algorithm for solving SAT problem. And here it is:
...
4
votes
1answer
53 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 ...
8
votes
1answer
100 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 ...
5
votes
2answers
152 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 ...
3
votes
1answer
84 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 ...
7
votes
1answer
120 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 ...
2
votes
1answer
110 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 ...
1
vote
1answer
245 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 ...
6
votes
1answer
233 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.
