24 questions linked to/from Reduce the following problem to SAT
1 vote
131 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 ...
7k 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 ...
1k 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,...
3k 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 ...
248 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 ...
2k 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{...
747 views

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

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

1 vote
441 views

### Reduction of K-Vertex-Cover to SAT: How to define the constraint?

Overall, one would naturally think that with n different nodes, and for x(1) for example representing node 1, it would be like: x(1)+x(2)+x(3)...+x(n) <= k This would mean that for every possible ...
145 views

### CNF form of variable assignment problem

There are n variables $x_1$, $x_2$,..., $x_n$ and each one of them takes values from 1 to k (k>= n) and all are distinct. How can I represent this in the CNF form? (I tried the trivial way of trying ...
1 vote
176 views

### Requiring at least one alldiff constraint to be satisfied converted to SAT

For generating certain hard puzzles, I am trying to model a problem (ultimately) in SAT. I don't know how to do that, so I am starting with CSP because it's more expressive. In CSP, there is a global ...
429 views

### Reducing Dominant Set Problem to SAT

I am trying to solve a problem and I am really struggling, I would appreciate any help. Given a graph $G$ and an integer $k$ , recognize whether $G$ contains dominating set $X$ with no more than $k$ ...
1 vote
245 views

### Counting the number of satisfied models - given mathematical constraints

Question There are plenty of algorithms for solving the #SAT problem, with one being the DPLL algorithm and is implemented for all kinds of programming languages. As far as I've seen, they all take a ...