Timeline for "State of the art" algorithms deciding entailment of propositional formulas?
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 16, 2020 at 11:20 | comment | added | Higemaru | Yes, I am aware. So in a sense the question is more "Negation+VeryEasy versus SAT solver", as one could use Tseytin transformation + Negation to arrive at a DNF. I will check whether using a SAT solver will work for me. | |
| Jun 16, 2020 at 11:18 | comment | added | Yuval Filmus | The negation of a DNF is a CNF (and vice versa). This could explain the confusion between CNFs and DNFs. | |
| Jun 16, 2020 at 11:17 | comment | added | Higemaru | Thanks, that's a good argument for Tseytin transformations. | |
| Jun 16, 2020 at 11:17 | comment | added | Yuval Filmus | Tseytin transformation runs in linear time. | |
| Jun 16, 2020 at 11:16 | comment | added | Higemaru | Yes, but if solving a DNF is, as you say, very easy, why "go to the trouble" of using a SAT solver, when it doesn't even get rid of the need to transform to normal form first? (Is it because a Tseytin transformation is much more efficient than transforming to DNF - or rather, is the combination of Tseytin+SAT that much faster than DNF+VeryEasy?) | |
| Jun 16, 2020 at 11:12 | comment | added | Yuval Filmus | Satisfiability is a special case of your problem. | |
| Jun 16, 2020 at 11:12 | history | edited | Yuval Filmus | CC BY-SA 4.0 |
added 118 characters in body
|
| Jun 16, 2020 at 11:11 | comment | added | Higemaru | Yes, does that mean your answer includes "look at algorithms for SAT solvers" in some way? Solving my problem using DNFs seems pretty straight forward, but I thought one might be able to solve it without transforming into a normal form first. | |
| Jun 16, 2020 at 11:06 | comment | added | Yuval Filmus | The point of this answer is that your question is a special case of SAT. We already know how to solve SAT in practice – that's the area of SAT solving. | |
| Jun 16, 2020 at 11:05 | comment | added | Yuval Filmus | SAT solvers solve the satisfiability problem, which doesn't make much sense for DNFs (it's very easy). | |
| Jun 16, 2020 at 11:04 | comment | added | Higemaru | What is the advantage of transforming to CNF (which Wikipedia tells me is the result of a Tseytin transformation) and then solving as opposed to transforming to DNF and then solving? I'm more interested in understanding the algorithms, less so in quickly implementing the best practical way to solve a given problem. | |
| Jun 16, 2020 at 10:27 | history | answered | Yuval Filmus | CC BY-SA 4.0 |