Questions tagged [sat]
SAT stands for the Boolean satisfiability problem.
307
questions
0
votes
0
answers
8
views
Do asymptotic bounds for k-SAT algorithms assume the formulas can have up to $O(|V|^k)$ clauses?
Defining the terms:
$f_k(V)$ - an unquantified boolean formula in CNF that contains clauses of length up to $k$ literals.
$V$ - the set of arguments of $f_k(V)$.
$C$ - the set of clauses $f_k(V)$ ...
- 207
0
votes
0
answers
42
views
Short UNSAT Certificates for X3SAT
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiability problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
- 499
-4
votes
0
answers
28
views
Solving K-Flip SAT problem in Polynomial time
Given a dataset with N variables, M clauses in CNF form, and a randomly generated truth assignment T. I am trying to find a truth assignment T' that flips at most k variables and satisfies more ...
- 1
0
votes
0
answers
30
views
+50
Direct fpt reduction from Weighted 3SAT to Weighted 2SAT
In parameterized complexity, for each fixed $q$, the problem Weighted $q$-CNF SAT is W[1]-complete. In particular, this means that one can turn a 3CNF formula $\varphi$ into a 2CNF formula $\varphi'$ ...
- 419
1
vote
0
answers
102
views
proof that 2-SAT is P-hard [closed]
i'm doing university work about the 2-sat problem and it is asked why 2-sat is p-hard. We discussed that 3-sat is np-hard and proved this by reduction from cnf-sat to 3cnf-sat. for my work the ...
- 11
2
votes
1
answer
124
views
Complexity of the Complete (3,2) SAT problem?
A complete $k$-CNF formula is a $k$-CNF formula which contains all clauses of size $k$ or lower it implies.
Deciding the satisfiability of a $k$-CNF formula is clearly a tractable problem since a $k$-...
- 1,069
0
votes
2
answers
67
views
Find whether a 3CNF formula with every clause having either all the variables negated or all the variables non-negated is satisfiable
Given a 3CNF formula $\phi$ with the condition that, for every clause of $\phi$, either all the variables are negated or all the variables are non-negated. For example, some allowed clauses are $(x_1\...
2
votes
1
answer
232
views
The complexity of 3SAT
It is well known that 3SAT remains NP-complete if every variable occurs exactly twice positively, exactly once negated.
then, does 3SAT remain NP-complete if every variable occurs exactly once ...
- 49
0
votes
0
answers
69
views
APX-hardness of Max-3-SAT(5)
Max-3-SAT($k$) for a natural number $k$ is the task of finding the maximum number of satisfiable clauses in a Boolean formula in CNF, where every clause contains at most 3 literals and every variable ...
- 11
6
votes
1
answer
136
views
Complexity of maximizing the number of models in a parametric formula
Let $F(x,y)$ be a propositional formula where $x$ and $y$ are vectors of Booleans. We want to maximize over $x$ the number of models of $F$ over $y$. As a decision problem, this becomes: given $F(x,y)$...
- 1,112
0
votes
0
answers
67
views
SAT to k-in-3-SAT reduction
Given a 3-SAT clause. Is there a way to convert 3-SAT to k-in-3-SAT such that:
The number of new variables introduced are less than the number of clauses (without adding dummy clauses etc.)?
The ...
- 294
-1
votes
1
answer
119
views
Polynomially solvable 3-SAT problem instances [closed]
Given the 3-SAT problem with $v$ variables and $c$ clauses:
Is there a clause to variable ratio for which the 3SAT problem is 'easy' i.e. solvable in polynomial time?
We are assuming the 3-SAT ...
- 801
6
votes
2
answers
184
views
Is there an Upper Bound on Number of Redundant Clauses in a satisfiable $3-SAT$?
For a non-empty $3-SAT$ with $n\geq3$ variables and $T\geq1$ non-identical non-degenerate clauses $C_i$:
$$S=C_1 \wedge \ldots \wedge C_T$$
where a non-degenerate clause is one containing $3$ unique ...
- 171
1
vote
1
answer
110
views
3-SAT runtime if an optimal order to eliminate possible solutions is known
As a mental exercise I have been playing around with the 3-SAT problem, but I am having difficulty proving or disproving the usefulness of a current idea that I am playing around with.
My current ...
1
vote
1
answer
205
views
Can this NP-hardness proof for Super Mario Brothers (and other games) be simplified?
In "Classic Nintendo Games are (Computationally) Hard", a generalized framework based on reducibility of 3-SAT for proving NP-hardness of classic Nintendo games is presented, and several ...
- 11
9
votes
1
answer
251
views
Does Horn SAT (Horn formula in CNF) have an integral polytope?
In some ways, my question is related to this: Is the matching polytope integral?
Matching and Horn-SAT are both polynomial time solvable.. So I wonder if there is a Horn polytope, similar to the ...
- 103
1
vote
1
answer
113
views
Lower bound for proving a random 3-SAT formula is unsat?
For a random 3-CNF formula with n variables and m clauses, assume this formula is unsat, what is the lower bound for proving it to be unsat?
Some results posted in Lower bounds for random 3-SAT via ...
- 61
0
votes
1
answer
177
views
Lexicographic Boolean satisfiability
Maximal Satisfying Assignment (Lexicographic Boolean satisfiability / LexMaxSAT), the problem of finding the lexicographically maximum x_1, . . . , x_n ∈ {0, 1}^n that satisfies Boolean formula φ, or ...
2
votes
0
answers
86
views
Resource on phase transition in MAXCUT problems
Could anyone suggest reading materials on phase transition in MAXCUT problems other than [1]? Thanks.
Ref:
Coppersmith, Don, David Gamarnik, Mohammad Taghi Hajiaghayi, and Gregory B. Sorkin. "...
- 997
-2
votes
1
answer
64
views
Linear Integer Arithmetic Satisfiability with Three Literals [closed]
I'm stuck on trying to find an unsatisfiable conjunction of the form $a \wedge b \wedge c$ where:
$a \wedge b$ is satisfiable
$a \wedge c$ is satisfiable
$b \wedge c$ is satisfiable
$a, b, c$ are ...
- 99
2
votes
1
answer
118
views
Efficient tools for checking SMT formulas with two quantifiers ($\exists\forall$)
I would like to check a sort of SMT formulas with two quantifiers where universal variables range over finite/bounded integer domains. An example formula is
$$\exists x \forall y ((y \ge 1 \land y \le ...
- 75
2
votes
0
answers
94
views
Resource on the Lee-Yang zeroes of the partition function of random $3$-SAT problems
Could anyone point me to the representative papers on the study of the Lee-Yang zeroes of the partition function of random $3$-SAT problems?
- 997
8
votes
2
answers
235
views
Are there analogous works to PPSZ algorithm for #P?
The PPSZ algorithm tells us that we can do SAT-solving for
$k-$CNF in time at-most $2^{1-(1-o(1))\frac{\pi^2}{6k}}$.
My question is that do we know such results for counting problems in class #P too ? ...
- 684
0
votes
0
answers
65
views
Asymptotically sub-optimal but provably optimal algorithms in a finite range for NP-Hard problems?
Given a formula in propositional logic with $100$ variables. We know that there can be no SAT-checking provably faster than $O(2^n)$, unless P=NP. Now let's say I could find an algorithm which does ...
- 684
0
votes
1
answer
155
views
Comparing SAT to MCSP reduction class separations and faster SAT class separations?
Assume $SAT$ is in $QuasiP$. We immediately infer $NQuasiP=QuasiP$ and $EXP=NEXP$. From https://people.csail.mit.edu/rrw/easy-witness-nqp.pdf we infer $NQuasiP$ is not in $P/poly$ which implies $...
- 12.5k
1
vote
0
answers
26
views
Clauses structure as quenched random matrix for random $k$-SAT problems
In the Section III of Statistical mechanics of the random K-SAT model, the clauses structure of random $k$-SAT problems are expressed as $M \times N$ quenched random matrix where the numbers of ...
- 997
1
vote
1
answer
126
views
Complexity of a satisfiability problem
I would like the know the complexity of a specific satisfiability problem. I have a feeling it could be solved in polynomial time, but I am not sure about it. The problem is described below.
Given $n$ ...
- 13
2
votes
1
answer
126
views
Complexity of MAX-ONEs Monotone 2-SAT with $n^{3/2}$ or $C n^2$ clauses?
Let $\phi$ be negative monotone 2-CNF on $n$ variables and $n^{3/2}$
clauses.
What is the complexity of finding satisfying assignment with maximum
number of ones $k$?
Alternatively let $G$ be a graph ...
- 1,945
3
votes
1
answer
75
views
Generating hard satisfiability problems with given constraint graph
Is there a systematic way to tune the hardness of a set of satisfiability problems (say 3-SAT or MAX2SAT) where the constraint graphs are always embeddable into a fixed given graph?
- 997
8
votes
1
answer
333
views
On $\text{ETH}$ with $m$ as parameter: consequences of algorithm running in time $2^{\delta m}$ where $\delta \to 0$ as $k \to \infty$
It has been shown in [1] that $k\text{-SAT}$ has a $2^{o(n)}$ algorithm if and only if it has a $2^{o(m)}$ algorithm, $n$ being the number of variables and $m$ being the number of clauses.
Being $s_k=\...
- 6,615
7
votes
1
answer
322
views
Is solving the following system of boolean equations NP-hard?
I reduced a problem I'm currently working on to the following system of boolean equations:
$$
X_i \iff
\begin{cases}
\bigvee_{B \in A_i} \bigwedge_{k \in B} X_k \\
true \\
false
\end{cases}
$$
Where $|...
- 173
2
votes
0
answers
133
views
Can a tractable sequence distribution prefer satisfying to unsatisfying assignments?
Let $p(x)$ be a Boolean circuit on $n$ bits $x \in \{0,1\}^n$. Consider a program that computes a probability distribution over all sequences $x$, autoregressively factored as
$$\pi(x | p) = \prod_{0 ...
- 3,211
10
votes
1
answer
288
views
The number of clauses in an unsatisfiable CNF
I am interested in generalisations of the following observation:
An unsatisfiable $k$-CNF has at least $2^k$ clauses.
A special case of the observation is when $k=n$, where $n$ is the number of ...
1
vote
0
answers
133
views
SAT solvers & SAT solving methods admitting minimal satisfying assignments
I'm in need of a SAT solver that outputs minimal assignments - that is, a set of assignments to a subset of all propositional variables such that substitution into the CNF formula makes each clause ...
- 111
1
vote
1
answer
105
views
Common solutions to 3SAT and 2SAT models comprised of the same variables
I have a problem which is a combination of 3SAT & 2SAT instances.
Consider $L$ is a set of variables $(x_1 ... x_n)$. $S_3(L)$ is a 3-SAT instance and $S_2(L)$ is a 2SAT instance, both made of ...
- 41
4
votes
1
answer
247
views
3-SAT mixed with 2-SAT formulas
Context: Refering to the question: Complexity of the $(3,2)_s$ SAT problem? and since the paper by Porshen and Speckenmayer : Satisfiability of mixed Horn formulas, we know that even when $F_3$ is ...
- 1,069
3
votes
1
answer
79
views
Translating pure literal elimination into rup
I'm exploring building a CDCL SAT-solver with interesting reduction rules. I have two rules based on pure literal elimination, but if either of these rules generate a conflict, I don't know what to ...
- 916
4
votes
0
answers
165
views
On solving Planar Circuit SAT
This enquiry is three-sided.
Side 1 - State of the art
Which is the best known algorithm for $\text{PLANAR-CIRCUIT-SAT}$?
Which is the best known algorithm for $\text{PLANAR-CIRCUIT-SAT}$ assuming ...
- 6,615
1
vote
0
answers
224
views
Disproving $\oplus$ETH by reducing $\oplus k$-SAT with $n$ variables and $m$ clauses to planar graph with $o(m^2)$ vertices?
In this question and its answer, they discuss about reducing CNF-SAT with $n$ variables and $m$ clauses to a (problem on) planar graph $G=(V,E)$ with $|V|$ as small as possible. It is said that the ...
- 6,615
4
votes
1
answer
202
views
Isomorphism preserving transformation CNF to Graph?
In short we are interested in isomorphism preserving
transformation CNF to Graph.
Let $\phi_1,\phi_2$ be CNF formulas.
Define $\phi_1$ and $\phi_2$ to be isomorphic $\phi_1 \cong \phi_2$
if there ...
- 1,945
6
votes
3
answers
505
views
Can modern SAT-Solvers utilise the symmetry of First Order Logic?
Apologies if the question is trivial or is wrongly stated, I am a Physicist!
Assuming that we have a universally quantified first-order logic sentence, all variables are universally quantified, ...
- 684
-4
votes
1
answer
138
views
Is there an algorithm for 3x3 sudokus without backtracking? [closed]
From what I can see on Wikipedia and the Internet at large, all sudoku solving algorithms (including human ones) employ some kind of EXPTIME backtracking search for some sudokus.
Are there any SAT ...
- 183
1
vote
0
answers
168
views
At most how many satisfying assignments are there for a 2SAT with n variables?
It is not obvious but easy to see that, for some fixed set of satisfying assignments, there is no 2CNF that can satisfy the set of satisfying assignment exactly, when I discover this, I wonder at most ...
- 470
4
votes
2
answers
262
views
What are those deterministic algorithms for k-SAT that are not derandomization of random algorithms like PPSZ and Schöning's local search?
I am doing a survey on k-SAT where time complexity is in terms of n, i.e. the number of variables in a formula.
As for the fast algorithms for k-SAT, we see
biased-PPSZ, PPSZ, Schöning's local search,...
- 470
1
vote
1
answer
233
views
Reducing 3-XOR-SAT to HORN-SAT
In this question - XOR-SAT to Horn-SAT reduction, two algorithms are described for reducing any XOR-SAT formula to a HORN-SAT formula.
My question is: say I limit the clauses of an XOR-SAT formula to ...
- 103
11
votes
1
answer
443
views
What is the complexity of checking equivalence of two boolean formulae without NOT symbol?
Suppose I have two boolean formulae (propositions) $P_1$, and $P_2$ (can be assumed to be in CNF) over the same variables and such that there are no "NOT" symbols used. I.e. only conjunction and ...
1
vote
1
answer
300
views
Potentially stronger form of non-$ETH$
If we have a $2^{n^a}$ algorithm to $K$-$SAT$ where $a<1$ for all $K>2$ then $ETH$ fails and literature gives consequences. What are the consequences if $a=o(1)$?
- 529
3
votes
2
answers
126
views
Understanding non-equivalence of proof lengths according to proof systems
Here, in section 4.3, Fortnow says:
But to prove P != NP we would need to show that tautologies
cannot have short proofs in an arbitrary proof system.
I am ...
9
votes
2
answers
430
views
NP-hardness of a planar SAT variant
Background:
An instance of 3-SAT is called monotone if each clause consists only of positive literals or only of negative literals.
Given an instance $\phi$ of 3-SAT, we consider the bipartite graph $...
- 141
1
vote
1
answer
1k
views
What languages can be reduced to a NP-complete problem in polynomial time
NP-complete: Language is NP-complete, when it is in NP and every problem in NP is reducible to it in polynomial time. But what languages are reducible to a NP-complete problem (for example SAT) in ...
- 121