Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
493
questions
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 ...
