Skip to main content
The 2024 Developer Survey results are live! See the results

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
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
28 votes
4 answers
6k 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 ...
Rishav's user avatar
  • 391
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
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
22 votes
1 answer
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,...
Vor's user avatar
  • 12.6k
21 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
  • 321
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
21 votes
1 answer
781 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 ...
Sami Liedes's user avatar
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
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
20 votes
1 answer
957 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 ...
Juho's user avatar
  • 22.7k
19 votes
3 answers
4k 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 ...
Ribz's user avatar
  • 693
17 votes
2 answers
5k 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 ...
Matt Groff's user avatar
17 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
  • 173
17 votes
1 answer
3k 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 ...
Vor's user avatar
  • 12.6k
16 votes
2 answers
4k 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 ...
codetaku's user avatar
  • 263
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
16 votes
2 answers
1k 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 ...
Jernej's user avatar
  • 2,460
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
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
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
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
12 votes
4 answers
2k views

Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
Omar Shehab's user avatar
12 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
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
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
11 votes
1 answer
917 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 ...
Artem Kaznatcheev's user avatar
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
10 votes
1 answer
538 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,\...
Alexander Klauer's user avatar
10 votes
2 answers
363 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 ...
Elliot Gorokhovsky'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
9 votes
1 answer
2k views

Why the need for TSP solvers when there are SAT solvers?

Concorde TSP is a solver for TSP. SAT solvers are solvers for boolean satisfiability. TSP and SAT are NP-complete. Hence, why spent the time to develop Concorde TSP when there is an abundance of SAT ...
Jessica Cage's user avatar
9 votes
2 answers
243 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'$ ...
Joni's user avatar
  • 511
9 votes
1 answer
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 ...
Jake's user avatar
  • 3,800
9 votes
1 answer
158 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 ...
R B's user avatar
  • 2,634
9 votes
1 answer
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 (...
Xavier Labouze's user avatar
9 votes
1 answer
239 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(...
D.W.'s user avatar
  • 162k
8 votes
4 answers
826 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 ...
user64231's user avatar
8 votes
2 answers
667 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$ ...
Miao Dongjing's user avatar
8 votes
2 answers
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 ...
Numerator's user avatar
  • 472
8 votes
2 answers
3k 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. ...
Infinity's user avatar
  • 183
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
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
8 votes
2 answers
234 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 ...
Grigor Aghanyan's user avatar
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
8 votes
1 answer
437 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 ...
Matt Groff's user avatar
8 votes
2 answers
425 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 ...
user avatar

1
2 3 4 5
14