bio | website | |
---|---|---|
location | ||
age | ||
visits | member for | 4 years, 2 months |
seen | Oct 28 '14 at 15:25 | |
stats | profile views | 23 |
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? |