SAT stands for the Boolean satisfiability problem.

learn more… | top users | synonyms

-3
votes
0answers
84 views

Complexity of a generalization of SAT-UNSAT [on hold]

I posted the following question in cs-stackexchange as I do not think it is a research-level one. However, there has not been an answer yet. So I think it might warrant a trial here. Given a set of ...
4
votes
0answers
162 views

A SAT related question

Given a sequence of $n$ propositional formulas $\varphi_1, \cdots, \varphi_n$, a propositional formula $\phi$, a number $1\leq \theta\leq n$. Define $K=\min\{k\mid \wedge_{i=k}^n \varphi_i\not\models ...
3
votes
1answer
122 views

Is SAT with two “opposite” solutions NP-hard?

Here is a variant of the SAT problem in which a satisfying assignment must have additional properties. Input: A 3-CNF formula $f$ with variables $x_{1\dots k}$. Output: For an assignment $S$ of ...
6
votes
0answers
117 views

Does 1-in-3 SAT remain NP-hard even if every variable occurs both positively and negatively?

The standard problem 1-in-3 SAT (or XSAT or X3SAT) is: Instance: a CNF formula with every clause containing exactly 3 literals Question: is there a satisfying assignment setting precisely 1 literal ...
6
votes
1answer
100 views

Is the computation of a satisfying variable assignment for a Boolean formula $FP^{NP}$-hard?

By the well-known self-reducibility of SAT we can obtain a satisfying variable assignment for a Boolean formula by a polynomial number of calls to an $NP$ oracle (delivering only yes/no answers). ...
7
votes
0answers
66 views

Is the computation of a minimal correction subset (MCS) $FP^{NP}$-hard?

MCS problem: Given a set $\phi$ of Boolean clauses. Find a minimal correction subset (MCS) $M\subseteq\phi$ such that: $\phi\setminus M$ is satisfiable and for all $c\in M$ holds $\phi\setminus ...
5
votes
0answers
88 views

Satisfiability threshold and partially random formulas

My understanding is that if we have a totally random k-SAT formula, for a ratio $m < \alpha n$ far enough below the satisfiability threshold, we can solve for satisfiability in polynomial time ...
2
votes
0answers
71 views

Forming Sets from 3-SAT Clauses

I'm wondering if someone can provide a good algorithm for the following problem. If we take 3-SAT in conjunctive normal form, we can partition some or all of the variables (not the literals) into ...
12
votes
1answer
234 views

Complexity of the search version of 2-SAT assuming $\mathsf{L = NL}$

If $\mathsf{L = NL}$, then there is a logspace algorithm that solves the decision version of 2-SAT. Is $\mathsf{L = NL}$ known to imply that there is a logspace algorithm to obtain a satisfying ...
2
votes
1answer
136 views

Deciding satisfiability and non-validity

For propositional logic, a decision procedure for satisfiability can be turned into a decision procedure for non-validity by giving it the negated version of a formula. Does this hold for all logics ...
22
votes
1answer
592 views

Are there subexponential algorithms for PLANAR SAT known?

Some NP-hard problems which are exponential on general graphs are subexponential on planar graphs because the treewidth is at most $4.9 \sqrt{|V(G)|}$ and they are exponential in the treewidth. ...
4
votes
1answer
199 views

Reduction SAT to a problem on a planar graph with as few vertices as possible

Let $\phi$ be CNF formula with $n$ variables and $m$ clauses. I am looking for a reduction is $\phi$ satisfiable to a problem on a planar graph $G$ with as few vertices as possible. The majority of ...
3
votes
2answers
104 views

Translation of context-free parsing into SAT

Is there a published algorithm for translating a context-free parsing problem into SAT? That is, an algorithm that translates a context-free grammar and an input string into a set clauses that is ...
5
votes
0answers
143 views

Is MAX-SAT SETH (like) hard?

If we make a random assignment to the variables in $k$-sat ($m$ clauses), we are going to satisfy $(1-2^{-k})m$ clauses in expectation. In general satisfying fewer clauses is considered easy. There ...
-3
votes
1answer
121 views

Why can't Horn-SAT be solved in Log-space? [closed]

A simple algorithm for Horn-SAT (in CNF) is the following: Given: A Horn formula $\phi$ in CNF. Find a unit clause (a clause with one literal) $C_i$. $~$Set the variable $x_j$ appearing in $C_i$ to ...
29
votes
2answers
627 views

Is there an oracle such that SAT is not infinitely often in sub-exponential time?

Define $io$-$SUBEXP$ to be the class of languages $L$ such that there is a language $L' \in \cap_{\varepsilon > 0} TIME(2^{n^{\varepsilon}})$ and for infinitely many $n$, $L$ and $L'$ agree on all ...
17
votes
1answer
331 views

Constraint satisfaction problem (CSP) vs. satisfiability modulo theory (SMT); with a coda on constraint programming

Does someone dare to attempt to clarify what's the relation of these fields of study or perhaps even give a more concrete answer at the level of problems? Like which includes which assuming some ...
2
votes
1answer
107 views

Is there a name for this Assignment definition

The standard Assignment Problem asks for an optimal one-to-one assignment between agents and tasks. Now consider the following generalization: Instead of specifying a cost of a single agent-task ...
2
votes
1answer
142 views

Complexity of reversible Circuit Value

I am wondering what is known about the complexity of the reversible Circuit Value Problem (rCVP) and the corresponding reversible Satisfiability problem (rSAT). More precisely: a circuit ...
7
votes
0answers
122 views

What's the upper bounds for #3-SAT circuits?

We have, from this thread on 3-SAT upper bounds, and this answer on #P that the current best upper bounds for 3-SAT is faster than $O(1.31)^n$, and approximately $O(1.64^n)$ for #3-SAT. Can we do ...
9
votes
3answers
302 views

Properties expressible in 2-CNF or 2-SAT

How does one show that a certain property cannot be expressed in 2-CNF (2-SAT)? Are there any games, such as pebble games? It seems that the classical black pebble game and the black-white pebble ...
7
votes
3answers
192 views

How many sets of vectors can be represented as the solutions of a Horn-SAT instance?

Let the solution space of a SAT instance be the set of Boolean vectors of satisfying assignments of $\{0,1\}$ to the variables (that result in the formula evaluating to TRUE). In other words, a ...
22
votes
2answers
498 views

Best current space lower bound for SAT?

Following on from a previous question, what are the best current space lower bounds for SAT? With a space lower bound I here mean the number of worktape cells used by a Turing machine which uses ...
7
votes
1answer
226 views

Conversion between k-SAT and XOR-SAT

According to XOR Satisfiability Solver Module for DPLL Integration by Tero Laitinen, we need $2^{n-1}$ CNF clauses to convert an $n$ literal XOR-SAT clause if we do not want to increase the number of ...
7
votes
0answers
507 views

Consequences of $\oplus \mathbf{P} \subseteq \mathbf{NP}$

I have part of a proof attempt of $\oplus \mathbf{P} \subseteq \mathbf{NP}$. The proof attempt consists of a Karp reduction from the $\oplus \mathbf{P}$-complete problem $\oplus$3-REGULAR VERTEX COVER ...
22
votes
2answers
672 views

Is this variation of TQBF still PSPACE-complete?

Deciding if a quantified boolean formula such as $\forall x_1 \exists x_2 \forall x_3\cdots \exists x_n \varphi(x_1, x_2,\ldots , x_n),$ always evaluates to true is a classical PSPACE-complete ...
7
votes
2answers
389 views

MAX 1 in 2 SAT Algorithm

The maximum satisfiability problem (Max-Sat) is the problem of finding the maximum number of clauses that can be satisified in a Boolean satisfiability instance. The exactly 1 in 2 Sat problem asks, ...
4
votes
0answers
98 views

extracting/ exploiting similarity of SAT instances by solver

suppose that two SAT formulas on different variables $F_1, F_2$ are given on the input that are known to be true and the problem is to build an algorithm that finds a solution to each. the formulas ...
1
vote
0answers
158 views

Definition of Planar 3-SAT

What is the standard definition of Planar 3-SAT? I have seen a number of different definitions. What was the original paper that defined it and proved it to be NP-complete?
5
votes
1answer
351 views

Reduction from SAT to 0,1 integer linear program with zero or one solutions

Probably this is well known. There is probabilistic reduction from SAT to Unique SAT (0 or 1 solutions). According to answer and comments derandomizing the reduction would imply $PH \subseteq \oplus ...
1
vote
1answer
255 views

Would derandomizing the reduction from SAT to Unique SAT imply $NP$ and $coNP$ are in $\oplus P$?

The Unique SAT problem (USAT) is to determine whether a given formula has a satisfying assignment, when we are guaranteed that it has at most one satisfying assignment. By a theorem ...
3
votes
1answer
96 views

Satisfiability for various branching programs

Clearly, SAT for CNF, formula, or many classes of boolean circuits have strong significance on the entire theory community. Branching program, or BDD is one of the most basic and popular ...
1
vote
0answers
64 views

(co-)Horn formulation of Frankl's union-closed sets conjecture

Based on comments on MO there is simple forumlation of Frankl's union-closed sets conjecture in terms of (co-)Horn. In co-Horn CNF at most one literal is negated in every clause (Horn CNF where every ...
-1
votes
1answer
125 views

SAT formula specifying that exactly $k$ of $N$ boolean variables are active using less than $N$-choose-$k$ terms

Is there a way to express the condition that exactly $k$ of $N$ boolean variables are active without writing a disjunction of $N$-choose-$k$ terms, i.e., all possible configurations of the $N$ ...
4
votes
3answers
127 views

Remove unneeded atoms in CNF minimalization (SAT preprocessing)

This might be a very basic question. I am interested in all atoms of a propositional formula that can be removed from a particular formula, while the derived formula has the same satisfiability ...
2
votes
0answers
170 views

Independent Sets that are Odd Covers

I am interested in a certain type of independent set I call an "odd cover". A set of vertices is independent if no two vertices in the set are connected with an edge. A set of vertices is an "odd ...
8
votes
2answers
191 views

Approximating #P-hard problems

Consider the classical #P-complete problem #3SAT, i.e., to count the number of valuations to make a 3CNF with $n$ variables satisfiable. I am interested in the additive approximability. Clearly, there ...
2
votes
2answers
130 views

Number of SAT checks that are needed to find all combinations of subset of boolean variables of a propositional formula

Please mind that I sometimes lack formal mathematical knowledge and English is not my first language, so I might miss the right words. Please change the tile if needed. Also, I have choosen this site ...
0
votes
0answers
71 views

A self-contained proof that OrdHorn relations are tractable?

I'm currently investigating a family of temporal relations called 'Ordered Horn' ($OH$ for short). This class was introduced in 'Reasoning about Temporal Relations: A Maximal Tractable Subclass of ...
8
votes
1answer
130 views

$\overline{SAT} \in NTIME(subexp)$?

Is it possible that $\overline{SAT} \in NTIME(\exp(n^{0.9}))$ ? Are there interesting consequences of such containment? Would it contradict the Exponential Time Hypothesis?
21
votes
3answers
1k views

Has there been any research on $k$-SAT above the satisfiability threshold?

A well known characteristic of $k$-SAT instances is the ratio of the number of clauses $m$ over the number of variables $n$, i.e., the quotient $\rho = m/n$. For every $k$, there is a threshold value ...
2
votes
0answers
149 views

Is SAT in $c^{\sqrt{n}}$ time with preprocessing worthwhile?

We may be able to solve SAT in $c^{\sqrt{n}}$ for $n$ variables and a constant $c$. Now we can suppose that we require a certain amount of preprocessing to get this result. For example, in this ...
0
votes
0answers
55 views

quadratic constraints in a constraint satisfaction problem

It seems like most constraint satisfaction problems can be posed in terms of SAT. The question is two fold 1) How can any CSP with quadratic constraints be framed as a satisfiability instance 2) Is ...
0
votes
0answers
89 views

Does this meet the space requirements for the lower 3-SAT bounds?

According to "What are the best current lower bounds on 3SAT?", Ryan Williams has an answer that states that the (time * space) requirements for 3-SAT must meet or exceed $n^{2 \cos(\pi/7) - o(1)}$ ...
5
votes
3answers
404 views

If SAT is in PCP, for some constant q, then P = NP

I have seen this statement before, but I haven't really seen a proof of it: If $SAT\in PCP_{1,2^{−q}}[\log(n),q]$, for some constant $q$, then $P = NP$. Now, if $SAT\in PCP_{1,2^{−q}}[\log(n),q]$, ...
4
votes
0answers
169 views

another solution problem (ASP) of integer multicommodity flow: is it NP-complete?

I know that integer multicommodity flow is NP-complete. It was proven in "On the complexity of time table and multi-commodity flow problems" (http://dl.acm.org/citation.cfm?id=1382492) that any SAT ...
18
votes
2answers
289 views

Polynomial time solvable instances of Max-Sat

The problem Max-Sat ask you to find an assignment of a CNF formula which satisfy as many clauses as possible. For the simpler problem SAT there are many known special cases which can be solved in ...
5
votes
1answer
195 views

Solve multiple instances of SAT with a 2-approximating #SAT query

Assume we have some oracle $A$ such that when given as input a Boolean formula $\phi$, it outputs a 2-approximation to the number of satisfying assignments of $\phi$. If we are given multiple SAT ...
10
votes
1answer
170 views

Minimum amount of colors preventing an equilateral uniformly colored subtriangle

In the Bundeswettberweb Infomatik 2010/2011, there was an interesting problem: For fixed $n$, find a minimal $k$ and a map $\varphi: \{(i,j)|i\leq j \leq n\}\rightarrow \{1,\ldots,k\}$, such that ...
1
vote
1answer
170 views

Hardness of XSAT

The standard NP-hard SAT problem is the problem of Boolean satisfiability of conjunctions of clauses, where clauses are disjunctions of literals. I am interested in the problem of the Boolean ...