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

learn more… | top users | synonyms (1)

1
vote
1answer
18 views

Shaefer's Dichotomy Theorem [duplicate]

Could you please resolve a confusion with Schaefer's theorem for me? Namely, why does it not imply many problems in P are NP-complete? For example, primality testing surely cannot be reduced to one of ...
3
votes
0answers
47 views

“Balancing” positive and negative literals in 2-sat

I saw in an answer to this post that it is possible to construct 3-sat clauses with extra variables such that the number of positive and negative literals for each variable are equal. Does anyone ...
-1
votes
0answers
17 views

Resolution rule for SAT [closed]

Consider the following statement. Let $x$ be a propositional variable and $\alpha$ and $\beta$ be propositional formulas. The formula $\phi_1 = (x \vee \alpha) \wedge (\neg x \vee \beta)$ ...
2
votes
1answer
75 views

Complexity of a SAT related problem

Given a set of (propositional) formulae $\Phi$, two formulae $\phi$ and $\xi$, determine whether there exists $\Psi\subseteq \Phi$ such that $\Psi\models \phi$ and $\Psi\not\models \xi$. Question: ...
6
votes
1answer
58 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 ...
9
votes
1answer
1k 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 ...
0
votes
1answer
44 views

Can Tarjan's SCC algorithm find satisfying assignment to just 'any' digraph?

Is Tarjan's algorithm capable of finding satisfying assignment to any digraph consists of variables (vertices) and implications (edges)? I know that it solves implication graphs constructed by 2SAT ...
8
votes
2answers
77 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 ...
6
votes
1answer
39 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 ...
1
vote
1answer
95 views

Can Circuit Value Problem or HORN-SAT be reduced to PATH problem?

PATH = {(X,R,S,T) | exists an x in S that is admissible} Where R is a relation of X x X x X, S is a unary relation of X and T is a unary relation of X aswell. An x element of X is admissible if it is ...
0
votes
0answers
15 views

Arthur-Merlin protocol to decide a set size

Please look at the example here at the bottom of page 3, http://www.cs.nyu.edu/~khot/CSCI-GA.3350-001-2014/sol3.pdf Here it seems that the set whose size Arthur is trying to approximate is known in ...
2
votes
0answers
25 views

Parameterized complexity of Weighted Satisfiability with few variable occurrences

Given an integer $k$ and a Boolean CNF Formula $\phi$, Weighted Satisfiability asks whether $\phi$ is satisfiable by a model of weight $k$, i.e., a model that sets at most $k$ variables to true. This ...
2
votes
1answer
63 views

The initial NP-complete problem

It is always claimed that Cook and Levin gives the very first NP-complete problem and proof of it. But when I look at the actual proof I think what Cook and Levin did was reduced (or transformed) SAT ...
4
votes
2answers
675 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
votes
2answers
91 views

Why don't modern SAT solvers use the notion of a “watched clause”, in the same way they use the notion of a “watched literal”?

Modern SAT solvers use the notion of "watched literals": when a value is chosen for a literal $l$, the solver only checks whether that falsifies clauses with $l$ in them if $l$ is one of the watched ...
2
votes
1answer
32 views

If in all satisfying assignments all pair of variables can take all possible values is this tautology?

I suppose this is both easy and false. Let $\phi$ be propositional boolean formula on variables $x_1 \ldots x_n$. Suppose in all satisfying assignments of $\phi$, all pairs of variables $(x_i,x_j),i ...
2
votes
1answer
42 views

Basic question about backjumping in SAT solvers

I am reading "Formalization and Implementation of Modern SAT Solvers", by Filip Marić. My question is about how backjumping is defined. In an example [1], there is a conflict clause C equal to ...
1
vote
1answer
24 views

How does derandomization of 3SAT work via conditional expectations?

Given a single SAT clause with its 3 literals coming from 3 different variables it is obvious that a random assignment of values will satisfy it with probability 7/8 But I do not understand how ...
-1
votes
1answer
152 views

How to prove a Double CNF SAT is in NP [duplicate]

So I've been stuck trying to figure this problem out for a while. I've looked on wikis and all over stack exchange but I'm really stumped. This isn't my best subject, so any sort of explanation would ...
-1
votes
1answer
83 views

Restricted version fo CNF-SAT

Given formula $\phi$ on CNF-form in CNF-SAT. Clauses can be arbitrarily long. The problem is NP-complete and it is also given that part of the problem is that a variable can occur many times in a ...
3
votes
0answers
50 views

smallest satisfiability-equivalent formulas (generalized Tseitin transform)?

What is known about the following optimization problem for formulas in propositional logic: input: formula $F$ output: formula $G$ in CNF with $\mathrm{Var}(G) \supseteq \mathrm{Var}(F)$ such that ...
7
votes
2answers
89 views

Switching Lemma and AC0 reductions between SAT problems

Have there been efforts to show (using the Switching Lemma), for example, that SAT or 3SAT cannot have an AC$^0$ reduction to 2SAT? What are the issues or difficulties involved? SAT and 3SAT are ...
2
votes
1answer
63 views

How to choose between several constraints for a SAT task using quality metric?

I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin ...
1
vote
0answers
18 views

Efficiently decidable logics

So propositional logic (PL) is efficiently (in P) decidable because I can convert formulas to an equisatisifiable CNF-formula, negate and convert (efficiently, by De Morgans laws) to DNF. I can then ...
5
votes
2answers
430 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 ...
7
votes
1answer
343 views

DNF to CNF conversion: Easy or Hard

In relation to the thread CNF to DNF — conversion 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 paper, they seem to ...
2
votes
1answer
43 views

Constructing solution to 3SAT formulas using oracle queries [duplicate]

I'm interested in 3SAT and querying an oracle. Suppose we had an oracle that can decide, on an input boolean formula $\phi$, whether there exists any assignment to the variables that makes the formula ...
-2
votes
1answer
50 views

Proof of Circuit-Sat to Nand-Sat polynomial time many–one reducibility

Given a gate called Nand with the following truth table: A | B | A Nand B ------------------ 0 | 0 | 1 0 | 1 | 1 1 | 0 | 1 1 | 1 | 0 We can ...
3
votes
1answer
52 views

Understanding terms related to 2SAT algorithm [closed]

Recently I am learning about solution of the 2-satiability problem using strongly connected components. There is a theorem related to this problem given below: Let $F = Q_lx_1 Q_2x_2\ldots Q_nx_n C$ ...
-3
votes
1answer
39 views

Complexity if special case of SAT [duplicate]

I have the following problem: How to show that the special case of SAT, in which each clause has either exactly two literals or at most one negative literal, is NP-complete?
3
votes
1answer
67 views

Are there name and literature for this SAT-like problem?

Given $f : \{0,1\}^* \to \{0,1\}$ and $n \in \mathbb{N}$, we define $\textsf{Prob}(f,n)$ as the following problem: Find an $x \in \{0,1\}^n$ such that $f(x) = 1$. A machine solving ...
3
votes
3answers
416 views

The relation between 2SAT and 3SAT

Show that proving 2SAT is not NP-Complete would prove that 3SAT is not in P. Or eqivalently - Show that proving 3SAT is in P would prove that 2SAT is NP-Complete. I can see there is an ...
3
votes
1answer
61 views

Are there any open source SAT solvers with UNSAT core extraction algorithm built in?

Just like the title says. I need to use a SAT solver on a series of CNF formulas but not only do I need an answer of the type satisfiable/unsatisfiable but also some subset of clauses whose ...
1
vote
1answer
28 views

How is the complexity of algorithms to solve 3CNF (decision problem) specified? [duplicate]

For k inputs, the complexity of naive algorithm is O(2^k). I understood this one. What is meant by "the size of the instance to be solved should be polynomial in k". Is it equivalent to the statement ...
4
votes
1answer
133 views

Algorithm for a special case of SAT/#SAT

Does anyone know of an algorithm that can solve the following special case of SAT in polynomial time? Are there any algorithms that can solve the counting (#SAT) version of it in polynomial time? ...
0
votes
1answer
56 views

SAT for arithmetic

Given two integers $X$ and $Y$, each can be encoded in binary $X=(x_4 x_3 x_2 x_1)$ and $Y=(y_4 y_3 y_2 y_1)$, how do I encode the constraint $$|X-Y|\geq n \quad\text{and}\quad|X-Y|= n$$ when $n$ is ...
0
votes
1answer
64 views

Satisfying assignments, twice-3SAT NP complete [duplicate]

I wanted to solve the following problem about 3SAT . The question is 1. to show if the problem is NP-complete and 2. whether the problem has two different satisfying assignments. "TWICE-3SAT Input: ...
3
votes
2answers
74 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 ...
7
votes
2answers
212 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 ...
6
votes
2answers
74 views

Common method for solving satisfiability problems which lie in P

I know from Schaefer's Dichotomy Theorem that only a few types of satisfiability problems are in P and any other problem is NP-complete. However, all of the algorithms I know for them use specific ...
2
votes
1answer
47 views

How do I prove a certain upper bound on the runtime of a probabilistic 2-SAT solver?

As a homework we had to prove a set of upper bounds on a given probabilistic algorithm to find a satisfying assignment for a satisfiable 2-CNF formula. The problem is reproduced below. I'm sorry for ...
5
votes
2answers
196 views

Why do we care about random Boolean SAT formula?

I've been looking for a reference for the above question. As far as I know the answer is: If we can make a solver that is efficient for all randomly generated instances, it should be efficient for ...
1
vote
1answer
31 views

Hardness of 3SAT-k

According to these scribe notes (and a paper), 3SAT-5 is NP-hard. The problem is defined to be: given a 3SAT formula, each variable occurs in at most 5 clauses. It is also proven that 3SAT-4 is ...
2
votes
0answers
21 views

Applications for balanced Boolean function satisfiability

Assume the following problem: Input: A Boolean black-box $U$ of a balanced Boolean function (balanced meaning equal number of satisfying and unsatisfying truth assignments) Output: A satisfying ...
0
votes
1answer
44 views

Constrain certain variables in CNF to unique satisfying assignments

[Reposted because the original question was deleted by the poster.] I'm looking for a way to add additional clauses (and maybe additional variables) to an already existing SAT instance so that ...
1
vote
1answer
60 views

How many satisfying assignments are there in a set of 3-CNF clauses where no clause share the same variable?

Say I have a set of 3-CNF clauses $$\mathcal{S} = \{ x_1 \vee x_2 \vee \bar{x_3}, ~~x_4 \vee x_5 \vee x_6\}$$ where $\bar{x}$ is the negation of $x$. Each variable range over $\mathbb{Z}^2$. How ...
0
votes
0answers
42 views

Is there a constant for size of disjoint clauses in 3-CNF

We are given a 3-CNF formula $\Phi$ on n variables, and a guarantee that at least $\epsilon$ fraction of $2^n$ possible assignments satisfy all clauses in $\Phi$. Now construct set $S$ of disjoint ...
0
votes
0answers
68 views

#SAT Complexity [closed]

I have been looking at algorithms for solving #SAT and calculated that simply extending a SAT algorithm like DPLL by adding the negation of a solution to the original formula and solving again takes ...
5
votes
1answer
83 views

Why is DPLL better than brute force?

I understand that by being clever about the way we navigate the search space of the SAT problem we're going to get better performance than by randomly choosing and testing solutions, though of course ...
1
vote
1answer
76 views

What complexity class is this ciruit problem?

I'm exploring an algorithm that solves k-SAT. It uses a ton of preprocessing, so I'm thinking that this will be a circuit bounds. Without knowing the runtime, I speculate on how quickly it will ...