SAT stands for the Boolean satisfiability problem.

learn more… | top users | synonyms

-1
votes
1answer
167 views

What is the simplest known solver for a np-complete problem?

Lets define the simpler of two terms as the one with shortest description length on the untyped λ-calculus. Trying to find the simplest solver for a np-complete problem, I've got this: ...
2
votes
1answer
68 views

Complexity of generating a pseudo-Boolean function

A pseudo-Boolean function is a mapping from $\mathcal{B}^n = \{0, 1\}^n$ to $\mathbb{R}$. Following is a pseudo-Boolean function. $$s_1 s_4 - s_2 s_3 - s_3 s_5 - s_2 s_5 + s_1 + s_4 - s_1 s_3 - ...
6
votes
1answer
143 views

Limited number of variable occurrences in 1-in-3 SAT

Is there a known result on complexity class of 1-in-3-SAT with restricted number of variable occurrences? I've come up with the following parsimonious reduction with Peter Nightingale, but I want ...
1
vote
0answers
35 views

Converting Partial Weighted Max SAT to CIRCUIT SAT

I am interested in converting Partial Weighted Max SAT to SAT. I have been recommended to go through CIRCUIT SAT. Partial Weighted Max SAT consists of a set of hard clauses and a set of weighted ...
4
votes
0answers
167 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 ...
4
votes
1answer
130 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
124 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
102 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
73 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
91 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
74 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
237 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
138 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
597 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
204 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
105 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
146 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
124 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
632 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
364 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
146 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
123 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
307 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
504 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
234 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
513 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
675 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
401 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
99 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
161 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
355 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
259 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
97 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
65 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
129 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 ...
3
votes
0answers
173 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
193 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
132 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
73 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
135 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
90 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
408 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
172 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
292 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 ...