Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

Filter by
Sorted by
Tagged with
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 ...
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?
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 ...
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 ...
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 ...
33
votes
2answers
4k views

Do any quantum algorithms improve on classical SAT?

Classical algorithms can solve 3-SAT in $1.3071^n$ time (randomized) or $1.3303^n$ time (deterministic). (Reference: Best Upper Bounds on SAT ) For comparison, using Grover's algorithm on a quantum ...
32
votes
3answers
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 ...
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 ...
31
votes
1answer
4k 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 ...
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 ...
30
votes
2answers
847 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 ...
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 ...
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 ...
28
votes
6answers
1k views

Well known classes of boolean formulas that require exponentially long resolution proofs

You might often find cutting plane methods, variable propagation, branch and bound, clause learning, intelligent backtracking or even handwoven human heuristics in SAT solvers. Yet for decades the ...
27
votes
7answers
19k views

Why is CNF used for SAT and not DNF?

I don't quite understand why almost all SAT solvers use CNF instead of DNF. It seems to me that solving SAT is easier using DNF. After all, you just have to scan through the set of implicants and ...
27
votes
2answers
1k views

Ladner's Theorem vs. Schaefer's Theorem

While reading the article "Is it Time to Declare Victory in Counting Complexity?" over at the "Godel's Lost Letter and P=NP" blog, they mentioned the dichotomy for CSP's. After some link following, ...
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 ...
27
votes
1answer
793 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. ...
26
votes
3answers
967 views

Computing any information about Max-3SAT

For a 3CNF formula $C$ let $M(C)$ be the maximal number of satisfied clauses in any assignment to $C$. It is known that Max-3SAT is hard to approximate (subject to P≠NP), i.e. there is no polytime ...
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 ? (...
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 ...
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 ...
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? ...
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 ...
23
votes
2answers
2k views

Are there any hard instances of 3-SAT when the clauses can only use literals that are “nearby” each other?

Let the variables be $x_1 , x_2 , x_3 ... x_n$. The distance between two variables is defined as $d(x_a , x_b) = |a-b|$. The distance between two literals is the distance between the corresponding ...
23
votes
3answers
4k views

Minimum Unsatisfiable 3-CNF Formulae

I am currently interested in obtaining (or constructing) and studying 3-CNF formulae which are unsatisfiable, and are of minimum size. That is, they must consist of as few clauses (m = 8 preferably) ...
22
votes
2answers
849 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 ...
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 ...
20
votes
5answers
28k views

Direct SAT to 3-SAT reduction

Here the goal is to reduce an arbitrary SAT problem to 3-SAT in polynomial time using the fewest number of clauses and variables. My question is motivated by curiosity. Less formally, I would like ...
20
votes
6answers
867 views

SAT algorithms not based on DPLL

Are there any algorithms for SAT solving which are not DPLL based? Or are all algorithms used by SAT solvers are DPLL based?
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$ ...
19
votes
2answers
1k 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 ...
18
votes
2answers
828 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 ...
18
votes
2answers
767 views

How many tautologies are there?

Given $m, n, k$, how many of $k$-DNFs with $n$ variables and $m$ clauses are tautology? (or how many $k$-CNFs are unsatisfiable?)
18
votes
1answer
713 views

A topological space related to SAT: is it compact?

The Satisfiability problem is, of course, a fundamental problem in theoretical CS. I was playing with one version of the problem with infinitely many variables. $\newcommand{\sat}{\mathrm{sat}} \...
18
votes
1answer
803 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$], ...
18
votes
2answers
483 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 ...
17
votes
5answers
399 views

Open or Interactive Constraint Satisfaction

In the past, I implemented coordination models using SAT and regular constraint satisfaction as the core workhorse in their engines. Continuing in this line of work, I would like to make the models ...
17
votes
5answers
608 views

Unique $k$-SAT benchmarks

This question is probably on the border line between on-topic and off-topic, however I've seen similar questions here, therefore I'll ask it. I'm implementing a Unique $k$-SAT solver, whose input is ...
17
votes
1answer
2k views

What are the #P-complete subfamilies of #2-SAT?

Short version. The original proof that #2-SAT is #P-complete shows, in fact, that those instances of #2-SAT which are both monotone (not involving the negations of any variables) and bipartite (the ...
16
votes
1answer
452 views

Average-case tautologies/contradictions, beyond the random k-CNF model

It is well known that random $ k $-CNF formulas over $ n $ variables with $ cn $ clauses are unsatisfiable (i.e. they are contradictions) with high probability, for sufficiently large constant $ c $. ...
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 ...
15
votes
1answer
439 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 ...
15
votes
1answer
1k views

Ranking the Difficulty of NP Hard Problems in Practice

This question is tightly related to another post: Phase Transitions in NP Hard Problems but it is somewhat different. While that question is about the hardness of particular instances of NP hard ...
15
votes
2answers
2k views

Random 3-SAT: What is the consensus experimental range of the threshold?

The critical ratio of clauses to variables for random 3-SAT is more than 3 and less than 6, and seems to be commonly described as "around 4.2" or "around 4.25". Mezard, Parisi, and Zecchina prove (in ...
15
votes
0answers
240 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
3answers
1k views

Checking formulas with two quantifiers ($\forall \exists$) - 2QBF

SAT solvers give a powerful way to check the validity of a boolean formula with one quantifier. For instance, to check the validity of $\exists x . \varphi(x)$, we can use a SAT solver to determine ...
14
votes
1answer
636 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?
14
votes
2answers
542 views

What's the complexity of Median-SAT?

Let $\varphi$ be a CNF formula with $n$ variables and $m$ clauses. Let $t \in \{ 0,1 \}^n$ represent a variable assignment and $f_{\varphi}(t) \in \{ 0, \ldots , m \}$ count the number of clauses ...

1
2 3 4 5 6