bio | website | |
---|---|---|
location | ||
age | ||
visits | member for | 4 years, 1 month |
seen | Oct 28 '14 at 15:25 | |
stats | profile views | 22 |
Oct 27 |
awarded | Scholar |
Oct 27 |
awarded | Supporter |
Oct 27 |
comment |
System of boolean equations, Satisfiability
@EmilJeÅ™ábek cool, thanks for the help. |
Oct 27 |
accepted | System of boolean equations, Satisfiability |
Oct 27 |
comment |
System of boolean equations, Satisfiability
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 |
comment |
System of boolean equations, Satisfiability
This is not correct. The inequality $(1-x_i) + (1-x_j) + (1-x_k) + y_C \geq 1$ is not equivalen to $x_i\vee x_j \vee x_k = 0$, check for $(0, 0, 1)$. This can be somehow feasible to impose the following $(1-x_i) + (1-x_j) + (1-x_k) + y_C \geq 3$, but this will make weighting of $y_C$ sensitive to number of nonzero $x$'s in equation. |
Oct 27 |
awarded | Student |
Oct 27 |
comment |
System of boolean equations, Satisfiability
This is not a weighted MaxSat. But I would be happy to be wrong, if you can show me how to reduce my problem to the equivalent MaxSat instance. |
Oct 27 |
revised |
System of boolean equations, Satisfiability
added 3 characters in body |
Oct 27 |
awarded | Editor |
Oct 27 |
comment |
System of boolean equations, Satisfiability
Please see the updated version |
Oct 27 |
revised |
System of boolean equations, Satisfiability
added 199 characters in body |
Oct 27 |
comment |
System of boolean equations, Satisfiability
$ik\in\{1,\dots,M\}$, where $M$ is number of variables. |
Oct 27 |
asked | System of boolean equations, Satisfiability |
Aug 11 |
awarded | Teacher |
Jun 5 |
answered | Is all non-convex optimization heuristic? |