Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

Filter by
Sorted by
Tagged with
47
votes
9answers
8k views

Best Upper Bounds on SAT

In another thread, Joe Fitzsimons asked about "the best current lower bounds on 3SAT." I'd like to go the other way: What's the best current upper bounds on 3SAT? In other words, what is the time ...
48
votes
4answers
4k views

What are the best current lower bounds on 3SAT?

What are the best current lower bounds for time and circuit depth for 3SAT?
28
votes
6answers
2k views

Which SAT problems are easy?

What are "easy regions" for satisfiability? In other words, sufficient conditions for some SAT solver to be able to find a satisfying assignment, assuming it exists. One example is when each clause ...
27
votes
3answers
2k views

Translating SAT to HornSAT

Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about HornSAT seems to imply that it is, but I have not been able to chase down ...
25
votes
5answers
2k views

Verifying unique solutions of SAT

Consider the following problem: given a CNF formula and an assignment that satisfies this formula, is there another satisfying assignment for this formula ? What is the complexity of this problem ? (...
21
votes
10answers
3k views

#SAT Solver download

Could anyone please point to one or more websites where is possible to download a working implementation of a #SAT solver? I'm interested in those returning the exact solution count, not an ...
18
votes
2answers
827 views

Lower bounds on #SAT?

The problem #SAT is the canonical #P-complete problem. It's a function problem rather than a decision problem. It asks, given a boolean formula $F$ in propositional logic, how many satisfying ...
2
votes
0answers
545 views

State of the art for SAT solvers [duplicate]

Possible Duplicate: Best Upper Bounds on SAT I'm working on the obstruction-set-free grid coloring problem; a specific instance of it is described in this previous question on coloring 17x17 ...
48
votes
5answers
2k views

Theoretical explanations for practical success of SAT solvers?

What theoretical explanations are there for the practical success of SAT solvers, and can someone give a "wikipedia-style" overview and explanation tying them all together? By analogy, the smoothed ...
24
votes
4answers
2k views

Starting SAT solver papers

I want to make a first SAT solver. I know the SAT competition and the SAT conference, and there are just so many papers on this subject. I'm a starter, an overwhelmed starter. Where should I begin? ...
19
votes
3answers
2k views

Shortest Equivalent CNF Formula

Let $F_1$ be a satisfiable CNF Formula with $n$ variables and $m$ clauses. Let $S_{F_1}$ be the solution space of $F_1$. Consider the problem of determining, given $F_1$, another CNF Formula $F_2$ ...
30
votes
3answers
2k views

How many instances of 3-SAT are satisfiable?

Consider the 3-SAT problem on n variables. The number of possible distinct clauses is: $$C = 2n \times 2(n-1) \times 2(n -2) / 3! = 4 n(n-1)(n-2)/3 \text.$$ The number of problem instances is the ...
29
votes
3answers
1k views

What does one mean by heuristic statistical physics arguments?

I have heard that there are heuristic arguments in statistical physics that yield results in probability theory for which rigorous proofs are either unknown or very difficult to arrive at. What is a ...
25
votes
2answers
2k views

Why is there an enormous difference between SAT solvers?

SAT solvers are very important in algebraic attacks, for example walksat and minisat. However, when solving the benchmark problems available here there is an enormous performance difference between ...
10
votes
3answers
535 views

Is embedding a solution feasible for SAT?

I am interested in "hard" individual instances of NP-complete problems. Ryan Williams discussed the SAT0 problem at Richard Lipton's blog. SAT0 asks whether a SAT instance has the specific solution ...
8
votes
1answer
2k views

Reducing #SAT to #MONOTONE-2SAT

The problem #MONOTONE-2SAT is known to be #P-complete. This means that #SAT can be reduced to it. My question is: given a #SAT instance $F$, which is the transformation that converts $F$ to its ...
11
votes
2answers
765 views

What's the correlation between treewidth and instance hardness for random 3-SAT?

This recent paper from FOCS2013, Strong Backdoors to Bounded Treewidth SAT by Gaspers and Szeider talks about the link between the treewidth of the SAT clause graph and instance hardness. For ...
14
votes
1answer
635 views

Consequences of sub-exponential proofs/algorithms for SAT

Would there be any major consequences if SAT had at most subexponential unsat proofs or even more strongly, SAT had subexponential-time algorithms?
9
votes
2answers
386 views

Information on k-SAT (Introduction, Bounds, Methods, etc.)

I'd like to know where I can turn for a good, gentle introduction to k-SAT (this may be for mathematicians that may not have a good computer science background). I'd also like to know papers that ...
33
votes
5answers
5k views

Fast Reduction from RSA to SAT

Scott Aaronson's blog post today gave a list of interesting open problems/tasks in complexity. One in particular caught my attention: Build a public library of 3SAT instances, with as few variables ...
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 ...
32
votes
1answer
2k views

Is Gap-3SAT NP-complete even for 3CNF formulas where no pair of variables appears in significantly more clauses than the average?

In this question, a 3CNF formula means a CNF formula where each clause involves exactly three distinct variables. For a constant 0<s<1, Gap-3SATs is the following promise problem: Gap-3SATs ...
25
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 ...
13
votes
2answers
986 views

Counting solutions of Monotone-2CNF formulas

A Monotone-2CNF formula is a CNF formula where each clause is composed by exactly 2 positive literals. Now, I have a Monotone-2CNF formula $F$. Let $S$ be the set of $F$'s satisfying assignments. I ...
15
votes
6answers
3k views

variations of SAT

I looked up on the internet, but I could not find any 'big-list' of variants of SAT problem. Apart from the (common) SAT, k-SAT, MAX-kSAT, Half-SAT, XOR-SAT, NAE-SAT what else variants are ...
24
votes
1answer
1k views

What is known about the complexity of finding minimum circuits for SAT?

What is known about the complexity of finding minimal circuits that compute SAT up to length $n$? More formally: what is the complexity of a function which, given $1^{n}$ as input outputs a minimal ...
9
votes
1answer
315 views

Evidence for $\mathsf{P} \neq \mathsf{PP}$ if the polynomial hierarchy collapses?

We think that $\mathsf{PH}$ does not collapse, and that $\mathsf{PP}$ is not in $\mathsf{P}$. Suppose on the contrary that $\mathsf{PH}$ does collapse, say even $\mathsf{P}= \mathsf{NP}$. $\mathsf{...
8
votes
1answer
365 views

On theoretical aproaches for solving $\mathsf{SAT}$ in special cases

In what cases $\mathsf{SAT}$ can be solved in polynomial time? I know two cases: $2$-$\mathsf{SAT}$ and Horn-$\mathsf{SAT}$. Question 1: Is there a reference with algorithms for solving $\mathsf{...
12
votes
2answers
380 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?
11
votes
1answer
397 views

Making SAT solvers competitive with specialized algorithms

What are obstacles to making SAT solvers competitive with specialized graph algorithms? In other words, is it feasible to expect SAT solvers that can replace the role of algorithm designer -- ie, be ...
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 ...
18
votes
1answer
801 views

Context-sensitive grammar for SAT?

By a classic result of Kuroda, the complexity class NSPACE[$n$] (also known as NLIN-SPACE) is precisely the class CSL of context-sensitive languages. The satisfiability problem SAT is in NSPACE[$n$], ...
11
votes
2answers
768 views

Are quasi-polynomial sized circuits for 3-SAT trivial?

Suppose we consider 3-SAT with $v$ variables and $c$ clauses. I am researching a method that appears to take $O(v^{2+\log c})$ time/space to solve any SAT problem fitting this description, to within ...
11
votes
2answers
929 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 ...
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 ...
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 ...
5
votes
1answer
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 ...
2
votes
2answers
471 views

Questions about special types of partial assignments

Considering the definition "2-SAT: Given a CNF formula whose clauses have exactly 2 literals, does there exist an assignment of $\mathsf{TRUE}$ or $\mathsf{FALSE}$ to the variables that will ...
2
votes
1answer
962 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-...
0
votes
1answer
128 views

Comparing SAT to MCSP reduction class separations and faster SAT class separations?

Assume $SAT$ is in $QuasiP$. We immediately infer $NQuasiP=QuasiP$ and $EXP=NEXP$. From https://people.csail.mit.edu/rrw/easy-witness-nqp.pdf we infer $NQuasiP$ is not in $P/poly$ which implies $...
11
votes
3answers
782 views

Where do I turn for help with research/publishing?

I have been developing a SAT algorithm for a while, and have reached a point where I'd like to share it. I don't know many people in computer science, and I'm not sure exactly where to turn. I'm ...
8
votes
2answers
449 views

Complexity of the $(3,2)_s$ SAT problem?

Let define the $(3,2)_s$ SAT problem : Given $F_3$, a satisfiable 3-CNF formula, and $F_2$, a 2-CNF formula ($F_3$ and $F_2$ are defined on the same variables). Is $F_3 \wedge F_2$ satisfiable? What ...
7
votes
2answers
562 views

SAT Solution Space - Definition of Cluster of Solutions

I'm looking for a formal definition of Cluster of Solutions. My current understanding is the following. Let $x$ be a boolean assignment on $n$ variables. Let $f: \{ 0,1 \} ^n \to \mathbb{N}$ be a ...
7
votes
2answers
414 views

What are the current best upper bounds of #P?

#P is the class of counting problems for problems in NP. In other words, a solution to #P returns the number of solutions to a particular problem in NP. I'm wondering if there have been any studies ...
6
votes
0answers
266 views

Connected components of k-CNF formulas [closed]

Let $F$ be a random k-CNF formula with $n$ variables and $m$ clauses. Let $G$ be the undirected graph built in the following manner: there is a vertex $v$ for every clause $c \in F$, and there is an ...
5
votes
1answer
330 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 ...
1
vote
1answer
205 views

Can an oracle allowing errors be non-relativizing?

I am experimenting with k-SAT. I'm using an oracle that returns the total number of satisfiable truth assignments, which is in #P. The interest here is that this total is returned modulo a natural ...