Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

66 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
44
votes
0answers
1k views

Problem unsolvable in $2^{o(n)}$ on inputs with $n$ bits, assuming ETH?

If we assume the Exponential-Time Hypothesis, then there is no $2^{o(n)}$ algorithm for $n$-variable 3-SAT, and many other natural problems, such as 3-COLORING on graphs with $n$ vertices. Notice ...
15
votes
0answers
239 views

Does small circuits for a NP-complete problem contradict ETH?

The remarks of the Theorem 4 in the paper "On the complexity of circuit satisfiability" claims that: if circuit satisfiability (CktSat) problem can be decided by deterministic circuits of $2^{o(n)}$ ...
15
votes
0answers
474 views

Williams' Method, Natural Proofs and Constructivity

I have some questions on the previous question which is written bellow. Natural Proof and Constructivity : The topic of the previous question Recently, Ryan Williams proved that Constructivity in ...
14
votes
0answers
602 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, ...
14
votes
0answers
460 views

DPLL and Lovász Local Lemma

Let $\varphi$ be a CNF formula. Suppose that each of $\varphi$'s clauses consist of exactly $t$ literals (and, moreover, all literals within one particular clause correspond to different variables). ...
12
votes
0answers
242 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\...
9
votes
0answers
150 views

Complexity of fractional SAT

Let $(a, k)$-SAT be $k$-SAT with the promise that if there is there is a satisfying assignment, then there is such an assignment that satisfies at least $a$ literals of every clause. Can 3-SAT with $...
9
votes
0answers
393 views

What are the best known reductions from SAT to CNF-SAT?

Problems Let SAT denote the following problem: Given a boolean formula, does there exist a satisfying assignment? Let CNF-SAT denote the following problem: Given a ...
9
votes
0answers
455 views

When is CSP faster than SMT/SAT?

Do CSP solvers have any fundamental advantages over SMT/SAT solvers, in terms of performance? The answer is going to be problem dependent, so I should also ask: what does a problem need to contain in ...
8
votes
0answers
266 views

Given a Boolean formula, does there exist a small circuit that computes a satisfying assignment?

The 3-SAT problem can be defined as follows: 3-SAT Input: A 3-CNF formula $\phi$ of size $m$ with $n$ variables. Question: Does there exist a variable assignment that satisfies $\phi$? ...
8
votes
0answers
140 views

“k-Swap SAT” problem

I would like to know if the following NP-complete problem has a name and has been studied: Input: Given a CNF formula $\varphi$ on $n$ variables, a truth assignment $\sigma:[n] \to \{T,F\}$ and an ...
7
votes
0answers
202 views

Converting a Truth Table into k-CNF formula of Minimal Size in Linear Time

Let $T$ be a truth table of a boolean function $f$ on $n$ input bits. More concretely $T$ could be a list of length $2^n$ such that $T[i] = f(bin(i))$, where $bin(i)$ is the binary representation of ...
7
votes
0answers
143 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 ...
7
votes
0answers
552 views

Another Solution Problem (ASP) of integer multi-commodity 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 that any SAT problem can be reduced to an integer ...
7
votes
0answers
192 views

Generalization of SAT, where we replace OR with another symmetric function

Let $\sigma(y_1,\dots,y_k)$ denote some boolean symmetric function on $k$ boolean inputs, $\sigma:\{0,1\}^k\to\{0,1\}$. In $k$-SAT, an instance is a conjunction of clauses, where each clause is the ...
7
votes
0answers
623 views

Complexity of Exactly $A$-SAT

Let define the "Exactly $A$-SAT" problem : Given a CNF formula $F$ and a set $A$ of positive integers, is it true that the number of models of $F$ is in $A$? What is the complexity of Exactly $A$-...
6
votes
0answers
270 views

Reverse Skolemization?

I'm wondering if there are any references on "reverse skolemization", that is, converting a formula with functions into one purely consisting of quantifiers by eliminating function applications. I'm ...
6
votes
0answers
219 views

How hard is APPROXIMATE-#SAT?

It is well known that the problem of counting the satisfying assignments of SAT, namely the problem #SAT, is #P-complete. It is also suspected (somewhat less widely) that even deciding SAT should ...
6
votes
0answers
533 views

Generalized sequential machine synthesis subject to language equivalence/inclusion and reachability

A generalized sequential machine (GSM) is a generalization of a Mealy machine where on each transition one input symbol is read and 0 or more output symbols are written. As in a Mealy machine, we ...
6
votes
0answers
253 views

The latest concerning Valiant-Vazirani

I'm wondering what the best method obtained for the Valiant-Vazirani theorem is. We can state the following criteria: (1) First and foremost, has anyone been able to derandomize it? (2) If not, ...
5
votes
0answers
52 views

Hard family for degree-$D$ MAX-3LIN

Max 3LIN is the problem where one is given a linear system of equations $C$ over $\mathbb{F}_2$ with $3$ variables per equation, and needs to determine the maximum number of equations that can be ...
5
votes
0answers
116 views

Is monotone 1-in-3 MAXSAT known to be APX hard?

Monotone 1-in-3 SAT is the problem where each clause of the SAT problem contains exactly 3 positive variables. The goal is to find an assignment such that exactly one variable is true in each clause ...
5
votes
0answers
125 views

Seminal papers related to SMT theories (particularly QF_ABV)

I am working on an application using Quantifier-Free Bit-Vector/Array satisfiability which may or may not require mucking around with the internals of an SMT solver, and would like to understand what'...
5
votes
0answers
86 views

Reference request for a $\Delta_2^P$ satisfiability problem

I am looking for the name and a reference for a $\Delta_2^P$-complete problem that looks like the following Input: A collection of CNF formulas $\phi_i(x_1^i, x_2^i,\dots, x_m^i, z_1, z_2, \dots, z_{...
5
votes
0answers
405 views

How to do Type Inference using an SMT solver?

I understand that Hindley-Milner Type Inference can be implemented using an off-the-shelf SMT (Satisfiability Modulo Theories) solver? How would this work, for example for a very simple type system (...
5
votes
0answers
155 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 (...
5
votes
0answers
241 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 ...
5
votes
0answers
117 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 ...
4
votes
0answers
110 views

On solving Planar Circuit SAT

This enquiry is three-sided. Side 1 - State of the art Which is the best known algorithm for $\text{PLANAR-CIRCUIT-SAT}$? Which is the best known algorithm for $\text{PLANAR-CIRCUIT-SAT}$ assuming ...
4
votes
0answers
78 views

Finding a largest symmetrical subset of a k-CNF propositional formula

I have a k-CNF propositional formula $F$ which do not admit any global symmetry i.e. there is no permutation $\sigma$ of its variables such that $\sigma(F) = F$ . I'm interested in finding the largest ...
4
votes
0answers
180 views

Subexponential algorithms vs separations

Williams (see also slide 29 here) has shown that an $\frac{2^{n}}{n^{10}}$ algorithm for satisfiability of circuits belonging to a class $\mathcal{C}$ imply that $\mathrm{NEXP}\nsubseteq \mathcal{C}$. ...
4
votes
0answers
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 ...
4
votes
0answers
117 views

Variant of Toda's theorem for intermediate levels of the polynomial hierarchy

Is there a version of Toda's theorem for intermediate levels of the polynomial hierarchy ? More precisely, is there any variant of the Toda's theorem that states: Let $\# wSAT$ be the number of ...
4
votes
0answers
117 views

Gradual increase in hardness from P to PH of #SAT

We know that counting the number of solutions to $3-SAT$ is the canonical $\#P-Complete$ problem. Equivalently, it is the canonical $PH-Hard$ problem. However, counting the number of solutions to $3-...
4
votes
0answers
280 views

What is the complexity of #satisfiable instances of k-SAT ?

To continue the question posted by user1749 on Oct 13 2010 : How many instances of 3-SAT are satisfiable? Which was: Consider the 3-SAT problem on n variables. The number of possible distinct ...
3
votes
0answers
59 views

Efficient transformation of clausal proof into resolution proof

Clausal proof is used to certify unsat results of SAT solvers. However the main theoretical results are on resolution proof (for instance, the non existence of a polynomial resolution proof for the ...
3
votes
0answers
266 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 ...
3
votes
0answers
64 views

How fast can we group clauses with few variables in common in k-SAT?

Given a k-SAT problem with $C$ clauses and $V$ variables, we can group the clauses together into groups of $g$ clauses with few exceptions, where the exceptions contain $g-1$ or fewer clauses. If we ...
3
votes
0answers
144 views

Hardness of Horn-modulated Satsifiability problem?

It is known that there is sharp complexity jump between Horn 3-SAT and 3-SAT problems. The former is $P$-complete while the later is $NP$-complete. I would like to see a continuous spectrum of ...
2
votes
0answers
129 views

Can a tractable sequence distribution prefer satisfying to unsatisfying assignments?

Let $p(x)$ be a Boolean circuit on $n$ bits $x \in \{0,1\}^n$. Consider a program that computes a probability distribution over all sequences $x$, autoregressively factored as $$\pi(x | p) = \prod_{0 ...
2
votes
0answers
67 views

SAT solvers & SAT solving methods admitting minimal satisfying assignments

I'm in need of a SAT solver that outputs minimal assignments - that is, a set of assignments to a subset of all propositional variables such that substitution into the CNF formula makes each clause ...
2
votes
0answers
89 views

On the goal of learned clause database reduction in CDCL SAT solvers

Modern SAT solvers frequently reduce the size of their learned clause database in order to keep its size as manageable as possible. This has as effect not to slow down the speed of unit propagations. ...
2
votes
0answers
106 views

Transforming a DAG-like resolution proof to a tree like resolution proof

How can a DAG-like resolution proof be transformed to a tree-like resolution proof? Is such a transformation possible in polynomial time?
2
votes
0answers
37 views

Approximate answer to Max-SMT (bitvector) query

I have a problem that could be completely solved as Max-SMT instances in the theory of quantifier-free bit-vectors, but it apparently is too complex to be tractable with current Max-SMT technology. ...
2
votes
0answers
81 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 ...
2
votes
0answers
75 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 ...
2
votes
0answers
88 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 ...
2
votes
0answers
163 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 ...
2
votes
0answers
183 views

Most general form of SAT which is in P

2-SAT is in P. Additionally, a (CNF) SAT-problem is trivially poly-time solvable if no two expressions can be resolved (via Robinson resolution, ie for every pair of disjunctive clauses, they either ...
1
vote
0answers
22 views

Clauses structure as quenched random matrix for random $k$-SAT problems

In the Section III of Statistical mechanics of the random K-SAT model, the clauses structure of random $k$-SAT problems are expressed as $M \times N$ quenched random matrix where the numbers of ...