Timeline for System of boolean equations, Satisfiability
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 27, 2014 at 17:42 | comment | added | Emil Jeřábek | I’m sorry, but I do not have practical experience with SAT solvers, so I can’t give recommendations. My guess would be that a (MAX)SAT solver should be able to exploit the fact that the variable $y_i$ is localized to only four clauses (one of which is a unit clause), so the translation shouldn’t introduce any performance penalty, but there is really no way to know how efficient it is in practice other than trying it out. | |
| Oct 27, 2014 at 16:39 | vote | accept | Valera | ||
| Oct 27, 2014 at 16:37 | comment | added | Valera | Thanks, this formulation does look equivalent. Any idea, if the MaxSat solvers would behave nicely with this type of clauses? And one more side question, since you look like an expert in the field: can you recommend open-source sat-solver, that can treat millions of variables and tens of millions of clauses? | |
| Oct 27, 2014 at 16:27 | history | answered | Emil Jeřábek | CC BY-SA 3.0 |