# 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 ...
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 ...
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 ...
297 views

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 ...
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 ...
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 ...
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 ...
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)$, ...
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 ...
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 ...
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 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.
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 ...
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 ...
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 ...
1 vote
186 views

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 ...
605 views

128 views

Assume I have two Krom formulas $\psi_1, \psi_2$. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, $\... 2 votes 0 answers 418 views ### Reducing Dominant Set Problem to SAT I am trying to solve a problem and I am really struggling, I would appreciate any help. Given a graph$G$and an integer$k$, recognize whether$G$contains dominating set$X$with no more than$k$... 1 vote 1 answer 638 views ### Is Monotone 3-SAT with exactly 3 distinct variables untractable? I have given the following SAT variation: Given a formula F in CNF where each clause C has exactly 3 distinct literals and for each C in F either all literals are positive or all literals are negated.... 3 votes 4 answers 2k views ### Why isn't SAT in coNP? I understand why NP=coNP if SAT is in coNP (How do I prove that SAT in coNP implies NP=coNP?). But I'm missing why the following machine doesn't turing recognize the complementary of SAT: Given a ... 0 votes 1 answer 64 views ### MAXSAT using dpll algorithm? It's possible to return from a dpll algorithm M as maximum for MAX-SAT problem?: I have a sample: https://gist.github.com/davefernig/e670bda722d558817f2ba0e90ebce66f we can modify recurrency to return ... 12 votes 4 answers 2k views ### Are there competitions for integer programming? Are there competitions for integer programming like there are for SAT and MAXSAT? 2 votes 1 answer 232 views ### Proof for NP-hardness of simultaneous minimization and maximization of a weighted subset I am working on a problem defined as the following Given a set of$n$elements called$R \subseteq \mathbb{N} \times \mathbb{N}$and numbers$Z,G \in \mathbb{N}$, where$Z$is a measure of our ... -2 votes 1 answer 41 views ### Does 2SAT contained in SAT? Is it true that$2 S A T \subseteq S A T ?$and in general is$k S A T \subseteq S A T $where k is any positive integer is true? Thanks. 0 votes 0 answers 156 views ### CNF encoding of additions I have$m$equations of the following form: $$x_1+x_2+\cdots+x_n=s,$$ where each variable is either 1 or 0, and the total number of variables is$m\approx3{,}000\$. So I’m thinking of modeling each ... 