SAT stands for the Boolean satisfiability problem.

learn more… | top users | synonyms

0
votes
0answers
52 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 ...
7
votes
1answer
111 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?
18
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
135 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
41 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 ...
1
vote
0answers
76 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
334 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]$, ...
3
votes
0answers
56 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
211 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 ...
5
votes
1answer
175 views

Solve multiple instances of SAT with a 2-approximating #SAT query

Assume we have some oracle $A$ such that when given as input a Boolean formula $\phi$, it outputs a 2-approximation to the number of satisfying assignments of $\phi$. If we are given multiple SAT ...
10
votes
1answer
145 views

Minimum amount of colors preventing an equilateral uniformly colored subtriangle

In the Bundeswettberweb Infomatik 2010/2011, there was an interesting problem: For fixed $n$, find a minimal $k$ and a map $\varphi: \{(i,j)|i\leq j \leq n\}\rightarrow \{1,\ldots,k\}$, such that ...
1
vote
1answer
109 views

Hardness of XSAT

The standard NP-hard SAT problem is the problem of Boolean satisfiability of conjunctions of clauses, where clauses are disjunctions of literals. I am interested in the problem of the Boolean ...
4
votes
0answers
73 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 ...
3
votes
0answers
78 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 ...
4
votes
1answer
152 views

For what k is MAX-2-SAT-k NP-complete?

It is well-known that it is NP-complete to decide whether in a 2-CNF at least s clauses are satisfiable. It also follows from the reduction from 3-SAT-3 that we can suppose that every literal occurs ...
0
votes
1answer
90 views

How to go about finding the most “complex” function?

Intro Hi, I'm a hobbyist, with no formal education, tinkering with SAT solving and boolean algebra minimization. So expect bad terminology. I hope you will forgive me I'm asking a wrong question in a ...
6
votes
0answers
160 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 ...
0
votes
0answers
88 views

Determining if a function is constant or not using period finding

Consider an arbitrary boolean function $$f: {\lbrace 0,1 \rbrace}^n \rightarrow \lbrace 0,1 \rbrace$$ which we write as: $$f(x_1, x_2 ... x_n) $$ where each $x_i$ is a boolean variable We note ...
9
votes
2answers
197 views

Is Almost-2-SAT NP-hard?

Is a CNF SAT problem NP hard when the total number (but not the width) of the 3-or-more-term clauses is bounded above by a constant? What about specifically when there's only one such clause?
5
votes
0answers
104 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 ...
2
votes
0answers
138 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 ...
9
votes
1answer
237 views

Computational Model in SETH

Impagliazzo, Paturi and Calabro, Impagliazzo, Paturi introduced Exponential-Time Hypothesis (ETH) and Strongly Exponential-Time Hypothesis (SETH). Roughly, SETH says that there is no algorithm which ...
6
votes
2answers
218 views

SAT in some DTIME always via a constructive proof?

Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are ...
7
votes
1answer
247 views

Transform a CNF into an equivalent 3-CNF defined on the same variables

(I posted this question on CS ten days ago, with no answer since then - so I post it here.) Any CNF formula can be transform in polynomial time into a 3-CNF formula by using new variables. It is not ...
2
votes
2answers
308 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 ...
12
votes
0answers
298 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 ...
12
votes
1answer
126 views

Detecting circuit that's similar in functionality and implementation

Let $x=(x_1,\dots,x_n)$ be a vector of boolean variables. Let $C,D$ be two boolean circuits on $x$. Say that $C$ is similar to $D$ if: $\Pr[C(x) \ne D(x)]$ is exponentially small, when $x$ is ...
14
votes
5answers
294 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 ...
7
votes
6answers
538 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 ...
0
votes
0answers
182 views

Which subproblems of 3SAT are still NP complete?

The problems in the class NP-complete satisfies the property that if any of them is in P, then all other NP-complete problem is in P. The 3SAT is NP-complete, as much as every kSAT with $k\geq 3$. (On ...
3
votes
2answers
264 views

What's the meaning of “input size” for 3-SAT?

In the computational complexity theory, we say that an algorithm have complexity O(f(n)) if the number of computations that solve a problem with input size n is bounded by cf(n), for all integer n, ...
6
votes
0answers
109 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 ...
8
votes
1answer
302 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 ...
6
votes
2answers
283 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 ...
1
vote
4answers
209 views

Weighted SAT: is this a known problem?

Given an arbitrary SAT instance, I would like to find the solution with the minimum weight. The weight of a valid assignment is computed using a function. Is this a known problem or are there other ...
9
votes
1answer
531 views

Enumerate all solutions of a SAT problem

All the #SAT solvers I know, e.g RelSat, C2D, only return the number of satisfiable instances. But I want to know each of those instances? Is there such a #SAT solver or how I should modify an ...
2
votes
1answer
107 views

Approximate-#SAT solver

I am looking for a solver that computes an approximation to #SAT. In other words, given a formula $\phi(x)$ in CNF, approximately count the number of satisfying assignments to $\phi$. I'm interested ...
10
votes
3answers
220 views

An easy case of SAT that is not easy for tree resolution

Is there a natural class $C$ of CNF formulas - preferably one that has previously been studied in the literature - with the following properties: $C$ is an easy case of SAT, like e.g. Horn or 2-CNF, ...
7
votes
2answers
280 views

Application of methods from dynamical system to the study of k-SAT and similar problems

I am looking for literature (survey and non-survey papers) about transforming the k-SAT problem (or similar problems) into a system of Ordinary Differential Equations (ODEs) and study the solution ...
6
votes
2answers
254 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 ...
3
votes
1answer
176 views

How is this graphical representation of SAT/CSP instances called?

Given a CNF formula (SAT problem), we can construct the constraint/dependency graph, which contains a vertex for each variable and a hyperedge for each clause. Same goes for CSPs, where we have a ...
2
votes
0answers
51 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 ...
1
vote
1answer
86 views

Implied Clause and Resolvent

(I posted this question on MathSE first, no answer, that is the reason why I come here.) Let $F$ be a 3-CNF formula on $n$ variables. A clause $c$ is implied by the formula if $F$ and $F \wedge c$ ...
9
votes
2answers
525 views

Restricted Monotone 3CNF formula: counting satisfying assignments (both modulo $2^n$ and modulo $2$)

Consider a Monotone 3CNF formula having both the following additional restrictions: Every variable appears in exactly $2$ clauses. Given any $2$ clauses, they share at most $1$ variable. I would ...
8
votes
1answer
141 views

How do I use canonical ordering to reduce symmetry in the SAT encoding of the pigeonhole problem?

In the paper "Efficient CNF Encoding for Selecting 1 from N Objects", the authors introduce their "commander variable" technique for encoding the constraint, and then talk about the pigeonhole ...
4
votes
0answers
211 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, ...
9
votes
2answers
1k views

About Inverse 3-SAT

Context: Kavvadias and Sideri have shown that the Inverse 3-SAT problem is coNP Complete: Given $\phi$ a set of models on $n$ variables, is there a 3-CNF formula such that $\phi$ is its exact set of ...
3
votes
1answer
125 views

About Closure under Resolution

The question looks very simple, that is why I posted it first on MathSE, unsuccesfully - no answer for 12 days. I tried to find a short and elegant answer to the question, but I haven't succeed yet. ...
12
votes
1answer
268 views

A 3-CNF formula that requires resolution width $5$

Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. For every $w$, there are unsatisfiable formulas $F$ in ...
31
votes
0answers
529 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 ...