13 questions linked to/from Reduce the following problem to SAT
57 views

### Is there a simple way to construct a Boolean formula that is true if and only if at most $k$ of the input variables are true? [duplicate]

I could of course construct a truth table for the function $$f(x) = \left(\sum_i x_i\right) \leq k$$ Where $x$ is an assignment and I'm slightly abusing notation to count Booleans. And then I could ...
4k views

### Encoding 1-out-of-n constraint for SAT solvers

I'm using a SAT solver to encode a problem, and as part of the SAT instance, I have boolean variables $x_1,x_2,\dots,x_n$ where it is intended that exactly one of these should be true and the rest ...
576 views

### Recipe book for SAT encodings?

SAT solvers are getting more and more efficient in solving large instances and are being used as back-ends in various contexts. Every time one wants to use them to solve a problem in a specific domain,...
2k views

### Maximize distance between k nodes in a graph

I have an undirected unweighted graph $G$ and I want to select $k$ nodes from $G$ such that they are pairwise as far as possible from each other, in terms of geodesic distance. In other words they ...
2k views

### When problem A reduces to problem B, which problem is more complex?

When discussing complexity classes, when we say that problem $A$ reduces to problem $B$, are we saying that problem $A$ is at least as complex as problem $B$, or the other way around?
175 views

### Convert $\sum x_i = y$ to 3-sat

I have a simple looking question. What is the most efficient conversion of $\sum_{i=1}^n x_i = y$ to 3-sat? Here $x_i$ is either $1$ or $0$ and $y$ is some positive integer. Can you do better than ...
497 views

### Mapping graph to another graph's sub-graph

How to solve the induced sub-graph isomorphism problem?
982 views

### Reducing k Vertex Cover to SAT (last clause problem)

I am working on a transformation from k Vertex Cover to SAT and I have some issues regarding the last clause in the boolean formula. Here is my approach: \forall \text{ nodes } n_i \in V, \text{...