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

1
2 3 4 5
11