33 reputation
5
bio website
location
age
visits member for 3 years, 5 months
seen Oct 28 at 15:25

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?