Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

Filter by
Sorted by
Tagged with
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 ...

1
2 3 4 5 6