Questions tagged [sat]
SAT stands for the Boolean satisfiability problem.
287
questions
2
votes
1answer
108 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 ...
2
votes
0answers
88 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?
8
votes
2answers
204 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 ? ...
0
votes
0answers
58 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 ...
0
votes
1answer
133 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 $...
1
vote
0answers
22 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 ...
1
vote
1answer
106 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$ ...
2
votes
1answer
111 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 ...
3
votes
1answer
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?
8
votes
1answer
313 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=\...
7
votes
1answer
308 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 $|...
2
votes
0answers
132 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 ...
10
votes
1answer
229 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 ...
2
votes
0answers
74 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 ...
1
vote
1answer
80 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 ...
4
votes
1answer
235 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 ...
3
votes
1answer
61 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 ...
0
votes
0answers
75 views
Hardness of approximation by reduction from MAX-E3SAT
For the MAX-E3SAT define $k=\sum_i^n (g_i-1)$, where $n$ is the number of variables and $g_i=\text{max}(\{\text{occurrences of }x_i, \text{occurrences of }\neg x_i\}), \text{ for each }i=\{1,\ldots,n\}...
4
votes
0answers
116 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 ...
1
vote
0answers
222 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 ...
3
votes
1answer
136 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 ...
6
votes
3answers
410 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, ...
-4
votes
1answer
132 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 ...
1
vote
0answers
86 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 ...
4
votes
2answers
199 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,...
1
vote
1answer
161 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 ...
9
votes
1answer
247 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
1answer
295 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)$?
3
votes
2answers
124 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
2answers
356 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 $...
1
vote
1answer
759 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 ...
5
votes
1answer
244 views
What are the consequences of a faster algorithm for $CIRCUIT$-$SAT$?
What is the best algorithm known for $CIRCUIT$-$SAT$ in $n$ variables and $m$ gates?
What is the consequence if there is an $\alpha\in(0,1)$ such that $CIRCUIT$-$SAT$ in $n$ variables and $m$ gates ...
6
votes
1answer
130 views
SMT solving with less-than theory and monotonic functions
I am attempting to solve a less-than theory within an SMT paradigm that involves variables assigned to reals and assumes that all the functions used in the theory are monotonic. The theory's signature ...
4
votes
1answer
274 views
Complexity of SAT parameterized by treewidth
Many papers state that Boolean satisfiability is in FPT when parameterized by primal, dual, or incidence treewidth. What are the best known time complexities of these parameterized algorithms? In ...
8
votes
1answer
367 views
On theoretical aproaches for solving $\mathsf{SAT}$ in special cases
In what cases $\mathsf{SAT}$ can be solved in polynomial time?
I know two cases: $2$-$\mathsf{SAT}$ and Horn-$\mathsf{SAT}$.
Question 1: Is there a reference with algorithms for solving $\mathsf{...
9
votes
1answer
315 views
Evidence for $\mathsf{P} \neq \mathsf{PP}$ if the polynomial hierarchy collapses?
We think that $\mathsf{PH}$ does not collapse, and that $\mathsf{PP}$ is not in $\mathsf{P}$.
Suppose on the contrary that $\mathsf{PH}$ does collapse, say even $\mathsf{P}= \mathsf{NP}$.
$\mathsf{...
15
votes
0answers
243 views
Does small circuits for a NP-complete problem contradict ETH?
The remarks of the Theorem 4 in the paper "On the complexity of circuit satisfiability" claims that: if circuit satisfiability (CktSat) problem can be decided by deterministic circuits of $2^{o(n)}$ ...
6
votes
0answers
277 views
Reverse Skolemization?
I'm wondering if there are any references on "reverse skolemization", that is, converting a formula with functions into one purely consisting of quantifiers by eliminating function applications.
I'm ...
5
votes
0answers
57 views
Hard family for degree-$D$ MAX-3LIN
Max 3LIN is the problem where one is given a linear system of equations $C$ over $\mathbb{F}_2$ with $3$ variables per equation, and needs to determine the maximum number of equations that can be ...
1
vote
1answer
202 views
Count satisfying assignments of CNF formulas over all possible negation assignments
Consider the set of all CNF instances that can be generated by adding negations to a single monotone CNF instance. How hard is it to compute the sum of the counts of satisfying assignments for the set?...
6
votes
1answer
98 views
Axioms of Minimum Size Resolution Refutations
Let $\phi$ be an unsatisfiable CNF formula and let $\Pi$ be a resolution refutation of $\phi$ of minimum size. Let $\psi$ be the subformula of $\phi$ containing the clauses that actually appear as ...
0
votes
0answers
80 views
Given $n\times n$ matrix $A$ with integer entries, find #$k$SAT formula that yields $\mathrm{perm}(A)>0$
For each #$k$SAT instance one can build a matrix $A$ such that $\mathrm{perm}(A) = F(\Sigma)$, where $\Sigma$ is the solution count of the $k$SAT formula and $F$ an easy to invert function.
My ...
6
votes
1answer
253 views
Example problem that is not in $2^{o(n)}$ but could be solved in $O(2^{cn})$ for any $c > 0$ (suggested by wording of ETH)
In the wikipedia article on Time Complexity it is written that:
The exponential time hypothesis (ETH) is that 3SAT, the satisfiability problem of Boolean formulas in conjunctive normal form with, ...
5
votes
0answers
122 views
Is monotone 1-in-3 MAXSAT known to be APX hard?
Monotone 1-in-3 SAT is the problem where each clause of the SAT problem contains exactly 3 positive variables. The goal is to find an assignment such that exactly one variable is true in each clause ...
2
votes
1answer
122 views
Maximum-minimum satisfiability
In MAX-SAT, given a formula, we want to maximize the number of satisfied clauses: given a formula $\phi = c_1 \cap \cdots \cap c_n$, where each $c_i$ is a disjunction, we want to find the largest $k\...
9
votes
0answers
159 views
Complexity of fractional SAT
Let $(a, k)$-SAT be $k$-SAT with the promise that if there is there is a satisfying assignment, then there is such an assignment that satisfies at least $a$ literals of every clause. Can 3-SAT with $...
1
vote
0answers
59 views
How to efficiently verify if a semantic symmetry of a CNF formula is valid?
It is easy to verify that a syntactic symmetry of a CNF formula is correct.
Is it also possible to check in polynomial time that a semantic symmetry which is not a syntactic symmetry of a formula is ...
2
votes
0answers
90 views
On the goal of learned clause database reduction in CDCL SAT solvers
Modern SAT solvers frequently reduce the size of their learned clause database in order to keep its size as manageable as possible. This has as effect not to slow down the speed of unit propagations.
...
4
votes
0answers
78 views
Finding a largest symmetrical subset of a k-CNF propositional formula
I have a k-CNF propositional formula $F$ which do not admit any global symmetry i.e. there is no permutation $\sigma$ of its variables such that $\sigma(F) = F$ . I'm interested in finding the largest ...
3
votes
0answers
59 views
Efficient transformation of clausal proof into resolution proof
Clausal proof is used to certify unsat results of SAT solvers. However the main theoretical results are on resolution proof (for instance, the non existence of a polynomial resolution proof for the ...
