Linked Questions
25 questions linked to/from Reduce hitting set to SAT, and cardinality constraints
1
vote
0
answers
164
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 ...
- 1,048
34
votes
3
answers
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 ...
D.W.♦
- 166k
20
votes
3
answers
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,...
- 425
9
votes
2
answers
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 ...
- 203
6
votes
2
answers
274
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 ...
- 1,036
3
votes
1
answer
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{...
- 253
3
votes
2
answers
766
views
Mapping graph to another graph's sub-graph
How to solve the induced sub-graph isomorphism problem?
- 83
4
votes
2
answers
510
views
Is it feasible to solve this subset cover problem with SAT solver?
The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied:
if $S \subseteq \mathcal{S}$ then $|S|=6$;
for any $A \subseteq \{1,...
- 568
5
votes
2
answers
1k
views
Global optimization of state assignments in a directed graph with a tree-based distance cost
I am exploring a general optimization framework to solve problems characterized by the following structure. Any literature references, search terms, or algorithmic strategies would be greatly ...
- 151
4
votes
1
answer
255
views
Maximum minimal set coverage
Suppose we are given a universal set $U$ and a family of subsets of $U$, denoted by $F$ (elements in $F$ are subsets of $U$). We assume that all elements in $F$ can cover $U$, i.e., $U\subseteq \...
- 215
1
vote
1
answer
594
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 ...
2
votes
0
answers
653
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$ ...
- 53
7
votes
2
answers
147
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 ...
- 85
1
vote
1
answer
182
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 ...
- 487
1
vote
3
answers
279
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 ...
- 129