# Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

341 questions
Filter by
Sorted by
Tagged with
109 views

### Can you find a counterexample / disprove my P=NP solution?

I've posted the full article here. The source code is available here. Basically, in the Linear Programming (LP) task, we solve a system of inequalities: one inequality per BSAT clause. In each ...
100 views

### Is there a generalized SAT problem for higher-order logics?

The SAT problem is based upon Boolean expressions, but is there a generalized SAT problem based upon higher order logics?
• 111
1 vote
156 views

### Relation between $k$-sum failure and $P=NP$

If $P=NP$ then $W[1]=FPT$ holds. Hence $k$-sum conjecture fails at a finite $k$. What can we say about the time complexity of $SAT$ and the lowest $k$ at which $k$-sum conjecture fails? In particular, ...
• 13k
1 vote
49 views

### Short learned clauses for XSAT

Are there any studies about how effective a limited resolution pre-processor is for DPLL-CDCL type SAT solvers? By limited resolution pre-processor I mean a pre-processor that generates short (1,2, or ...
191 views

### Calculation on Sparsification and critical clauses in SAT

I followed from this question. I need to prove, the final result $s_k \leq (1 − \Omega(k^{−1}))s_{\infty}.$ But before prove the final result first I need to prove the $s_k \leq (1 − d/k))s_{\infty}$. ...
• 109
1 vote
322 views

### Sparsification and critical clauses in SAT

I have been studying the Exponential-Time Hypothesis, ETH, from this paper, there defined $s_k = \inf\{\delta \geq 0 | k\text{-}SAT \in RTIME[2^{\delta n}]\}$. But in that paper's page number 10, I ...
• 109
393 views

### Time complexity of PPZ algorithm

I am trying to understand PPZ (Paturi, Pudlák, Zane) derandomization algorithm for k-SAT, it seems to be very difficult for me. The last line in the below of the image, I don't understand the time ...
• 133
1 vote
42 views

### Max number of m-clauses NOT subsumed by k-clauses

This question is releated to: Max number of k-clauses such that no two clauses can be resolved? and How often can a clause cause a conflict Assume there are $N$ variables and a maximum size set of $k$-...
1 vote
83 views

### Max number of k-clauses such that no two clauses can be resolved?

Let $n$ be the number of variables and $k$ the size of the clauses. What is the maximum number of k-clauses such that no two clauses can be resolved to a smaller (less than $k$) clause. I will accept ...
135 views

### Solve 3CNF in Poly-Time with Satisfiability Oracle

The problem: Given an algorithm A which can tell whether any 3CNF formula is satisfiable in poly-time, develop an algorithm B that calculates a solution for the formula, also in poly-time, using A as ...
95 views

### Complexity of Identifying SAT Problems with a Unique Solution from Satisfiable Instances

I am curious about the computational complexity involved in identifying SAT problems that have only one solution from a set of satisfiable SAT instances. input and output: input: A satisfiable cnf ...
• 316
173 views

### Variation of (derandomized) Valiant-Vazirani

I am interested in the following "improvement" of the Valiant-Vazirani reduction. As pointed out here, under the right derandomization assumptions one can obtain a deterministic polynomial-...
• 987
188 views

### How often can a clause cause a conflict?

This question is about DPLL+CDCL algorithms. How often can a clause cause a conflict? I want to use a specific algorithm. Assume a DPLL+CDCL SAT solver using a fixed variable order. Variables and unit ...
242 views

### Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?

I have a question regarding the Conflict-Driven Clause Learning (CDCL) algorithm applied to an unsatisfiable CNF formula $F$. Specifically, can all the conflict clauses learned by the CDCL algorithm ...
• 316
1k views

1 vote
131 views

### Can "dense" SAT instances be solved in time $o(2^n)$?

By "dense" I mean instances in which the ratio of variables to clauses is below the critical threshold $2^k\ln2−\frac{(1+\ln2)}2+\epsilon_k$ for $k$-SAT. For general SAT, however, I suppose ...
• 355
164 views

### Conversion between NP certificates

This might be a well-known fact, but I can't convince myself of whether this is true. Suppose I have some NP language and two different verifying procedures V and V' for L. For any x in L, is it the ...
• 987
1 vote
61 views

### Efficient algorithm/ implementation to compute Transitive Closure of a Rule with respect to a Relationship

(Recalling some) Definitions: Fix a finite collection of finite sets: $A_1,\ldots,A_k$. Then relationship $R\subseteq A_1 \times A_2 \times \ldots\times A_k$. (Remark: $A_i$'s need not be distinct.) ...
1 vote
87 views

• 1,598
158 views

### What's the connection between branchwidth and treewidth

I understand that treewidth and branchwidth are essentially equivalent for a fixed graph, given that $branchwidth(G) = Θ(treewidth(G))$. However, my question pertains to a specific case involving ...
• 316
168 views

### Sources that prove solving 2-SAT with DP takes linear time

Would anyone have any sources that describe/an explanation of how solving 2-SAT using dynamic programming takes a linear amount of time? Can't seem to find a text that proves it in detail/formality. ...
1 vote
188 views

### What advancements in SMT solvers have contributed to progress in the field of theoretical computer science?

SMT solvers use first-order logic on top of SAT solvers with boolean logic. For example, CVC4 is an SMT solver able to accept a rich set of mixed constraints over strings, integers, reals, arrays, ...
• 191
2k views

### Algebraic equivalent of SAT?

Starting with a simple observation. If $x,y\in\{0,1\}$, then the arithmetic product $x\cdot y$ corresponds to the logical conjunction if we interpret $1$ as true and $0$ as false. But then, for a ...
• 1,598
92 views

### Require Hamming weight in CNF

I have a SAT problem in conjunctive normal form that I’d like to solve, but I need to add one more condition: for the existing variables $x_1,\ldots,x_n$ the Hamming weight is $k$. (It would be ok to ...
• 1,745
86 views

### Regarding UNSAT bechmark of SATLIB found as SAT instance

I found the Satisfiable assignment to one of the UNSAT [SATLIB benchmark][1] instance, specifically uuf50-01.cnf as below answer: [1, 2, 3, 4, -5, -6, -7, -8, 9, 10, -11, 12, 13, 14, -15, -16, 17, 18, ...
• 11
152 views

### 3SAT instances where no assignment fails to satisfy more than one clause: do they eixst, and what complexity class do they belong in?

Title says it all. I am curious of the 3SAT problem but limited to instances where only one clause is left unsatisfied by any literal assignment. Do such problems exist, and if they do, what is it ...
• 101
1 vote
75 views

### Running time of SAT and other EXPTIME algorithms [closed]

I need to propose an algorithm for a NP-hard problem. I use dynamic programming which leads to a running time $O(2^s\cdot n^2), s\leq n.$ The algorithm aims to finding a path in a graph $G(V, E)$ (in ...
220 views

### list of 3-CNF formula that can be solved in polynomial time

Suppose i want to program a 3-SAT solver. I want my solver to first check whether a formula is in the list of 3-CNF that currently known can be solved in polynomial time before resorting to brute ...
• 101
654 views

### Solving 3-SAT in O(n^6)?

There's an algorithm (published on GitHub) which is claimed to solve any 3-SAT formulation in polynomial time with a complexity of max O(n^6). I would usually brush claims like this away, but having ...
• 73
162 views

### Short UNSAT Certificates for X3SAT

Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiability problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
1 vote
440 views

### proof that 2-SAT is P-hard [closed]

i'm doing university work about the 2-sat problem and it is asked why 2-sat is p-hard. We discussed that 3-sat is np-hard and proved this by reduction from cnf-sat to 3cnf-sat. for my work the ...
221 views

### Complexity of the Complete (3,2) SAT problem?

A complete $k$-CNF formula is a $k$-CNF formula which contains all clauses of size $k$ or lower it implies. Deciding the satisfiability of a complete $k$-CNF formula is clearly a tractable problem ...
• 1,117
169 views

• 181
1 vote
174 views

### 3-SAT runtime if an optimal order to eliminate possible solutions is known

As a mental exercise I have been playing around with the 3-SAT problem, but I am having difficulty proving or disproving the usefulness of a current idea that I am playing around with. My current ...
1 vote