Skip to main content

Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

Filter by
Sorted by
Tagged with
33 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.'s user avatar
  • 162k
23 votes
3 answers
4k 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 ...
Dchris's user avatar
  • 415
16 votes
2 answers
4k 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 ...
Jason's user avatar
  • 171
25 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 ...
Mark Dominus's user avatar
  • 1,537
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,...
Bordaigorl's user avatar
16 votes
3 answers
10k 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) ...
nat's user avatar
  • 163
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 ...
Artem Kaznatcheev's user avatar
15 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.'s user avatar
  • 162k
11 votes
1 answer
16k 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 ...
Martin Seymour's user avatar
8 votes
2 answers
2k 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 ...
onigame's user avatar
  • 203
7 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 ...
Mat's user avatar
  • 502
6 votes
2 answers
723 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 ...
Dchris's user avatar
  • 415
3 votes
4 answers
2k 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 ...
wamitw's user avatar
  • 31
3 votes
1 answer
2k views

Show that the SAT Problem for CNF formulas with at most two occurences of each variable can be solved in polynomial time

Assuming, I have an arbitrary CNF Formula in which each variable has at most two occurences, how can I proof/show that this can be solved in polynomial time? My first thoughts so far: because each ...
Eden Hassard's user avatar
1 vote
1 answer
202 views

Boolean constraints for a connected component of a graph

Suppose I have an undirected graph $G=(V,E)$, and boolean variables $x_v$ (one for each vertex $v \in V$). These variables select a subset $S \subseteq V$ of vertices, namely the vertices $S=\{v \mid ...
D.W.'s user avatar
  • 162k
21 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.
jkjk's user avatar
  • 311
20 votes
2 answers
23k 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 (...
user11171's user avatar
  • 311
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 ...
Ari's user avatar
  • 1,631
14 votes
2 answers
32k 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 ...
pnp's user avatar
  • 763
13 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: ...
Albert Hendriks's user avatar
12 votes
3 answers
2k 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 ...
Albert Hendriks's user avatar
11 votes
1 answer
10k 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 ...
TCSGrad's user avatar
  • 592
8 votes
1 answer
715 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 ...
SapereAude's user avatar
7 votes
2 answers
2k 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-...
Juho's user avatar
  • 22.6k
6 votes
2 answers
266 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 ...
Simd's user avatar
  • 996
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.
Ilya Gazman's user avatar
3 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 ...
user1843790's user avatar
3 votes
1 answer
1k views

3-SAT and Systems of Nonlinear Modular Equations

How is the 3-SAT problem reduced to solving for a system of nonlinear modular equations? I have read https://stackoverflow.com/questions/4294270/how-to-prove-that-a-problem-is-np-complete in how to ...
Jeff's user avatar
  • 113
3 votes
2 answers
15k 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 ...
Ilya Gazman's user avatar
3 votes
1 answer
365 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 ...
rus9384's user avatar
  • 1,746
3 votes
2 answers
752 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 ...
John Threepwood's user avatar
3 votes
1 answer
1k 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 <...
gabbar0x's user avatar
  • 133
2 votes
1 answer
745 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\...
RandomAsker889's user avatar
2 votes
1 answer
4k 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 ...
valarion's user avatar
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 ...
user avatar
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)?
Silsaty's user avatar
  • 11
0 votes
2 answers
457 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.'s user avatar
  • 162k
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 ...
Adeiln's user avatar
  • 303
11 votes
1 answer
569 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 ...
Husrev's user avatar
  • 190
11 votes
1 answer
833 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 ...
sdcvvc's user avatar
  • 3,501
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 ...
Russell Easterly's user avatar
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 ...
tonik's user avatar
  • 195
8 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 \...
Mees de Vries's user avatar
7 votes
3 answers
436 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-...
elluser's user avatar
  • 175
6 votes
2 answers
433 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 ...
Adrian's user avatar
  • 63
6 votes
2 answers
6k views

Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
Tikhon Belousko's user avatar
6 votes
1 answer
388 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 ...
Xavier Labouze's user avatar
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 ...
Dor Cohen's user avatar
5 votes
1 answer
645 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 ...
user110726's user avatar
5 votes
0 answers
131 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 ...
vzn's user avatar
  • 11.1k