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
0
votes
0answers
2 views

Strong ETH vs Weak ETH

I am reading basics of Exponential Time Hypothesis (ETH). There are two forms of ETH: Weaker There exists no $2^{o(n)}$ algorithm for $3$-SAT, where $n$ is the number of variables. Stronger form If $\...
0
votes
1answer
20 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 ...
1
vote
1answer
12 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 ...
-2
votes
0answers
42 views

Difference 2SAT and 3SAT

Hi and good day everyone. This is my first time here. I am new with satisfiability problem. I need to choose between 2Sat or 3Sat for my project. Here is my questions: What is the major difference ...
0
votes
2answers
70 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
1answer
35 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 ...
0
votes
1answer
34 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
1answer
25 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 ...
0
votes
1answer
34 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.
2
votes
0answers
27 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 ...
3
votes
2answers
89 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 ...
0
votes
1answer
48 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
1answer
39 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
1answer
29 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)$. a) Is ...
2
votes
1answer
34 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 ...
2
votes
1answer
89 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 ...
3
votes
1answer
40 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 ...
0
votes
1answer
46 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=...
0
votes
0answers
14 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 ...
3
votes
1answer
135 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 $...
0
votes
1answer
34 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 )\...
2
votes
2answers
72 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, $\...
2
votes
0answers
30 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
1answer
93 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....
2
votes
3answers
103 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
1answer
43 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 ...
11
votes
3answers
2k views

Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
2
votes
1answer
179 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 ...
-1
votes
1answer
37 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
0answers
27 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 ...
3
votes
1answer
59 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 ...
1
vote
3answers
169 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 ...
3
votes
1answer
33 views

Reference asking: phase transition in SAT

This is not a technical question, I hope this community has a room for such questions, but I will delete it in case this is inappropriate. It has been experimentally observed (e.g. here) that when ...
1
vote
1answer
64 views

What are the differences between symbolic execution and SAT solvers?

My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the ...
0
votes
1answer
47 views

When does Gaussian elimination solve exact 1-in-3 SAT?

Terms: A literal is a variable or its negation. A clause is a set of literals. An exact 3-in-1 clause is satisfied if an assignment of values to variables results in exactly 1 ...
0
votes
0answers
16 views

Translating running times of $3$-coloring to $k$-$SAT$ complexity

Suppose there is an $O(f(n))$ algorithm for $3$-coloring a graph on $n$ vertices what does it translate to in terms of time complexity for solving $k$-$SAT$ with $m$ clauses?
3
votes
1answer
93 views

Having trouble understanding a proof of Mahaney’s theorem

I am reading a blog post of Lance Fortnow, which includes a proof of Mahaney's theorem. I am not sure why $a’$ cannot be in between $w_i$ and $w_j$ in Case 1, and also why $a’$ cannot be in between $...
0
votes
1answer
35 views

Maximum number of positive literals in 2SAT

MAX 2SAT is NP complete. Instead of satisfying the maximum number of clauses, I have a fully satisfiable 2SAT formula and I want to have the maximum number of positive literals in the assignment (...
1
vote
1answer
61 views

P=NP when number of inputs that give 1 is bounded by polynomial

Suppose there exists some NP-complete problem such that the number of inputs that gives 1 as an output is bounded by a polynomial; that is, if the problem is $f \colon \{0, 1 \}^* \to \{0, 1\}$, then, ...
1
vote
2answers
88 views

Converting Mathematical Statements to SAT Formulas

Is it possible to write a mathematical statement (like Goldbach's conjecture, for example) as a nontrivial 3-SAT formula that is satisfiable iff that statement is true? iff it is false? iff it is ...
0
votes
0answers
25 views

the correctness of 2-satisfiability problem algorithm by using implication graph

I learned finding a solution of 2-sat problem algorithm below. The point are below (1) when constructing the implication graph (2) finding there is no occurrence of a variable x and its negation x' ...
1
vote
1answer
52 views

building a polynomial algorithm that solves SAT when given a polynomial TM that solves SAT on two formulas

Here's the question: Assume there exists a polynomial time machine $M$ that receives two formulas $\varphi_1,\varphi_2$ and satisfies the following: If $\varphi_1 \in \mathrm{SAT}$ and $\...
2
votes
0answers
27 views

Names of specific SAT variants

I enjoy reading research on satisfiability, but sometimes it's easier to find relevant information when you know the names of the variants. Example: All the clauses are width 3 and must have ...
1
vote
1answer
67 views

Turing reducibility of 2 versions of the satisfiability problem

I need help with this problem. There are 2 versions of the satisfiability problem: [1] decision version: determine whether an arbitrary formula f is satisfiable or not [2] search ...
1
vote
1answer
64 views

Reducibility of 2 boolean satisfiability problems

I beg some help with this problem. There are 2 boolean satisfiability problems. Problem $A$: Determining whether an arbitrary formula of size $n$ is $satisfiable$. Problem $B$: Determining ...
1
vote
0answers
57 views

CircuitSAT to 1-in-3SAT

This question follows Unique 3SAT to Unique 1-in-3SAT Consider an AND gate such that (A ∧ B) = C. It can be trivially expressed in 3SAT with 4 clauses and no extra variables. $$ (A ∨ B ∨ \overline{...
2
votes
2answers
209 views

Unique 3SAT to Unique 1-in-3SAT

Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment. It was made from a binary multiplication circuit where I multiplied two primes numbers A and B such ...
1
vote
1answer
30 views

Unique 1-in-3 SAT

Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment. I know the value of each bit of the unique assignment because it was made from a binary ...
0
votes
1answer
102 views

Prove or Disprove, 3SAT ≤p 2SAT, then P = NP

I know that 3SAT is in NP and 2SAT is in P. And 2SAT can reduce to 3SAT just says 3SAT is strictly harder than 2SAT, so I don't think this proves P = NP, but it doesn't seem to disprove it either.
10
votes
2answers
3k views

What is wrong with this simple proof of P=NP?

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

1
2 3 4 5
10