Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
503
questions
-3
votes
0answers
31 views
parameterized complexity
Given a SAT formula $φ$ where no variable appears negated, decide if there exists a satisfying assignment which sets at most $k$ variables to value 1.
Show that this problem can be solved in roughly $...
0
votes
2answers
35 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 ...
5
votes
6answers
2k 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
0answers
36 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 ...
2
votes
2answers
91 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 ...
25
votes
4answers
5k 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 ...
0
votes
1answer
51 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 ...
2
votes
1answer
40 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 ...
2
votes
1answer
30 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 ...
2
votes
0answers
42 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 ...
0
votes
1answer
39 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
0answers
19 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 ...
0
votes
1answer
26 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 ...
2
votes
1answer
13 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
2answers
84 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
40 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
46 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
45 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
42 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.
4
votes
0answers
97 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
95 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
74 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
40 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
34 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
38 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
99 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
41 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
48 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
144 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
35 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
76 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
43 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
110 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
168 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
47 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
185 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
35 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
67 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
171 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
34 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
93 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
69 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
106 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
39 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
63 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
95 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 ...
