Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
641
questions
0
votes
1
answer
40
views
Why is conjunctive normal form (CNF) "better" for SAT than disjunctive normal form (DNF)?
When hand-manipulating algebra DNF (sum of products) is easier than
CNF (product of sums). Possibly because factoring is more difficult
than expanding. So why is it the opposite for computational ...
- 1,084
0
votes
1
answer
36
views
Should I remove equivalent variables in a CNF file to be used by a SAT solver?
My CNF file ends with many pairs of clauses that represent that two variables are equivalent (eg: -3 7, 3 -7, 5 -11, -5 11, etc.). Do most SAT solvers automatically pre-process these and replace every ...
0
votes
1
answer
17
views
How to solve boolean SAT with equality constraints
Say I have boolean formula in form of a CNF(x1,x2,...) with $x_i$ being boolean variables.
Testing the satisfiability of the CNF is the SAT problem, i.e. determine ...
- 161
0
votes
0
answers
54
views
Finding a Polynomial Time algorithm for the 3-SAT Problem
Let us consider m clauses containing 3 variables each i.e. A1,A2,A3...Am . Let the total literals in consideration be n. Then each clause :
Ai = (xr $\lor$ xs $\lor$ xt)
where 1 $\le$ r,s,t $\le$n and ...
-1
votes
1
answer
42
views
SAT polynomial time
Hi I understood it is not currently possible to solve SAT in polynomial time. Does this mean we can not currently solve an expression with n different boolean variables or with m different symbols in ...
- 101
1
vote
1
answer
17
views
Boolean constraints for a connected component of a graph
Suppose I have an undirected graph $G=(V,E)$, and boolean variables $x_v$ (one for each vertex $v \in V$). These variables select a subset $S \subseteq V$ of vertices, namely the vertices $S=\{v \mid ...
D.W.♦
- 152k
1
vote
1
answer
52
views
Encoding SAT EqualsK Constraint with Two Possible Values
I am wondering about a way to CNF encode an EqualsK constraint with two possible values. In other words, I want to solve for the equation:
$$
(\sum_{i=1}^n x_i = A) \lor (\sum_{i=1}^n x_i = B)
$$
...
- 13
0
votes
1
answer
26
views
Can you transform 3sat (or equivalent) into another satisfiability problem that increases the ratio of solutions to non-solutions
Say I have f(x1,x2,x3,...) where the output is either 0 for all inputs (unsatisfiable) or a variable boolean output of 0 or 1 depending on the input (satisfiable). Let's not consider functions that ...
0
votes
0
answers
48
views
Why weakening rule doesn't increase the size of resolution refutation?
I am studying the complexity of SAT resolution refutation. There is a useful tool named weakening rule
The weakening rule:
B -->B ∨ C
says that from a clause B we can derive the weaker clause B ∨ ...
- 176
0
votes
1
answer
29
views
SAT with every variable occuring exactly once
With the Circuit-SAT problem, I often see the "split" gate (I don't know the official name of it). This gate has a truth table of:
$$
\begin{array}{|c |c c|}
0 & 0 & 0\\
1 & 1 &...
- 193
0
votes
1
answer
25
views
What's the relation between DPLL and BDDs?
BDDs are a way of representing Boolean formulas.
DPLL is an algorithm to determine satisfiability of Boolean formulas.
My understanding is that the two are used for SAT solving.
How are they combined?
- 2,230
0
votes
0
answers
27
views
If $\overline{3SAT}\in BP\cdot NP$ then $PH=\Sigma_3^P$
I have the problem
If $\overline{3SAT}\in BP\cdot NP$ then $PH=\Sigma_3^P$
To solve this I am using a result $BP\cdot NP\subset NP/poly$ which I can prove (not doing here). I have two solutions but ...
- 123
0
votes
1
answer
36
views
Time complexity to convert a truth table to a boolean circuit
The SAT problem is often explained in terms of truth tables. Given some random boolean circuit, calculate its truth table; does there exist an output of $1$ in the truth table?
But how about going the ...
- 193
4
votes
0
answers
28
views
Benchmark of SAT solvers on random k-SAT instances at satisfiability threshold
I am looking for a solid reference (peer-reviewed publication) on the design and/or benchmarking of SAT solvers for random k-SAT ($4 \leq k \leq 8$) operating at satisfiability threshold.
The majority ...
- 41
0
votes
0
answers
8
views
Do you resolve all clauses in the processed bucket in the Davis-Putnam algorithm?
I'm reading the description and example of Davis-Putnam on page 102 of the Handbook of Satisfiability and I'm confused by the example they use.
To start with, they fill the following buckets
$C: \{\...
- 101
0
votes
0
answers
11
views
Would proving that finding a satisfiable input is intractable prove that SAT is intractable? [duplicate]
With the SAT problem, there is a corresponding search variant. Given an arbitrary boolean expression, find a given input such that the output of the boolean expression is $1$. To my knowledge, this ...
- 193
0
votes
0
answers
28
views
Is this a valid method to merge clauses in CNF formulas?
Assume $$C_1 = (x_1 \lor x_2 \lor \lnot x_3)\hspace{0.2cm} C_2 = (x_4 \lor x_5 \lor x_3) \hspace{0.2cm} C_3 = (x_3 \lor x_5 \lor x_6)$$ Let
$$ \phi_1 = C_1 \land C_2 \land C_3$$ and
$$ \phi_2 = (x_1 \...
- 185
2
votes
0
answers
42
views
Modified DPLL for 3-SAT by reducing to 2-SAT
In Boolean Satisfiability of CNF formulae we have $k$-SAT where each clause has at most $k$ literals. It is well known that $k$-SAT is polynomial time reducible to $3$-SAT. It is also well known that $...
- 135
0
votes
1
answer
30
views
the size of nice tree decomposition
Recently, I am reading paper An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances, which use tree decomposition to give an upper bound for SAT resolution refutation.
For a ...
- 176
0
votes
1
answer
21
views
Complexity of this variant of the Monotone(+,2−) -SAT problem?
In this post,Monotone$(+, 2^-)$-SAT problem is defined as follows:
Given a monotone CNF formula $F^+$, where each variable appears exactly once (as a positive literal), and a monotone 2-CNF formula $...
- 55
1
vote
1
answer
42
views
Is Horn-SAT with XOR-relations NP-complete?
I was wondering if the combination of Horn-SAT and XOR-SAT is solvable in polynomial time or not.
It seems they can be solved in polynomial time as both are in class P and also that Horn-SAT is P-...
- 55
1
vote
1
answer
18
views
Are the indices of variables in the formula variable?
Let $L$ be an arbitrary language in $\Sigma_3$. Thus it can be written that $x \in L \Leftrightarrow \exists y^{p(|x|)} \forall z^{p(|x|)} \exists w^{p(|x|)} \langle x,y,z,w \rangle \in B$ where $p(\...
- 2,923
1
vote
1
answer
44
views
Encoding "all-except" constraints in CNF
I am looking for an efficient CNF encoding of the following situation: I have sets of boolean literals $A = \{ a_1, \ldots, a_m \}$, $B = \{ b_1,\ldots, b_n \}$ and subsets $B_1, \ldots, B_m$, where ...
- 166
1
vote
0
answers
34
views
Restricted Planar 3-SAT NP-hard
As we all know, 3-SAT is NP-hard.
Two of the less known results are that Planar 3-SAT is NP-hard and also a 'restricted' 3-SAT, where any literal appears in at most two clauses turns out to be NP-hard....
- 133
1
vote
1
answer
48
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
33
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 ...
- 121
0
votes
2
answers
47
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
55
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. ...
- 111
1
vote
1
answer
60
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) ...
- 37
1
vote
1
answer
69
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 ...
- 11
0
votes
1
answer
56
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
3
votes
1
answer
69
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
48
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 ...
- 176
0
votes
1
answer
28
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
109
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 ...
- 195
2
votes
1
answer
64
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 ...
- 675
9
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 ...
- 195
1
vote
1
answer
40
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 ...
- 290
1
vote
0
answers
90
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
53
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
67
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 ...
- 113
1
vote
1
answer
43
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
25
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:
...
- 421
-1
votes
1
answer
159
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?
- 125
1
vote
1
answer
66
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
95
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
46
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
46
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}...
- 135