Questions tagged [satisfiability]

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

Filter by
Sorted by
Tagged with
1 vote
0 answers
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 ...
nc404's user avatar
  • 111
3 votes
1 answer
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 ...
Anthony O's user avatar
  • 177
1 vote
1 answer
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 ...
Mario Giambarioli's user avatar
2 votes
1 answer
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 ...
Mario Giambarioli's user avatar
1 vote
0 answers
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 ...
komorra's user avatar
  • 71
2 votes
1 answer
297 views

Not satisfiable 3SAT instance implications

Suppose we have an instance of 3SAT that is NOT satisfiable and we say $S$. If in $S$ there are the following $8$ clauses $\left(a\vee b\vee c\right)\wedge\left(a\vee\bar{b}\vee c\right)\wedge\left(a\...
Mario Giambarioli's user avatar
0 votes
0 answers
61 views

Can anyone explain the pigeon-hole encoding method in proportional logic

Someone there who worked with cardinal contraindications within the framework of propositional logic? I have a problem understanding the pigeon-hole method. It is a method of satisfaction. I have been ...
Ľubomír Rusnák's user avatar
1 vote
0 answers
189 views

IF satisfiability problem belonged to P, can the certificate be found efficiently?

IF SAT(satisfiability problem) belongs to P, then is it possible for a certificate of an arbitrary instance of SAT to be found efficiently?
Mikey's user avatar
  • 11
1 vote
0 answers
128 views

Reduction between Parity-SAT and approximate counting

Consider two problems as defined here. Approximate counting: Given a Boolean function $f(x)$, for $x \in \{0, 1\}^{n}$, distinguish between the two cases: The number of satisfying assignments for $f(...
Sid Meier's user avatar
  • 229
0 votes
2 answers
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 ...
gautam's user avatar
  • 25
5 votes
6 answers
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?
Pierce Smith's user avatar
1 vote
0 answers
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 ...
Russell Easterly's user avatar
5 votes
2 answers
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 ...
StackMachine's user avatar
28 votes
4 answers
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 ...
Rishav's user avatar
  • 391
0 votes
1 answer
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 ...
ChaosPredictor's user avatar
2 votes
1 answer
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 ...
apen's user avatar
  • 369
2 votes
1 answer
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 ...
dda's user avatar
  • 21
2 votes
0 answers
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 ...
Nicola Gigante's user avatar
0 votes
1 answer
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)$, ...
Gabi G's user avatar
  • 315
1 vote
0 answers
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 ...
advocateofnone's user avatar
0 votes
1 answer
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 ...
Tijani Eric van Lessen's user avatar
2 votes
1 answer
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 ...
Tijani Eric van Lessen's user avatar
1 vote
2 answers
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 ...
Shaif Chowdhury's user avatar
1 vote
1 answer
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 ...
envy grunt's user avatar
0 votes
2 answers
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 }...
Amy's user avatar
  • 1
1 vote
1 answer
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 ...
user128041's user avatar
1 vote
1 answer
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.
apen's user avatar
  • 369
4 votes
0 answers
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 ...
Pushpa's user avatar
  • 933
3 votes
2 answers
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 ...
Erel Segal-Halevi's user avatar
0 votes
1 answer
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 ...
Mario Giambarioli's user avatar
1 vote
1 answer
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 ...
nick.schachter's user avatar
1 vote
1 answer
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 ...
Vaibhav Karve's user avatar
2 votes
1 answer
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 ...
Jbd's user avatar
  • 123
1 vote
1 answer
186 views

Complexity of specific cases of MAX2SAT

I know that MAX2SAT is NP-complete in general but I'm wondering about if certain restricted cases are known to be in P. Certainly the languages $L_k:=\{ \phi \,|\, \phi\,\text{is an instance of 2SAT ...
Ari's user avatar
  • 1,611
3 votes
1 answer
44 views

Is MAX-averageSAT a well-known problem?

Is there any variant of the Boolean SAT or Max-SAT problem that has a flavor of maximizing or minimizing the average of the weights of the satisfied clauses of a WCNF formula? Any literature on an ...
Akhil Dixit's user avatar
1 vote
1 answer
83 views

NP-Complete Problem and Polynomial Hierarchy

I have tried to search the internet to check if the following is correct: If $\sum_{2}$ contains a NP-Complete problem then PH collapses to NP: $PH=NP$ For example if $SAT\epsilon\sum_{2}$ than: $PH=...
Idan C.'s user avatar
  • 11
0 votes
0 answers
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 ...
Zirui Wang's user avatar
3 votes
1 answer
605 views

How many clauses are required for SAT to be NP-hard in CNF formulas?

It is not hard to see that SAT for a CNF formula with $n$ variables and a constant number of clauses can be solved in polynomial time. On the other hand, it is not hard to see that a CNF formula with $...
Bernardo Subercaseaux's user avatar
-1 votes
1 answer
85 views

Equivalence of Horn formulas tractable?

Assume I have two Horn formulas $\phi_1, \phi_2$. Horn formulas are CNF formulas so that each clause has at most one unnegated literal. For example: $x_1 \wedge (\neg x_1 \vee \neg x_2 \vee x_3 )\...
D.W.'s user avatar
  • 156k
2 votes
2 answers
128 views

Equivalence of Krom formulas tractable?

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, $\...
Pepe's user avatar
  • 165
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$ ...
Joey's user avatar
  • 53
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....
Pepe's user avatar
  • 165
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 ...
wamitw's user avatar
  • 31
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 ...
Martin Inf1n1ty's user avatar
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?
Omar Shehab's user avatar
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 ...
Vladis Becker's user avatar
-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.
user1111111134241's user avatar
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 ...
Zirui Wang's user avatar
2 votes
1 answer
123 views

Complete resolution rule for 1-in-k SAT

In CNF SAT, each clause (A or B or C or...) must contain at least one true literal. The resolution rule applies to pair of clauses who have exactly one opposite literal. (A or B or C) and (!A or D ...
user avatar
1 vote
3 answers
245 views

Counting the number of satisfied models - given mathematical constraints

Question There are plenty of algorithms for solving the #SAT problem, with one being the DPLL algorithm and is implemented for all kinds of programming languages. As far as I've seen, they all take a ...
Rikard Olsson's user avatar

1 2 3
4
5
14