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
1 answer
29 views

Understanding the Strong Exponential Time Hypothesis

Let $n$ be the number of variables in the input formula and $m$ the number of clauses. Define $s_k = \inf\{\delta : k\text{-SAT can be solved in } 2^{\delta n} \text{ time}\}$. The strong exponential ...
  • 15
2 votes
0 answers
28 views

Problems with proof of NP-completness of SAT following Cooks original paper

I am currently in the process of trying to understand the original proof of NP-completeness of SAT given in the seminal paper by Cook [COOK71] and have struggled with a few of the details of the proof ...
0 votes
2 answers
44 views

Finding a 2SAT instance that has a specific solution set

Is there a 2SAT instance of variables $(a,b,c,d,e,f,g)$ that has exactly the solution set $S=\{ (1,0,0,0,0,0,0),(0,1,0,0,0,0,0),(0,0,1,0,0,0,0),(1,1,0,1,0,0,0),(1,0,1,0,1,0,0),(0,1,1,0,0,1,0),(1,1,1,1,...
1 vote
1 answer
25 views

Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?

I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ...
1 vote
1 answer
42 views

Variation of 3-SAT

I already know that SAT and 3-SAT are NP-complete. If in 3-SAT the Boolean expression should be divided to clauses,such that every clause contains at most (in the original problem it says exactly) ...
  • 87
1 vote
1 answer
50 views

How to reduce 3SAT to TwoOrMoreSAT?

I want to prove, that 2OrMoreSAT is NP-complete. It's defined as follows: A formula is considered strongly satisfiable if there exists a model such that two or more different literals in every clause ...
0 votes
1 answer
42 views

MAX-SAT approximation factor

I am stuck on an exercise that ask the approximation factor of a MAX-SAT approximated algorithm generalized from a MAX-3SAT algorithm MAX-3SAT: set every variable with a random value ($0$ or $1$ each ...
3 votes
1 answer
59 views

Finding a minimal set of package versions in a dependency graph with constraints

Suppose you have a dependency graph of "packages" registered in the ecosystem of a given programming language. We can model each package as a tuple ...
  • 133
1 vote
1 answer
44 views

Question about a proof of the existence of unsatisfiable linear k-CNFs for any k

Today I am reading paper Unsatisfiable Linear k-CNFs Exist, for every k by Dominik Scheder, 2007. But I have some problem to understand the proof of Theorem $3.2$. I don't know how to understand the ...
  • 165
0 votes
1 answer
27 views

How to get the formal model using propositional logic

Input There are three chairs (1,2,3) in the same row. We need to find a seat for three guests (a,b,c). Constraints The first guest does not want to be seated next to the third one (neither left nor ...
0 votes
1 answer
93 views

Why solving #2SAT in polynomial time implies P = NP?

The wikipedia article for #P states that if we have a polynomial-time algorithm for a #P-complete problem, P = NP is true. As #2SAT is #P-complete, this would mean that providing a polynomial-time ...
  • 185
2 votes
1 answer
43 views

NP-hard $k$-SAT variant with exactly $\ell$ occurrences per variable

For the purpose of this post, let $k$-SAT be SAT with exactly $k$ literals per clause, as opposed to the more common meaning of at most $k$ literals per clause. With the purpose of proving some ...
8 votes
2 answers
5k views

Is SAT an existential question?

Some sources state that an algorithm that solves the SAT problem not only needs to decide whether a given existentially-quantified formula is satisfiable or not, but, additionally, in the case where ...
  • 185
1 vote
1 answer
36 views

Possible to solve a combinatorial game with integer programming?

I recently had the idea that it would be neat if it were possible to make a SAT solver play combinatorial games. To start, I'm trying a relatively simple case of solving single-stack Misère Nim ...
1 vote
0 answers
62 views

CNF – satisfy at most a fixed number of clauses

I'm working on this task: Prove that the following problem can be solved in time $2^{k} \cdot \Vert \varphi \Vert^{\mathcal{O}(1)}$: given a boolean formula $\Vert \varphi \Vert$ in CNF, decide ...
  • 65
0 votes
1 answer
49 views

Logical Consequence - Equivalent Assertions

I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
  • 1
0 votes
1 answer
59 views

Running time of SAT and other EXPTIME algorithms

I need to propose an algorithm for a NP-hard problem. I use dynamic programming which leads to a running time $O(2^s\cdot n^2), s\leq n.$ The algorithm aims to finding a path in a graph $G(V, E)$ (in ...
1 vote
1 answer
36 views

Is ANF-SAT P or NP?

Given a finite set of equations in ANF, for example: $$ \begin{cases} (x_1 \land x_2) \oplus (x_1 \land x_3 \land x_4) \oplus 1 = 0 \\ x_3 \oplus (x_2 \land x_3 \land x_4) = 0 \\ (x_1 \land x_4) \...
  • 13
2 votes
1 answer
1k views

Why can't 3-SAT be solved efficiently if you convert all clauses (x ∨ y ∨ z) into (u ∨ z) by introducing a variable?

Let $a_i$, $b_i$, etc., be a literal, i.e., a variable or the negation of a variable. 3-SAT concerns formulas in CNF form: $(a_1 \vee a_2 \vee a_3) \wedge \dots \wedge (b_1 \vee b_2 \vee b_3)$ (3-CNF)....
0 votes
0 answers
23 views

Given an instance of a HORN-SAT problem with at most 3 literals per clause, what context-free grammar is equivalent to deciding the problem?

Given an instance of a HORN-SAT problem with at most 3 literals per clause, what context-free grammar is equivalent to deciding the problem? For example, here are some HORN clauses: ...
-1 votes
1 answer
150 views

How to prove that P = NP?

So if someone proves with an algorithm that SAT can be solved in deterministic polynomial time, then P = NP and that's it?
1 vote
1 answer
58 views

Simple Skolemization Question

Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
2 votes
0 answers
30 views

Reductions from 3-SAT that won't work directly from SAT

Our prof talked about why it's good to know that 3-SAT is NP-complete because it's easier to craft reductions from it than from plain SAT. However, all the examples we've seen (reduction to ...
  • 21
0 votes
0 answers
57 views

Polynomial Reduction from 3SAT

Given an undirected graph $G=(V,E)$ where $V$ is a set of vertices, and $E$ is a set of edges and given a set $D$ where $D \subseteq V $ and $ \forall v \in V \setminus D \: \mid \: \exists w \in D : ...
  • 1
0 votes
0 answers
45 views

Could we know what's the total number of unsatisfiable 3SAT formulas for a given n variables?

given some $n$ variables I would be interested to know what is the count of all 3SAT formulas under $n$ that are unsatisfiable. An example of all 3SAT forumlas under $n=3$ is the following: $$ ( x \...
1 vote
1 answer
42 views

Reducing a mixed Boolean expression containing XOR of conjunctions

I know that XOR-SAT can be solved in polynomial time using arithmetic in $F_2$ and Gaussian elimination. I have a set of formula that is of the form $$ G_i := \oplus_{j=0}^{i} \left ( a_j \land b_{i-j}...
  • 113
0 votes
0 answers
50 views

Can these variants of SAT/Tautology be actually pretty simple?

There are 8 (very similiar) languages I'd like to discuss here: CNF SAT DNF SAT CNF No-SAT (Existence of a false assignment) DNF No-SAT CNF Tautology DNF Tautology CNF Contradiction DNF Contradiction ...
0 votes
0 answers
35 views

resolving in CDCL

When resolving in Conflict driven clause learning, it is the case that if you resolve a conflicting clause with the reason of the negation of one of his literals, then this results in another ...
-1 votes
1 answer
38 views

Can you help me find some examples of 3co-SAT for 4 variables?

I've been studying the examples of 3co-SAT recently. It's easy to find an example of one variable. $(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$ Examples of 2 ...
  • 163
0 votes
0 answers
40 views

Why don't we consider that NP = co-NP while we can reduce Tautology problem into Satisfiability in polynomail time easily?

Let's determine if an expression is tautological or not and let's try this expression: ((a ⊼ b) ∨ c) ↔ (¬a ∨ ¬b ∨ c). We can turn this problem into CIRCUIT-SAT decision problem by asking if the ...
0 votes
1 answer
16 views

CNF-SAT time complexity and input processing

Boolean Satisfiability (CNF-SAT) problem in $n$ variables may contain a CNF formula with $O(2^n)$ clauses in the worst case. My question is: Wouldn't a program reading a CNF formula have to ...
  • 113
1 vote
1 answer
46 views

MSAT and IMSAT problems (restricted versions of SAT)

I was reading about about NP-intermediate problems on Wikipedia and saw the IMSAT problem mentioned over there. There is no Wikipedia page for that problem and they only cite this paper. In the paper ...
  • 113
1 vote
0 answers
36 views

Probability of a randomised algorithm solving SAT

Let WALKSAT be defined as follows: Let $σ$ be a random truth assignment to the vars For $t = 1, 2, . . . , 3n$: ◦ If $\phi$ is satisfied by $σ$, exit the loop ◦ Else, pick an unsatisfied clause $c$ ...
2 votes
1 answer
202 views

Complexity of the (Complete/Assign) 3-SAT problem?

A complete $k$-CNF formula on $n$ variables $(k\le n)$ is a $k$-CNF formula which contains all clauses of width $k$ or lower it implies. Let us define the (Complete/Assign) 3-SAT problem: Given $F$, a ...
1 vote
2 answers
63 views

what does **input** mean for the $3SAT$ question? Is it the number of variables $n$ or the number of clauses $m$

We know that $3SAT \in NP$, and the definition of $NP$ is as follows: $NP$ is the class of languages that have polynomial time verifiers. But I have a question: what does input mean for the $3SAT$ ...
  • 163
0 votes
1 answer
144 views

Time-complexity of evaluating a CNF formula

Given a Boolean formula over $n$ variables in CNF and a partial assignment to it, all the algorithms I can think of to evaluate the assignment run in time $\Theta(n^2)$. Is it possible to do it in $O(...
0 votes
0 answers
30 views

Correctness implication graph for 2-sat

i want to proof some stuff for the 2-sat problem. So we have something like this: $\varphi$ = (x$_{1}$ $\lor$ y$_{1}$) $\land$ (x$_{2}$ $\lor$ y$_{2}$) $\land$ ... $\land$ (x$_{n}$ $\lor$ y$_{n}$). We ...
0 votes
0 answers
46 views

I need to show that the problem is NP-complete

Double-SAT = {𝜓: 𝜓 has at least two satisfying truth assignments}. Hint: reduce from SAT. Start with a formula 𝜑 and modify it to get a formula 𝜓 so that 𝜑 is satisfibale if and only if 𝜓 has at ...
  • 11
0 votes
0 answers
54 views

Effecient encoding of sum equality in cnf+xor

I am wondering as to how to efficiently encode the following subcircuit for a binary satisfiability solver (cnf, and optionally xor clauses, if this helps): ...
  • 1,383
0 votes
1 answer
29 views

reducing the word problem for dtm to sat / cnf-sat / 2-sat

word problem: given a language L through a deterministic turing machine, is the word w in the language L? the problem should be decidable, since if there is a deterministic turing machine i can simply ...
3 votes
1 answer
75 views

Why can't $QBF$ be reduced to $SAT$

Let $QBF_k$ be the problem of determining the satisfiability of a formula of the form $Φ = Q_1x_1Q_2x_2 . . . Q_kx_k φ(x_1, . . . , x_n)$. where each $Q_i$ is one of the quantifiers $∀$ or $∃$. So, $Φ$...
2 votes
2 answers
119 views

Exponential Time Hypothesis and the input size vs number of variables

According to Exponential Time Hypothesis there does not exist a deterministic algorithm to solve SAT over $V$ variables in time $o(2^V)$. However, let's say the number of literals $n = \omega(poly(V))$...
  • 1,393
1 vote
0 answers
100 views

Is there an alternative method to using Gaussian elimination in order to solve 3-XORSAT

I have a large system of $3$-$XORSAT$ constraints (i.e. up to $3$ variables per constraint) and this can be represented in matrix form as a linear algebra problem $Ax=b$ $mod$ $2$. Solvability (i.e. ...
  • 11
1 vote
1 answer
65 views

Proving the NP hardness of two variants of SAT

$k$-$\text{RSAT}$ is a variant of $k$-$\text{SAT}$ where we restrict our attention to formulae in which each variable occurs at most $3$ times, and each literal occurs at most twice. The language $k$-$...
3 votes
1 answer
370 views

4-SAT but two literals per clause must be true

I'm trying to show that a modified 4-SAT in which at least two literals per clause must be true is NP-complete. I'll call it $4_2$-SAT. I understand the reduction from 3-SAT to 4-SAT, and I know why $...
1 vote
1 answer
43 views

Proving 2SAT is in P vs algorithm for finding a satisfying assignment

I want to understand the proof in the following link that 2SAT is in P. What is the need for the last corollary? Wouldn't be enough to just prove the case for the graph with the help of the path ...
  • 113
0 votes
0 answers
21 views

How overapproximation of boolean abstraction function works?

I just found that if original formula is unsat, using boolean abstraction function can result in sat. Clearly this is overapproximate. I wonder if I have contingent formula, does that means my boolean ...
4 votes
1 answer
179 views

What are efficient approaches to implement unit propagation in DPLL-based SAT solvers?

I'm trying to decompose deduction steps of DPLL algorithm -- unit propagation and pure literal elimination -- for parallelization. However, I want a baseline and asymptotic analysis to compare to my ...
  • 43
3 votes
1 answer
94 views

Find the flaw in the 3SAT solver algorithm

I consider decision version of 3SAT problem. Main idea is to find congruent clauses and construct such maximum formula, which satisfiability/truth table won't be changed. In case of unsatisfiable ...
4 votes
1 answer
135 views

3-SAT with atmost 3 variables and variable occuring once per clause

I've stumbled across this problem on CSES https://cses.fi/345/task/E/ and was wondering is it somehow reducible to 2-SAT with given constraints? So, the problem states that you need to solve a 3-SAT ...

1
2 3 4 5
13