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
511
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
654
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
2
votes
1
answer
383
views
Fast $k$-clique checking algorithm?
I have a problem where part of it requires answering the question: does graph $G=(V,E)$ contain a clique of size at least $k$?
Obviously, answering this question is a NP-Complete problem. I am no ...
- 121
3
votes
1
answer
138
views
Finding a minimal set of package versions in a dependency graph with constraints
Suppose you have a dependency graph of "packages" registered in the ecosystem of a given programming language. We can model each package as a tuple ...
- 133
0
votes
0
answers
177
views
Effecient encoding of sum equality in cnf+xor
I am wondering as to how to efficiently encode the following subcircuit for a binary satisfiability solver (cnf, and optionally xor clauses, if this helps):
...
- 1,493
0
votes
1
answer
106
views
How to converts Pseudo boolean constraints to cnf format?
How to convert Pseudo boolean constraints to CNF format
for example L1 + … + Ln ≥ 1 is converted to L1 ∨ … ∨ Ln
but how about:
L1 + … + Ln ≥ k
L1 + … + Ln < k
or
L1 + L2 = k
or
2 L1 + 2 L2L3 + L4 ...
- 25
2
votes
1
answer
71
views
Algorithm for finding subsets subject to union condition
I'm a mathematician and the following came up in my research:
Fix some positive integers $a_0,...,a_n$ and $N$.
Consider subsets $A_i \subset \{0,...,N\}$ where $|A_i|=a_i$, subject
to some fixed ...
- 133
1
vote
1
answer
81
views
packing with time-variant weights
This appears to be a knapsack / bin-packing problem, but I seem to have got stuck and could appreciate contributions.
Scenario 1: Tough (for me!)
There is a one day conference with a set of (4 or ...
- 33
1
vote
1
answer
93
views
Encoding SAT EqualsK Constraint with Two Possible Values
I am wondering about a way to CNF encode an EqualsK constraint with two possible values. In other words, I want to solve for the equation:
$$
(\sum_{i=1}^n x_i = A) \lor (\sum_{i=1}^n x_i = B)
$$
...
- 13
3
votes
1
answer
66
views
Equally coloring the edges of square tiles that form a grid
I need to generate a set of square tiles that are colored and are grid-able. Each square tile must have a unique set of 4 colors and each exterior edge of each tile is colored with a different color. ...
- 51
1
vote
1
answer
57
views
Having a 2D matrix with three typed elements, how to efficiently cover one of the types and NOT cover the other one?
I have a matrix with three possible elements: A, B and C. The size of the matrix could be a maximum of 15x16.
$$
\begin{bmatrix}
A & A & C & A\\
A & C & B & C\\
A & C & ...
- 111
1
vote
1
answer
57
views
Modified set cover to identify "orthogonal" partitions
Setup
I have a non-empty set of elements $U$ that are arranged spatially.
I would like to partition $U$ into $N$ non-empty, disjoint subsets, $A_i$, having up to $M$ elements each. Each subset is only ...
- 11