Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
76
questions
32
votes
3
answers
6k
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.♦
- 152k
23
votes
3
answers
3k
views
Converting (math) problems to SAT instances
What I want to do is turn a math problem I have into a boolean satisfiability problem (SAT) and then solve it using a SAT Solver. I wonder if someone knows a manual, guide or anything that will help ...
- 415
14
votes
2
answers
3k
views
Is finding a solution of a satisfiability problem harder than deciding satisfiability?
Is the problem of determining whether or not a given Boolean expression is satisfiable computationally distinct from actually finding a solution to the expression?
In other words, is there another ...
- 151
24
votes
3
answers
2k
views
Is there a sometimes-efficient algorithm to solve #SAT?
Let $B$ be a boolean formula consisting of the usual AND, OR, and NOT operators and some variables. I would like to count the number of satisfying assignments for $B$. That is, I want to find the ...
- 1,525
19
votes
3
answers
964
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,...
- 415
14
votes
2
answers
8k
views
Prove NP-completeness of deciding satisfiability of monotone boolean formula
I am trying to solve this problem and I am really struggling.
A monotone boolean formula is a formula in propositional logic where all the literals are positive. For example,
$\qquad (x_1 \lor x_2) ...
- 143
30
votes
3
answers
1k
views
Measuring the difficulty of SAT instances
Given an instance of SAT, I would like to be able to estimate how difficult it will be to solve the instance.
One way is to run existing solvers, but that kind of defeats the purpose of estimating ...
- 4,792
14
votes
2
answers
2k
views
MIN-2-XOR-SAT and MAX-2-XOR-SAT: are they NP-hard?
What is the complexity of $\text{MIN-2-XOR-SAT}$ and $\text{MAX-2-XOR-SAT}$? Are they in P? Are they NP-hard?
To formalize this more precisely, let
$$\Phi\left(\mathbf x\right)={\huge\wedge}_{i}^{...
D.W.♦
- 152k
11
votes
1
answer
15k
views
DNF to CNF conversion: Easy or Hard
In relation to the thread Proving that the conversion from CNF to DNF is NP-Hard (and a related Math thread):
How about the other direction, from DNF to CNF? Is it easy or hard?
On Page 2 of this ...
- 345
6
votes
2
answers
654
views
Modeling the problem of finding all stable sets of an argumentation framework as SAT
As a continuation of my previous question i will try to explain my problem and how i am trying to convert my algorithm to a problem that can be expressed in a CNF form.
Problem: Find all stable sets ...
- 415
3
votes
3
answers
1k
views
Why isn't SAT in coNP?
I understand why NP=coNP if SAT is in coNP (How do I prove that SAT in coNP implies NP=coNP?).
But I'm missing why the following machine doesn't turing recognize the complementary of SAT:
Given a ...
- 31
20
votes
1
answer
4k
views
Proving that the conversion from CNF to DNF is NP-Hard
How can I prove that the conversion from CNF to DNF is NP-Hard?
I'm not asking for an answer, just some suggestions about how to go about proving it.
- 301
19
votes
2
answers
21k
views
What's an example of an unsatisfiable 3-CNF formula?
I'm trying to wrap my head around an NP-completeness proof which seem to revolve around SAT/3CNF-SAT.
Maybe it's the late hour but I'm afraid I can't think of a 3CNF formula that cannot be satisfied (...
- 301
14
votes
1
answer
2k
views
Why do Shaefer's and Mahaney's Theorems not imply P = NP?
I'm sure someone has thought about this before or immediately dismissed it, but why does Schaefer's dichotomy theory along with Mahaney's theorem on sparse sets not imply P = NP ?
Here's my ...
- 1,601
14
votes
3
answers
3k
views
Is 2-SAT with XOR-relations NP-complete?
I'm wondering if there is a polynomial algorithm for "2-SAT with XOR-relations". Both 2-SAT and XOR-SAT are in P, but is its combination?
Example Input:
2-SAT part: ...
- 2,450
14
votes
2
answers
29k
views
Proving DOUBLE-SAT is NP-complete
The well known SAT problem is defined here for reference sake.
The DOUBLE-SAT problem is defined as
$\qquad \mathsf{DOUBLE\text{-}SAT} = \{\langle\phi\rangle \mid \phi \text{ has at least two ...
- 753
12
votes
2
answers
1k
views
Why does Schaefer's theorem not prove that P=NP?
This is probably a stupid question, but I just don't understand. In another question they came up with Schaefer's dichotomy theorem. To me it looks like it proves that every CSP problem is either in P ...
- 2,450
11
votes
1
answer
9k
views
How to prove that a constrained version of 3SAT in which no literal can occur more than once, is solvable in polynomial time?
I'm trying to work out an assignment (taken from the book Algorithms - by S. Dasgupta, C.H. Papadimitriou, and U.V. Vazirani, Chap 8, problem 8.6a), and I'm paraphrasing what it states:
Given that ...
- 592
8
votes
2
answers
1k
views
SAT algorithm for determining if a graph is disjoint
What are some good algorithms to have a SAT (CNF) solver determine if a given graph is fully-connected or disjoint?
The best one I can think of is this:
Number the nodes 1..N, where N is the number ...
- 193
8
votes
1
answer
671
views
Is a "local" version of 3-SAT NP-hard?
Below is my simplification of part of a larger research project on spatial Bayesian networks:
Say a variable is "$k$-local" in a string $C \in 3\text{-CNF}$ if there are fewer than $k$ clauses ...
- 319
7
votes
2
answers
1k
views
3-SAT where variables occur equally many times as a positive literal and as a negative literal
Let $\phi$ be a 3-CNF formula over variables $x_1,x_2,\ldots,x_n$. Every variable $x_i$, $i \in [n]$, occurs equally many times as a positive literal and as a negative literal in $\phi$.
Is it NP-...
- 22.4k
6
votes
2
answers
238
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 ...
- 860
4
votes
2
answers
3k
views
Formulas for which any equivalent CNF formula has exponential length
I read a claim that
there are formulas for which any equivalent CNF has exponential length.
Can you show me an example for such a boolean formula? I have been trying to build it myself and failed.
- 899
3
votes
1
answer
348
views
Satisfiabililty sufficient condition?
The conjecture itself:
k-SAT formula is satisfiable if no pair of unit assignment $l$ and $\overline l$ imply the formula to contain unsatisfiable (k-1)-SAT.
Example (XOR-SAT has no edges and cycles ...
- 1,393
3
votes
2
answers
659
views
Getting a variable assignment of a Tseitin transformed formula
Let $\phi$ be a Boolean formula and $\mathrm{Tseitin}(\phi)$ the corresponding Tseitin transformed equisatifiable formula.
It is well-known that one can get a variable assignment for $\phi$ by ...
- 249
3
votes
1
answer
851
views
How exactly does a Max 2 Sat reduce to a 3 Sat?
I've been reading this article which tries and explains how the max 2 sat problem is essentially a 3-sat problem and is NP-hard. However, if you see the article, I'm not able to understand why, after <...
- 133
3
votes
2
answers
13k
views
3-sat to 2-sat reduction
It is known that 3-SAT belong to - NP-Complete complexity problems, while 2-SAT belong to P as there is known polynomial solution to it.
So you can state that there is no such reduction from 3-SAT to ...
- 899
2
votes
1
answer
236
views
Reduction from SAT to SAT with exactly k true variables
Let $L$ be defined as follows:
$\small L = \{(\phi, k) \mid \phi \in SAT \mbox{ and there is a satisfying assignment for $\phi$ having exactly $k$ true variables} \}$
I am struggling to show that $SAT\...
2
votes
2
answers
2k
views
Best improvements to do to the DPLL SAT algorithm
As part of a college class, I'm asked to improve the performance of a basic DPLL sat solver. I'm already provided a basic, slow working version (essentially the DPLL algorithm; furthermore, to select ...
- 23
1
vote
1
answer
3k
views
Half-SAT intractability proof
I've been struggling lately with a problem that was in my last complex algorithms exam, and I can't find a solution.
The problem is as follows:
Half-SAT is a problem where C is a CNF boolean formula ...
- 13
1
vote
1
answer
2k
views
How do I prove that SAT in coNP implies NP=coNP?
Is it true that if SAT is in coNP then its also coNP-complete (because it is NP-complete)?
- 11
1
vote
2
answers
1k
views
P=NP, isn't it?
Cook and Levin showed in 1971 how deterministically in polynomial time from every non deterministic Turing machine M, that halts in polynomial number of moves/steps, and string w to create the boolean ...
user82913
0
votes
2
answers
387
views
Is 2QBF in P^NP?
2QBF is the following problem: given a CNF formula $\psi$ on $2n$ variables, determine the truth value of
$$\forall x \in \{0,1\}^n . \exists y \in \{0,1\}^n . \psi(x,y).$$
Question: Is 2QBF in $P^{...
D.W.♦
- 152k
20
votes
1
answer
3k
views
Implementing the GSAT algorithm - How to select which literal to flip?
The GSAT algorithm is, for the most part, straight forward: You get a formula in conjunctive normal form and flip the literals of the clauses until you find a solution that satisfies the formula or ...
- 303
11
votes
1
answer
766
views
Complexity of deciding if a formula has exactly 1 satisfying assignment
The decision problem
Given a Boolean formula $\phi$, does $\phi$ have exactly one satisfying assignment?
can be seen to be in $\Delta_2$, $\mathsf{UP}$-hard and $\mathsf{coNP}$-hard. Is anything ...
- 3,481
11
votes
1
answer
522
views
If one shows that UNIQUE k-SAT is in P, does it imply P=NP?
Valiant & Vazirani proved SAT is reducible to UNIQUE SAT under randomized probabilistic reductions in polynomial time. Calabro et al. showed that UNIQUE k-SAT is as hard as k-SAT. Now the ...
- 190
10
votes
2
answers
3k
views
What is wrong with this simple proof of P=NP?
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiabilty problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
- 341
9
votes
2
answers
5k
views
Is SAT an existential question?
Some sources state that an algorithm that solves the SAT problem not only needs to decide whether a given existentially-quantified formula is satisfiable or not, but, additionally, in the case where ...
- 195
7
votes
1
answer
2k
views
Is #HORNSAT polynomial?
A Horn clause is a disjunctive clause of literals containing at most one unnegated literal. Examples are
$$
\neg p \lor \neg r \lor \neg q,\\ \neg s \lor q,\\ \neg s \lor \neg q\lor r,\\ s,\\ \neg r \...
- 431
7
votes
3
answers
427
views
What is wrong with this seeming contradiction with a paper about AND-compression of SAT?
Got a simple construction seemingly contradicting a paper assuming plausible conjecture.
Since it is unlikely the conjecture to be false, what is wrong with the argument?
From a paper
An AND-...
- 175
6
votes
2
answers
3k
views
3-SAT problem with number of clauses equal to number of variables
Consider the 3-SAT problem where the formula is in conjunctive normal form and we restrict the Boolean formulas such that the number of clauses in the formula is equal to the number of variables. Is ...
- 472
6
votes
2
answers
5k
views
Understanding DPLL algorithm
I'm trying to understand DPLL algorithm for solving SAT problem. And here it is:
...
- 163
6
votes
2
answers
346
views
An Exact Method for Solving Small Instances of XORSAT
I have a couple of small instances for XORSAT for which I am to design and implement an exact method. However, there are a few catches. It is guaranteed that there always exists and answer but I need ...
- 63
6
votes
1
answer
362
views
Complexity of deciding the satisfiability of a quasi-monotone CNF formula
A quasi-monotone CNF formula is a formula where each variable appears at most once as a positive literal (and any number of times as a negative literal).
What is the complexity of deciding its ...
- 511
5
votes
1
answer
455
views
Is MIN or MAX-True-2-XOR-SAT NP-hard?
Is there a proof or reference that $\left\{\text{MAX},\text{MIN}\right\}\text{-True-2-XOR-SAT}$ is $NP$-hard, or that it (the decision version) is in $P$?
Let:
$$\Phi\left(\mathbf x\right)={\huge\...
- 6,171
5
votes
0
answers
129
views
research on OR and AND compression in SAT formulas [closed]
this is a new/advanced paper on OR and AND compression of SAT formulas, a newer area of research that seems not covered in any textbooks so far.
A simple proof that AND-compression of NP-complete ...
- 11k
5
votes
1
answer
304
views
Is there an instance of 3-SAT in less than 100 variables that no one has been able to solve?
In number theory, progress is sometimes guided by people stating a specific Diophantine equation that they don't know how to solve. Is there anything similar in the field of Boolean satisfiability?
...
- 51
5
votes
3
answers
4k
views
Find hamilton cycle in a directed graph reduced to sat problem
I need to find a Hamiltonian cycle in a directed graph using propositional logic, and to solve it by sat solver. So after I couldn't find a working solution, I found a paper that describes how to ...
- 53
4
votes
1
answer
535
views
Are SAT problems with at most one false clause NP-complete?
Is the problem of deciding whether a SAT instance, where at most one clause is false (that is, any given variable assignment will either lead to all clauses being true, or all but one), is satisfiable ...
- 43
4
votes
1
answer
710
views
transformation of constraint satisfaction to SAT
How can any Constraint satisfaction problem be converted to an instance of Satisfiability? I have a CSP and i know its NP hard to solve it, but i would like to convert to an instance of k-SAT, but im ...
- 41