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

learn more… | top users | synonyms

-2
votes
0answers
18 views

Randon 3SAT - when is a clause ture? [on hold]

Hi i have been give some random 3Sat data and ask to WalkSAT to solve for uni. Only thing is I don't really know where to start. I have some clauses say -61 -63 26 -40 92 57 -74 -84 54 How do I ...
1
vote
1answer
49 views

3-SAT to Max-2-SAT Reduction

I'm trying to find reduction from 3-SAT to Max-2-SAT, so far no luck. Let me first describe it. 3-SAT: Given a CNF formula $\varphi$, where every clause in $\varphi$ has exactly 3 literals in ...
1
vote
1answer
51 views

Application of Combinatorics, Logic and computability theory in physical science: Tiling of Wang Tile with proportionality [closed]

The original problem of Domino Tiling and Wang Tile has great theoretical interest on computability theory... However, the great emerging problem on application of Wang Tile in material science and ...
-1
votes
1answer
25 views

3SAT to CNF-SAT reduction

I am trying to prove that 3SAT is polynome time reducable to CNF-SAT, but I don't know how to do this. A formula F is in 3SAT iff f(F) is in KNFSAT, but since 3SAT is a part of KNFSAT, every formula ...
2
votes
2answers
66 views

Why is SAT in NP?

I know that CNF SAT is in NP (and also NP-complete), because SAT is in NP and NP-complete. But what I don't understand is why? Is there anyone that can explain this?
2
votes
1answer
34 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 ...
1
vote
2answers
43 views

How to represent a 0-valid boolean formula?

I read in these two papers http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/max-sat/p216-schaefer.pdf and http://people.csail.mit.edu/madhu/papers/noneed/fullbook.ps that if we ...
2
votes
2answers
89 views

Hardness of mixed 3-SAT and 2-SAT formula

It is well known that 3-SAT is $\sf NP$-complete , but 2-SAT is in $\sf P$. Let there be a formula with $n-1$ clauses with 2 literals each and only 1 clause with 3 literals. We can solve this ...
2
votes
1answer
87 views

Is this NP-completeness proof correct?

I want to prove that a problem $P_1$ is NP-complete. Let say that I want to do a reduction from SAT problem. If the instance of problem $P_1$ depends on $M$ and $N$, can I specify the sturcture of ...
2
votes
1answer
73 views

GSAT incompleteness example

The GSAT (Greedy Satisfiability) algorithm can be used to find a solution to a search problem encoded in CNF. I'm aware that since GSAT is greedy, it is incomplete (which means there would be cases ...
3
votes
1answer
180 views

Issue understanding the reduction of SAT to 3-SAT in poly time

Reading this http://classes.soe.ucsc.edu/cmps102/Spring10/lect/17/SAT-3SAT-and-other-red.pdf, I came to know that reducing a clause $C_i$ from a $SAT$ instance containing more than 3 literals to a ...
5
votes
2answers
72 views

Number of instances of SAT (boolean satisfiability) problems of size N?

I assume the size of an instance of the SAT problem is measured by its number of (Boolean) variables. What is total number of instances of SAT problems of size N? I guess that amounts to counting ...
1
vote
2answers
61 views

Proving 2P2N SAT is NP-Complete

I hope I named this CNF Boolean sentence the correct way. The way I see it, a 2P2N is where each literal appears twice (or at most twice, but we can say twice without loss of generality). I am ...
1
vote
1answer
103 views

Does NP-Complete imply non-satisfiability?

I've seen a lot of text concerning the first NP-Complete problem, Boolean Satisfiability. I guess I'm confused concerning the language. It sounds to me as though the problem could be difficult to ...
1
vote
2answers
68 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 ...
4
votes
1answer
109 views

Lower bound on running time for solving 3-SAT if P = NP

Is there a lower bound on the running time for solving 3-SAT if P = NP. For instance, is it known that 3-SAT can't be solved in linear time? What about quadratic?
2
votes
1answer
91 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 ...
1
vote
1answer
19 views

Complexity of calculating a single model versus all models of a propositional formula with a SAT solver

I have little background with SAT sovers and theoretical computer science. How can I describe the complexity of calculating all models of a propositional formula versus just the usual SAT problem of ...
4
votes
2answers
122 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$ ...
3
votes
1answer
61 views

CNF SAT conversions

I am interested in reductions from 3-CNF boolean expressions to similar restricted forms. For example, I am interested in knowing how to reduce a 3-CNF formula to another 3-CNF formula where each ...
-4
votes
2answers
74 views

Reduction validity

I am trying to reduce 3-sat to 2-sat. I found an assignment that make 3-ast satisfy, so it is satisfy, and same assignment is satisfy my 2-sat, so my reduction is valid. How ever there is more than ...
-3
votes
3answers
308 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 ...
0
votes
1answer
37 views

Complexity of Double-Horn-SAT?

On one hand, Horn-SAT is known to be tractable in linear time - where Horn-SAT is the problem of deciding whether a given set of propositional Horn clauses (with at most one positive literal) is ...
-2
votes
1answer
62 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 ...
4
votes
2answers
124 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 ...
-1
votes
1answer
65 views

Boolean algebra fast CNF convertion

I have been solving a "hard" boolean formula today and found a nice shortcut. So just wanted to share. When given the next formula how would you convert it to CNF? $\lnot(x \oplus y \oplus ...
0
votes
3answers
87 views

Resolution and what it means to derive the empty set

When using resolution, if the empty set {Ø} is derived from a formula like {¬x,¬y} {x,y}, does that mean the formula is unsatisfiable? If this is the case, why is ...
4
votes
1answer
137 views

Is the $k$P$k$N-3SAT problem NP-complete?

Consider the following 3-SAT variant defined over the variables $x_1,\ldots,x_n$. In the $k$P$k$N-3SAT problem each variable $x_j$, $j \in [n]$, occurs exactly $k$ times as a positive literal in ...
-1
votes
1answer
52 views

Why is SAT not in P? [duplicate]

I'm studing P and NP complexity classes. I like know, why is SAT not in P? Is it because I can not determine if any Boolean expression is satisfiable?
7
votes
1answer
181 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 ...
3
votes
1answer
94 views

MIN-2-XOR-SAT and MAX-2-XOR-SAT: are they NP-hard?

What is the complexity of MIN-2-XOR-SAT and 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}^{n}C_i,$$ where ...
2
votes
1answer
78 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 ...
5
votes
2answers
170 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 ...
-1
votes
2answers
129 views

Proving TWICE-3SAT is NP-complete [closed]

The TWICE-3SAT is defined as $$TWICE-3SAT=\{(\varphi) | \varphi \text{ has at least two different satisfying assignments } \}$$ How do we prove it is in NP-complete?
6
votes
1answer
109 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 ...
0
votes
1answer
173 views

Drawing an implication graph for 2-SAT clauses

I am trying to convert the following 2-sat clauses to implications and then draw the implication graph. The clauses are: ...
1
vote
1answer
203 views

Converting a 2-SAT formula into an implication graph

Both wikipedia and my lecturer explained how the 2 satisfiability problem work. However, I am finding it really hard understanding how this formula: ...
8
votes
1answer
251 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 ...
3
votes
0answers
52 views

Reductions to SAT

There is a long-standing and seemingly ever-growing trend to reduce various (even undecidable) problems to SAT to get practically useful solvers, like for instance [1]. I'm looking for some kind of ...
9
votes
1answer
108 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 ...
4
votes
2answers
122 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 ...
1
vote
1answer
118 views

Are there more easy SAT Problems?

Apart from $2SAT$, what versions of SAT problem is complete for the class NL? Is there dynamic programming algorithm to solve the $2SAT$ Problem?
11
votes
1answer
171 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 ...
9
votes
1answer
281 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 ...
2
votes
1answer
55 views

Is the following langauge in $P$ or $NPC$

Assuming $P \neq NP$ Is the following langauge in $P$ or $NPC$: $L=\{\langle\phi\rangle\mid\phi$ is a 3CNF formula with an assignment satisfying at least half of the clauses$\}$ The first thing I ...
3
votes
2answers
187 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 ...
10
votes
2answers
401 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 ...
4
votes
1answer
403 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) ...
4
votes
1answer
84 views

Asymptotic bounds on number of 3SAT formulas with unique solutions

A set is sparse if it contains polynomially bounded number of strings of any given string length $n$ otherwise it is dense. All known NP-complete sets are dense. It was proven that P=NP if and only if ...
1
vote
2answers
499 views

Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...