Valera
Reputation
Top tag
Next privilege 50 Rep.
Comment everywhere
 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?