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
13 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
106 views
+200

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
42 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
30 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
24 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
175 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 ...
5
votes
2answers
58 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
35 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
186 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
21 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
12 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
24 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
40 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
39 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 ...
1
vote
0answers
61 views

#SAT Complexity

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 ...
4
votes
1answer
58 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
68 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 ...
4
votes
0answers
103 views

If one shows s that UNIQUE k-SAT is in P, does it imply P=NP?

Valiant & Vazirani proved SAT transforms 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 question is, ...
1
vote
1answer
58 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
41 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
30 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
31 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 ...
9
votes
3answers
102 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
57 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
94 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 ...
3
votes
1answer
117 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 ...
4
votes
3answers
134 views

Detection of redundant boolean constraints

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 ...
2
votes
1answer
73 views

Reduce Set problem to SAT

So the problem is, given some set $M = \{x_1,x_2,\ldots,x_n\}$ and a set of subsets $S = \{S_1, S_2, \ldots, S_m\}$ where $S_i \subseteq M$. We want to find some set $X \subseteq M$ such that $|X| \le ...
3
votes
1answer
77 views

A Reduction from XORSAT to 2-SAT

Does anyone know of a non-trivial reduction from XORSAT to 2-sat since they are both in P? (By non-trivial I mean one that does not just solve the instance of XORSAT and map it to a fixed instance of ...
2
votes
1answer
111 views

Monotone boolean satisfiability with at most k 1s is NP-Complete

I am to prove that monotone boolean formula satisfiability checking when at most k variables are set to 1 is an NP-Complete problem. Proving that it is in NP is easy, but I'm having difficulty ...
-2
votes
2answers
95 views

Example for an unsatisfiable formula that can be made satisfiable by reordering quantifiers [closed]

Please give me an example of an unsatisfiable quantified 2 CNF formula. I need it in my proof and I am unable to think of one. I am looking for such an unsatisfiable quantified 2 CNF formula which ...
3
votes
1answer
92 views

Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?

Definition: A renamable Horn formula is a Boolean formula that can be transformed into a Horn formula by flipping the polarity of every instance of one of more of its variables. Example: $\qquad ...
0
votes
1answer
62 views

Check constraint under some condition in linear programming

I would like to minimize linear pseudo-boolean function $$\mathrm{obj} = \sum_i c_i \mathrm{sel}_i$$ subject to $$\sum_i c_i sel_i \geq \mathrm{Value} \qquad\qquad(1)$$ where $c_1,\dots c_5, ...
-3
votes
1answer
46 views

Why is Mixed Quantified Horn SAT in PSPACE?

I want to prove that Mixed Quantified Horn SAT is a PSPACE-complete problem. I have proved that it is PSPACE-hard. How can I prove that it is in PSPACE? My study: To prove QSAT to be in PSPACE: ...
3
votes
1answer
51 views

Why do we assume that a nondeterministic Turing machine decides a language in NP in $n^k-3$ in Sipser's proof

At page 277 of Sipser's Introduction to the Theory of Computation, a proof of the NP-completeness of SAT is given. The following comment is made on the trace of some machine $N$ which can decide a ...
3
votes
1answer
89 views

Solving SAT using tableau calculus

I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the ...
-2
votes
1answer
80 views

Quantifier String Placement [closed]

This is the edited question: Suppose I have $(x_1 \vee y_1 \vee y_2)$. x is existential and y is universal. Then it should be like this in the quantifier string: $\forall y_1 \forall y_2 \exists x_1$ ...
4
votes
3answers
192 views

What is wrong with this seeming contradiction with a paper about AND-compression of SAT?

EDIT 3: Might be wrong, but I am still confused by the answer's claim "It does not have to output an instance that preserves all satisfying assignments for all the input instances". This appears to ...
-2
votes
1answer
93 views

NP hard: Mixed Q Horn SAT

Prove that Mixed Quantified Horn SAT problem is NP hard by reducing the Q3SAT problem to it. Q3SAT: 3SAT with possibly universally and existentially quantified variables. Mixed Quantified Horn ...
2
votes
1answer
40 views

Does the AND-compression of SAT depends on the number of SAT instances?

From a paper An AND-compression is a deterministic polynomial-time algorithm that maps a set of SAT-instances $x_1,\dots,x_t$ to a single SAT-instance $y$ of size $poly(\max |x_i|)$ such that $y$ ...
5
votes
0answers
98 views

research on OR and AND compression in SAT formulas [closed]

this is a new/advanced paper on OR and AND compression of SAT formulas, a newer area of research that seems not covered in any textbooks so far. A simple proof that AND-compression of NP-complete ...
0
votes
1answer
211 views

NP Completeness of 3-SAT problem [closed]

I have started reading on algorithmic complexity for my thesis work. Already have studied on Polynomial time reducibility, NP-Complete, NP-Hard. Now trying to prove NP completeness of some of the ...
1
vote
1answer
41 views

Satisfiabilty 2-sat

Im trying to work out whether the following clause is satisfiable: {x, y},{x,¬y},{¬x, y},{¬x,¬y},{x, z},{x,¬z},{y, z},{y,¬z} My basic understanding is to work ...
3
votes
1answer
55 views

How can I identify that a restricted variant of Boolean SAT remains hard or not?

While I was studying SAT problem and its different instances, in Algorithms for the Satisfiability (SAT) Problem: A Survey by J. Gu et. al PDF, I came up with this variant (not mentioned there, but I ...
1
vote
1answer
241 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
66 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
49 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 ...
1
vote
3answers
147 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?
3
votes
1answer
59 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 ...