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
57 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
12 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 ...
1
vote
0answers
7 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
51 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
582 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
72 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
25 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
27 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
19 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
112 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
80 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
38 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
81 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
59 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
17 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 ...
4
votes
2answers
380 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
317 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
34 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
44 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
49 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$ ...
-4
votes
1answer
32 views

Complexity if special case of SAT

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?
2
votes
1answer
65 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
339 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
41 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
26 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
131 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
51 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
53 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
58 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
210 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
69 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
45 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
191 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
27 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
18 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
36 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
54 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
41 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
64 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
71 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
75 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 ...
6
votes
1answer
149 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 ...
2
votes
1answer
69 views

Encoding the pigeonhole principle in CBMC

CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions and ...
2
votes
1answer
45 views

Sound and complete algorithms for boolean satifiability

To my best knowledge, these are the sound and complete algorithms for boolean satisfiability Variations of DPLL algorithm (e.g. CDCL, Look-ahead solvers) Stalmarks method Binary Decision Diagram ...
0
votes
1answer
42 views

Doesn't a formula that tests each boolean string of length $N$ force SAT to execute at least $2^N$ tests?

Since you are free to chose any formula for the SAT problem, doesn't the choice of a formula that requires a test for each subset of the group of variables force it to perform $2^N$, essentially ...
1
vote
0answers
33 views

infinite system MAX-SAT

Is there a generalization of maximal satisfaction (MAX-SAT) based on infinitely many variables? One natural occurrence of such problem is the general Ising model in material science.
-1
votes
1answer
41 views

Co NP problem correponding to SAT

I've been reading lately about SAT problem, NP and co-NP. Many sources say that the SAT problem is co NP, though, I can't find a co-NP problem equivalent to SAT. Does anyone have any idea about ...
10
votes
3answers
115 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 ...
1
vote
1answer
63 views

Satisfiability of first-order logic is undecidable?

I struggle with understanding why the satisfiability in the first-order logic is undecidable. Could you explain it with some examples? I've also seen that satisfiability in some first-order formulas ...
8
votes
1answer
95 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 ...