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
30
votes
3answers
5k 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 ...
29
votes
3answers
893 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 ...
26
votes
4answers
5k views

Why is SAT so important in theoretical computer science?

In my Computability and Complexity class, we are focusing on P, NP, NP-complete, and NP-hard problems and the one thing that keeps coming up is the SAT problem, in the context of reduction from one ...
24
votes
3answers
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 ...
24
votes
2answers
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 ...
21
votes
1answer
2k views

Classification of intractable/tractable satisfiability problem variants

Recently I found in a paper [1] a special symmetric version of SAT called the 2/2/4-SAT. But there are many $\text{NP}$-complete variants out there, for example: MONOTONE NAE-3SAT, MONOTONE 1-IN-3-SAT,...
20
votes
1answer
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.
20
votes
1answer
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 ...
20
votes
1answer
901 views

Supporting data structures for SAT local search

WalkSAT and GSAT are well-known and simple local search algorithms for solving the Boolean satisfiability problem. The pseudocode for the GSAT algorithm is copied from the question Implementing the ...
20
votes
1answer
627 views

Why do all recent SAT solvers work on CNF instead of circuit SAT?

After the release of the AIGER library to handle and-inverter graphs sometime in 2006 (I think), some circuit SAT solvers were released in 2006-2008, and in a few SAT Races/Competitions there were AIG ...
19
votes
3answers
806 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,...
18
votes
3answers
3k views

Why there are no approximation algorithms for SAT and other decision problems?

I have an NP-complete decision problem. Given an instance of the problem, I would like to design an algorithm that outputs YES, if the problem is feasible, and, NO, otherwise. (Of course, if the ...
18
votes
2answers
18k 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 (...
16
votes
2answers
3k views

Poly-time reduction from ILP to SAT?

So, as is known, ILP's 0-1 decision problem is NP-complete. Showing it's in NP is easy, and the original reduction was from SAT; since then, many other NP-Complete problems have been shown to have ILP ...
16
votes
2answers
929 views

A dense NP complete language implies P=NP

We say that the language $J \subseteq \Sigma^{*}$ is dense if there exists a polynomial $p$ such that $$ |J^c \cap \Sigma^n| \leq p(n)$$ for all $n \in \mathbb{N}.$ In other words, for any given ...
16
votes
1answer
2k views

Planarity conditions for Planar 1-in-3 SAT

Planar 3SAT is NP-complete. A planar 3SAT instance is a 3SAT instance for which the graph built using the following rules is planar: add a vertex for every $x_i$ and $\bar{x_i}$ add a vertex for ...
15
votes
2answers
3k views

Is generalized XOR-SAT efficiently solvable?

I've seen how XOR-3-SAT is efficiently solvable (for instance, see the "XOR-satisfiability" section in the Wikipedia entry for Boolean satisfiability problem). I'm wondering a basic question: Is ...
14
votes
3answers
2k 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: ...
14
votes
1answer
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 ...
14
votes
2answers
7k 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) ...
13
votes
2answers
24k 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 ...
13
votes
2answers
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 ...
13
votes
2answers
1k 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}^{...
12
votes
2answers
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 ...
11
votes
1answer
12k 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 ...
11
votes
3answers
2k views

Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
11
votes
1answer
677 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 ...
11
votes
1answer
793 views

Can top SAT-solvers factor easy numbers?

Modern SAT-solvers are very good at solving many real-world examples of SAT instances. However, we know how to generate hard ones: for instance use a reduction from factoring to SAT and give the RSA ...
10
votes
2answers
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 ...
10
votes
1answer
7k 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 ...
10
votes
1answer
462 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 ...
9
votes
2answers
228 views

Find $\epsilon'$ s.t $L_\epsilon$ is $\mathsf{NP}$-hard for any $\epsilon<\epsilon'$

Let $L_\epsilon$ be the language of all $2$-CNF formulas $\varphi$, such that at least $(\frac{1}{2}+\epsilon)$ of $\varphi$'s clauses can be satisfied. I need to prove that there exists $\epsilon'$ ...
9
votes
1answer
360 views

Is weighted XOR-SAT NP-hard?

Given $n$ boolean variables $x_1,\ldots,x_n$ each of which is assigned a positive cost $c_1,\ldots,c_n\in\mathbb{Z}_{>0}$ and a boolean function $f$ on these variables given in the form $$f(x_1,\...
9
votes
1answer
1k views

Conflict Driven Clause Learning backtracking clarification

On the wikipedia page here it describes pretty well the CDCL algorithm (and it seems the pictures were taken from slides created by Sharad Malik at Princeton). However when describing how to backtrack ...
9
votes
2answers
343 views

Explaining SAT to high school science teachers

I am a high school sophomore who is interested in computer science. I developed a cool algorithm for #SAT, and I'm implementing and doing a science fair project on it. My adviser, who is the best ...
9
votes
1answer
147 views

What is the name of the problem? (partitioning graph into three covers)

I was wondering if this problem has a name: Given a simple graph whose edges are colored red, blue and green, $G=(V,B\cup R\cup G)$, is there a vertex-coloring $c:V\to \{B,R,G\}$ such that every edge ...
9
votes
1answer
1k views

Complexity of (SAT to 3-SAT) Problem?

It is well known that any CNF formula can be transform in polynomial time into a 3-CNF formula by using new variables (see here). If using new variables is not allowed, it is not always possible (...
9
votes
1answer
212 views

Verify correctness of quantifier elimination, using SAT

Let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be $n$-vectors of boolean variables. I have a boolean predicate $Q(x,y)$ on $x,y$. I give my friend Priscilla $Q(x,y)$. In response, she gives me $P(...
8
votes
4answers
701 views

Deterministic SAT solver

I have the following question. Is the SAT solvers are deterministic? I mean, for example, about miniSAT and DPLL algorithm. Are they completely deterministic? If these algorithms will return unSAT ...
8
votes
2answers
623 views

What is a dichotomy? Whether 2-SAT itself is a dichotomy of SAT?

Recently, I am reading papers about dichotomy. I do not understant what condition can be called as a dichotomy? What is the meaning of "a question is either in P or in NP-complete"? (assume P $\neq$ ...
8
votes
2answers
2k views

Is "Reachable Object" really an NP-complete problem?

I was reading this paper where the authors explain Theorem 1, which states "Reachable Object" (as defined in the paper) is NP-complete. However, they prove the reduction only in one direction, i.e. ...
8
votes
1answer
540 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 ...
8
votes
2answers
204 views

Assignment to make formula unsatisfiable

Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?". One way of ...
8
votes
1answer
288 views

How much can we reduce the number of clauses by converting from $k$-SAT to $(k+m)$-SAT?

If we suppose that we start with an instance of $k$-SAT, and try converting the problem to an instance of $(k+m)$-SAT, where there are $(k+m)$ literals per clause, can we guarantee a reduction in the ...
8
votes
2answers
405 views

A tentative satisfiability algorithm

General satisfiability (with a few exceptions such as Horn Clauses) is not believed to have an algorithmic solution. However, the following algorithm appears to be a solution for general ...
7
votes
3answers
410 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-...
7
votes
2answers
1k views

Is SAT in P if there are exponentially many clauses in the number of variables?

I define a long CNF to contain at least $2^\frac{n}{2}$ clauses, where $n$ is the number of its variables. Let $\text{Long-SAT}=\{\phi: \phi$ is a satisfiable long CNF formula$\}$. I'd like to know ...
7
votes
1answer
15k views

how do you prove that SAT is NP-complete?

As it is, how do you prove that SAT is NP-complete? I know what it means by NP-complete, so I do not need an explanation on that. What I want to know is how do you know that one problem, such as SAT,...
7
votes
2answers
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-...
7
votes
2answers
776 views

Lower Bounds for Size of Independent Set in a Graph?

I recently learnt that for any instance of a k-SAT problem with $m$ clauses and $n$ literals , we have an assignment of literals such that at least $m(1 - 2^{-k})$ clauses are satisfied. I was ...

1
2 3 4 5
12