Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

Filter by
Sorted by
Tagged with
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)$ ...
user avatar
  • 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 ...
user avatar
-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 ...
user avatar
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'$ ...
user avatar
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 ...
user avatar
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$-...
user avatar
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\...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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)$...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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. "...
user avatar
-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 ...
user avatar
  • 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 ...
user avatar
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?
user avatar
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 ? ...
user avatar
  • 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 ...
user avatar
  • 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 $...
user avatar
  • 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 ...
user avatar
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$ ...
user avatar
  • 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 ...
user avatar
  • 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?
user avatar
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=\...
user avatar
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 $|...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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, ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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,...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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)$?
user avatar
  • 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 ...
user avatar
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 $...
user avatar
  • 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 ...
user avatar

1
2 3 4 5
7