Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

Filter by
Sorted by
Tagged with
3 votes
2 answers
385 views

Generate connected induced subgraphs as the satisfying assignments to a SAT instance

I want a SAT instance (in CNF) whose set of satisfying assignments are the connected induced subgraphs of a given input graph. A general solution would be helpful, but I really only need this when the ...
Alejandro's user avatar
  • 141
13 votes
1 answer
3k views

Improving Cook's generic reduction for Clique to SAT?

I am interested in reducing $k$-Clique to SAT without making the instance much larger. Clique is in NP so it can be reduced to SAT using logarithmic space. The straightforward Garey/Johnson textbook ...
András Salamon's user avatar
5 votes
1 answer
700 views

Can we confirm that 2-SAT can indeed be transformed into Horn-SAT in this manner?

In the question, Translating SAT to HornSAT, Martin Seymour gives a method due to Joshua Grochow. It transforms 2-SAT into Horn-SAT, by creating a variable for every possible 2-SAT clause. Then, if ...
Matt Groff's user avatar
  • 2,100
14 votes
1 answer
651 views

How is the MA version of SETH proven to be false?

According to this paper, which discusses a nondeterministic extension of the Strong Exponential Time Hypothesis (SETH), "[…] Williams has recently shown related hypotheses about Merlin-Arthur ...
user avatar
2 votes
0 answers
87 views

#2-SAT or 3-SAT and variable that appears most often

Has anyone explored running times of 3-SAT or #2-SAT given by the occurrences of the highest occurring variable? In other words, if the variable that appears most often appears $x$ times, has anyone ...
Matt Groff's user avatar
  • 2,100
14 votes
0 answers
687 views

Does solving matrix multiplication in quadratic time imply that SETH is false?

I have a little conjecture that if you could perform matrix multiplication (or solve 3-clique) in $O(n^2 \log(n))$ time, then you could solve CNF-SAT in $O(2^{(1-\epsilon)n})$ time. In other words, ...
Michael Wehar's user avatar
1 vote
2 answers
94 views

Abstract high-level framwork for #SAT

In Abstract DPLL and some other sources there is a high-level framework/ model explained using states and transitions. I need (to build) such a model for a #SAT algorithm. I do know that #SAT ...
Fleeep's user avatar
  • 155
19 votes
2 answers
2k views

Is there a non-deterministic linear time algorithm for CNF-SAT?

The decision problem CNF-SAT can be described as follows: Input: A boolean formula $\phi$ in conjunctive normal form. Question: Does there exist a variable assignment that satisfies $\phi$? I'm ...
Michael Wehar's user avatar
1 vote
0 answers
79 views

Complexity of QBF with Restrictions on Models [closed]

Do you know the complexity of the following decision problem? Given a quantified boolean formula (QBF) $\phi$ with $2n$ free variables with $n\in\mathbb{N}$. Is there a satisfying assignment s.t. ...
Heinrich Ody's user avatar
6 votes
1 answer
311 views

Best SAT upper bounds based on number of clauses

What's the best upper bounds based on number of clauses? In this question shown fastest algorithms for SAT, but there bounds depends from number of variables ( $O(const^n)$ where n is number of ...
Alexey Kholodkov's user avatar
-1 votes
1 answer
45 views

pseudo boolean modularity constraint?

I have a constraint like d >= a ^ b ^ c, where a,b,c,d are binary, ^ is XOR. Is this a pseudo boolean modularity constraint or not? Most Pseudo boolean modularity constraints I saw are with equality, ...
HoneyB's user avatar
  • 3
2 votes
1 answer
358 views

Space requirements for solving True Quantified Boolean Formulas problem [closed]

I came across this section on the wikipedia page for the TQBF solving problem, and just can't wrap my head about the fact that the space requirement is linear. Moreover, it does not provide any ...
Nicolas Mattia's user avatar
-2 votes
1 answer
436 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: ...
MaiaVictor's user avatar
  • 3,137
2 votes
1 answer
88 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 - ...
Omar Shehab's user avatar
11 votes
2 answers
2k 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 ...
Ian Gent's user avatar
  • 428
2 votes
0 answers
149 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 ...
MSJ's user avatar
  • 21
4 votes
0 answers
194 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 ...
maomao's user avatar
  • 1,345
4 votes
1 answer
289 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 $x_{1\...
Tim's user avatar
  • 627
10 votes
1 answer
2k 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 ...
Dominik Peters's user avatar
6 votes
1 answer
152 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). Thus,...
John Threepwood's user avatar
12 votes
0 answers
266 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 (M\...
John Threepwood's user avatar
5 votes
0 answers
158 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 (...
Matt Groff's user avatar
  • 2,100
2 votes
0 answers
91 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 ...
Matt Groff's user avatar
  • 2,100
15 votes
1 answer
477 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 ...
user avatar
2 votes
1 answer
167 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 ...
Kobold's user avatar
  • 41
28 votes
1 answer
886 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. ...
joro's user avatar
  • 1,955
5 votes
1 answer
353 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 ...
joro's user avatar
  • 1,955
4 votes
2 answers
279 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 ...
Atamiri's user avatar
  • 185
5 votes
0 answers
256 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 ...
Thomas Ahle's user avatar
-3 votes
1 answer
264 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 ...
Martin Seymour's user avatar
30 votes
2 answers
919 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 ...
Ryan Williams's user avatar
33 votes
1 answer
5k 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 ...
the gods from engineering's user avatar
2 votes
1 answer
122 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 ...
Ivan's user avatar
  • 21
2 votes
1 answer
255 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 $B^n\...
Marc's user avatar
  • 686
7 votes
0 answers
153 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 ...
Matt Groff's user avatar
  • 2,100
12 votes
3 answers
1k 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 ...
Sameer Gupta's user avatar
8 votes
3 answers
312 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 ...
András Salamon's user avatar
23 votes
2 answers
1k 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 a ...
András Salamon's user avatar
9 votes
1 answer
2k 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 ...
Omar Shehab's user avatar
12 votes
1 answer
1k 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 ...
Giorgio Camerani's user avatar
32 votes
3 answers
2k 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 ...
JWM's user avatar
  • 742
9 votes
2 answers
2k 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, ...
Russell Easterly's user avatar
5 votes
0 answers
121 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 ...
vzn's user avatar
  • 11k
10 votes
1 answer
1k 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?
user24175's user avatar
  • 375
5 votes
1 answer
1k 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 ...
joro's user avatar
  • 1,955
2 votes
1 answer
1k views

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

The Unambiguous 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 Valiant-...
joro's user avatar
  • 1,955
5 votes
1 answer
406 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 computational ...
Shen's user avatar
  • 53
1 vote
0 answers
127 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 ...
joro's user avatar
  • 1,955
5 votes
2 answers
3k 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$ ...
rnegrinho's user avatar
  • 183
4 votes
3 answers
279 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 ...
mrsteve's user avatar
  • 443

1 2 3
4
5
7