New answers tagged


Arc-Consistency algorithm only works on binary constraints.You have to use binary encoding and hidden variable encoding method.


Assuming you work in CNF, construct "at least $k+1$-out-of-$n$" and add "or $p$" to each disjunction. Do the same for "at most $k-1$-out-of-$n$" and add "or $q$" to each disjunction. Then add one extra term to your main conjunction, $\neg p \vee \neg q$.


Given a graph $G = (V,E)$, here is a SAT instance which is satisfiable iff the graph is not connected. Pick an arbitrary vertex $v_0 \in V$, and add the following clauses, over the variables $x_v$ for $v \in V$: $x_{v_0}$. For every $(u,v) \in E$, $\lnot x_u \lor x_v$ and $\lnot x_v \lor x_u$. $\bigvee_{v \neq v_0} \lnot x_v$. Here is a SAT instance which ...


It is some sort of necro-answer to already answered and accepted question, but I want to note, that there is really easier way. Consider you have one of inequalities like this: $5*x_1 + 2*x_2 + 3*x_3 \leq 6$ You may easily test all no-vectors for this inequality: $(1, 1, 1)$, $(1, 1, 0)$ and $(1, 0, 1)$ others are ok. First vector $(1, 1, 1)$ means that ...

Top 50 recent answers are included