Linked Questions

1
vote
0answers
62 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 ...
22
votes
2answers
2k views

Reduce the following problem to SAT

Here is the problem. Given $k, n, T_1, \ldots, T_m$, where each $T_i \subseteq \{1, \ldots, n\}$. Is there a subset $S \subseteq \{1, \ldots, n\}$ with size at most $k$ such that $S \cap T_i \neq \...
17
votes
3answers
627 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,...
8
votes
2answers
419 views

Software for testing graph homomorphism

I have graphs $G_k$ and $H_k$ with $|\mathcal{V}(G_k)|=|\mathcal{V}(H_k)|^{2k}=n^{2k}$ with $k\in\Bbb N$ that pass sanity checks such as no-homomorphism lemma. Are there free and easy to use tools to ...
5
votes
2answers
184 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 ...
3
votes
2answers
549 views

Mapping graph to another graph's sub-graph

How to solve the induced sub-graph isomorphism problem?
5
votes
1answer
2k views

Variation of Set Cover Problem: Finding a maximum-sized collection of disjoint set-covers

I have the following problem, which seems to be similar to Set Cover. We are given a set $U$ of elements (the universe, e.g., $U=\{1,2,3,4,5\}$). We're also given a set $S$ of subsets (e.g., $S=\{\{1\...
2
votes
1answer
1k 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{...
3
votes
1answer
438 views

Reduce Set problem to SAT

So the problem is, given some set $M = \{x_1,x_2,\ldots,x_n\}$ and a set of subsets $S = \{S_1, S_2, \ldots, S_m\}$ where $S_i \subseteq M$. We want to find some set $X \subseteq M$ such that $|X| \le ...
4
votes
1answer
189 views

Efficient algorithm for simple constraint satisfaction problem

There are $k$ Boolean variables $x_1, x_2, \dots, x_k$. $m$ arbitrary subsets of these variables such that sum of each set equals to $1$ (i.e., only one variable is $1$, the others are $0$). E.g., ...
4
votes
2answers
141 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,...
7
votes
2answers
105 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 ...
-2
votes
1answer
207 views

Alternative representations for the zebra puzzle?

All of the solutions for the zebra puzzle have a variable for each of the properties and a domain with the possible values. For instance A for Nationalities, B for pets, ... Ai with i = 1..5 and the ...
1
vote
2answers
105 views

Why is Max SAT in P if SAT in P?

It holds that if SAT could be solved in poly time, one can also find in poly time the assignment that satisfies most clauses of the original formula. Does anyone have any idea how to show this? Let's ...
3
votes
1answer
78 views

Can a propositional threshold connective be expressed by standard connectives?

We are given a finite set of propositional atoms $\{x_1, \dots, x_n\}$ and an integer $k$. Can we capture through a propositional formula $\varphi$ (built from the standard connectives $\neg, \wedge, \...

15 30 50 per page