# Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

659 questions
Filter by
Sorted by
Tagged with
1 vote
26 views

### What is the difference between NP and co-NP? [duplicate]

I'm trying to understand the very simple concept of co-NP but I can't figure it out. On wikipedia, it gives the example of SAT and its complement: The complement of any problem in NP is a problem in ...
• 111
1k views

### How is this reduction of 3-SAT to Half-SAT not valid? [duplicate]

I am studying algorithms and there is a question in CLRS called the Half-SAT problem We are given a 3-CNF formula with n variables and m clauses where m is even. We wish to determine whether there ...
• 177
1 vote
165 views

### Minimal unsatisfiable core algorithm

Wikipedia says that There are several practical methods of computing minimal unsatisfiable cores. but I cannot find any. I suppose that “practical methods” means polynomial algorithms. Be careful, a ...
358 views

### NOT satisfiable 3SAT instance certificate

Given a NOT satisfiable 3SAT instance, that we say $S$. Suppose that $M$ is a minimal subset of clauses of $S$ such that $M$ is NOT satisfiable. Say $X$ the subset of variables of $S$ that belong to ...
1 vote
146 views

### Which features can be considered for neural network based SAT solving?

I'm trying to implement SAT solver, based on backtracking algorithm and BCP. This SAT solver is trying to pick one literal from each clause, from 3-CNF SAT instances. I've implemented a neural network ...
• 71
297 views

• 229
62 views

### Oracle that can only definitively say if an instance is unsatisfiable

Assuming I have an Oracle that takes as input a strictly 3SAT Boolean instance and states whether the instance is satisfiable or not. If it says instance is unsatisfiable then the instance is ...
• 25
3k views

### Can anyone give me an instance of 3SAT with exactly one solution?

I need an instance of 3SAT with exactly one solution but I cannot think of or find one anywhere. Can anyone please give me an example?
1 vote
65 views

### How often can a learned clause cause this solver to backtrack?

The is an improvement to the X3SAT solver I described in What is wrong with this simple proof of P=NP? I have fixed the flaw found in that solver. Now, I want to know how often the solver described ...
1k views

### Is there a Zero-Knowledge proof for SAT?

I know that SAT can be reduced to (3 vertex) Graph colouring, and there is a Zero-knowlegde protocol (ZKP) for graph colouring. However, I am interested in a ZKP that can be performed directly on a ...
6k views

### Why is SAT so important in theoretical computer science?

In my Computability and Complexity class, we are focusing on P, NP, NP-complete, and NP-hard problems and the one thing that keeps coming up is the SAT problem, in the context of reduction from one ...
• 391
165 views

### Complementary for $SAT$

I have tried to find a definition of complementary language to $SAT$, I mean $\overline{SAT}$. But I still confused, in case of $L\in \overline{SAT}$ is it mean: if $\varphi\in L$ then all ...
61 views

### Solving largely monotone SAT formulas

I just wonder if solving largely monotone SAT formulas (meaning most clauses do not contain negated literals, but some do) is in any way easier than general SAT formulas? In other words, are there ...
• 369
172 views

### $k$-SAT completeness proof when $k$ is linear in number of variables

I'm looking at a special version of SAT in which each clause has exactly $n/2$ literals, where $n$ is the number of variables. Can we prove NP-completeness of SAT in this case? I tried reducing 3-SAT ...
• 21
255 views

### Test suite for SAT solvers

I'm looking for a collection of SAT problems that are usable for a test suite, i.e.: are small/easy to solve, that is, this is not a benchmark but a correctness test suite some satisfiable, some ...
147 views

### Show that if $SAT \in P/klog(n)$ then $SAT \in P$

Show that if $SAT \in P/klog(n)$ then $SAT \in P$ Assuming that there is a a constant $k \in \mathbb{N}$ such that $SAT \in P/klog(n)$, I need to prove that $SAT \in P$. Since $SAT \in P/klog(n)$, ...
• 315
1 vote
60 views

### Different definitions of Exponential Time Hypothesis

I am reading basics of Exponential Time Hypothesis (ETH). There are two statements for it: Statement 1 There exists no $2^{o(n)}$ algorithm for $3$-SAT, where $n$ is the number of variables. Statement ...
• 2,932
36 views

### Which of these properties hold for all FO theories? (but not regarding fragments thereof)

Which of these properties hold for all FO theories? (but not regarding fragments thereof) a. Decidable b. At least expressive as propositional logic c. NP-complete a) Decidable: no, some first order ...
20 views

### What is a disequality path in the context of equality graphs?

A path consisting of a number of disequality edges and a single equality edge A path consisting of equality edges A path consisting of a number of equality edges and a single disequality edge A ...
1 vote
393 views

### Is there any algorithm for 3SAT problem that is fast and relatively easy to implement?

Here is the description for 3SAT satisfiability problem. I already know about the DPLL algorithm, but it's implementation is pretty complex. I would like some algorithm that is relatively simpler but ...
1 vote
88 views

### 1-OR-3-SAT is in P

1-OR-3-SAT: Input: 3-CNF formula $\varphi$ Question: whether there is an assignment $x$ such that in each clause there are one or three true literals. I need to show that this problem is in $P$. I ...
• 158
498 views

### Reduce Subset-Sum to Sat

Is there a reduction from SUBSET-SUM to SAT? Just general SAT, not 3-SAT. Also the given multiset S only has positive integers. SUBSET-SUM is defined as follows: Input: a multiset S = { x1 , ... , xn }...
• 1
1 vote
699 views

### Showing resolution algorithm for 2SAT is polynomial time

I don't quite understand why the resolution algorithm completes in polynomial time for 2SAT but not 3SAT. I'm looking at slide 42 of these slides for reference. It is clear that given two clauses of ...
1 vote
766 views

### Is it generally possible to convert CNF to Horn clauses?

My intuition is that it is not generally possible, but I cannot think of a proof.
• 369
162 views

### Answer Set Program to SAT translation

During the presentation (a talk) Answer Set Programming: Boolean Constraint Solving for Knowledge Representation and Reasoning Torsten Schaub (University of Postdam) stated around twenty-one minutes ...
• 933
200 views

### Playing video games to solve SAT instances

This paper shows that computer games, such as Super Mario, are NP-hard, by reduction from SAT. It may be possible to use this reduction to help solve hard instances of SAT: use the reduction to ...
• 5,730
719 views

### 3SAT and directed graph

Given a 3SAT instance (a Boolean expression in three conjunctural normal form), we draw a directed graph, where for each Boolean variable $x_{i}$ we have the nodes $x_{i}$ and $!x_{i}$; for each ...
1 vote
85 views

### Universal Quantifiers in QBFs

I've been looking into reductions to/from the TQBF language and have managed to get stuck on something that is almost certainly not true (or, if it is true I'm missing a significant computational cost ...
1 vote
54 views

### Is there an algorithm for reducing CNFs further?

I have a Boolean formula in conjunctive normal form (CNF) $$(a\vee b \vee c) \wedge (a \vee b \vee \neg c) \wedge (x \vee y)$$ I know that this can be simplified to $(a\vee b)\wedge (x \vee y)$. Is ...
73 views

### algorithm for checking satisfiability

In order to prove that SAT is in NP, I need to come up with a polynomial time verfier (an algorithm). The Cooks Levin Theorem uses a non-deterministic Turing machine but that's not what I am looking ...
• 123
1 vote
186 views

• 11
15 views

### Global-input-local-output p-time algorithms

Are there polynomial-time algorithms whose input is global but output is local in nature? What I have in mind is a problem instead of an algorithm. It’s the satisfiability (SAT) problem. Each clause ...
• 952
605 views

• 156k
128 views

• 952