Questions tagged [sat]
SAT stands for the Boolean satisfiability problem.
296
questions
0
votes
0answers
25 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 ...
-1
votes
1answer
83 views
Polynomially solvable 3-SAT problem instances
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 ...
5
votes
2answers
149 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 ...
1
vote
1answer
103 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
1answer
198 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 ...
9
votes
1answer
241 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 ...
1
vote
1answer
108 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 ...
0
votes
1answer
168 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
0answers
84 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. "...
-2
votes
1answer
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 ...
2
votes
1answer
117 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
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?
8
votes
2answers
224 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
64 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
147 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
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 ...
1
vote
1answer
120 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
125 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
330 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
320 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
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 ...
10
votes
1answer
280 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
0answers
105 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
102 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
244 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
72 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 ...
4
votes
0answers
156 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
223 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
187 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
472 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
135 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
143 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
243 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
208 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 ...
11
votes
1answer
372 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
299 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
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
2answers
413 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
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 ...
5
votes
1answer
254 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
144 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
336 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
394 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
322 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
248 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
301 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
60 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
272 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
101 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 ...
