Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

6
votes
1answer
77 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
66 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
227 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, ...
4
votes
0answers
79 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
97 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\...
8
votes
0answers
117 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
41 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
81 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
73 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 ...
2
votes
0answers
52 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 ...
2
votes
0answers
83 views

Transforming a DAG-like resolution proof to a tree like resolution proof

How can a DAG-like resolution proof be transformed to a tree-like resolution proof? Is such a transformation possible in polynomial time?
4
votes
1answer
75 views

Resolution augmented with the rule of symmetry or the rule of extension

Krishnamurthy (here is the abstract of his paper) showed that resolution augmented with the principle of symmetry forms a proof system (referred to as SR) in which certain formulas (which do not admit ...
-5
votes
1answer
117 views

What do you think of Bokov's “CNF-SAT is in P” proof? [closed]

There are now several versions of G. V. Bokov's paper "Complexity of the CNF-satisfiability problem", cf. https://arxiv.org/abs/1804.02478 In the most recent version of his paper, the proof is only ...
2
votes
0answers
35 views

Approximate answer to Max-SMT (bitvector) query

I have a problem that could be completely solved as Max-SMT instances in the theory of quantifier-free bit-vectors, but it apparently is too complex to be tractable with current Max-SMT technology. ...
22
votes
2answers
2k views

Are there any hard instances of 3-SAT when the clauses can only use literals that are “nearby” each other?

Let the variables be $x_1 , x_2 , x_3 ... x_n$. The distance between two variables is defined as $d(x_a , x_b) = |a-b|$. The distance between two literals is the distance between the corresponding ...
6
votes
1answer
234 views

What are the consequences of solving XOR 3-SAT in Logspace?

XOR Formulas Consider boolean formulas with connectives $\wedge$ (AND) and $\oplus$ (XOR). Such a boolean formula is a valid instance for XOR SAT if it is a conjunction of $\oplus$-clauses. An $\...
1
vote
0answers
87 views

Proof of SAT is complete for NP via first-order reductions

So I have been reading this: https://people.cs.umass.edu/~immerman/book/ch7.pdf I do not understand the proof of theorem 7.16, which says that SAT is complete for NP via first-order reductions. My ...
2
votes
1answer
516 views

What is best known space requrement for solving SATISFIABILITY problem in exp time

I searched a lot for finding best space requirement algorithm for SATISFIABILITY problem but I didn't find any thing better than brute force that is in DSPACE(n). is there exists better bound? and ...
1
vote
1answer
102 views

Can MONOTONE WSAT be in solved in polynomial time?

In the weighted monotone satisfiability problem (MONOTONE WSAT), the input is an n-variable MONOTONE CNF Boolean formula (when there is no a clause with a negated variable) and an integer k, and the ...
1
vote
1answer
51 views

Is there a standard format for Dependent QBF?

I know there is a standard input format DIMACS for a formula is in conjunctive normal form (CNF) and QDIMACS for quantified Boolean formulas. Is there a similar standard format for the Dependent-QBF (...
5
votes
0answers
107 views

Seminal papers related to SMT theories (particularly QF_ABV)

I am working on an application using Quantifier-Free Bit-Vector/Array satisfiability which may or may not require mucking around with the internals of an SMT solver, and would like to understand what'...
6
votes
1answer
155 views

Ways to think formally about Satisfiability Modulo Theories

Apologies if this is not a well-thought-out question, but I am interested in formalizing a problem which is ultimately described by a SMT formula in the theory of quantified arrays and linear ...
4
votes
0answers
185 views

How hard is APPROXIMATE-#SAT?

It is well known that the problem of counting the satisfying assignments of SAT, namely the problem #SAT, is #P-complete. It is also suspected (somewhat less widely) that even deciding SAT should ...
6
votes
2answers
551 views

a polynomial representation of boolean functions

I came up with this linear transformation to map boolean functions to polynomials and it seems to have some nice properties. I was wondering if there is any reference describing this (and/or similar) ...
1
vote
0answers
87 views

How hard is gapped satisfiability?

It is well known that general satisfiability (of polynomially many clauses) is NP-hard, and in fact, it is conjectured that an algorithm deciding instances of SAT takes time nearly $2^n$ on $n$ ...
4
votes
1answer
390 views

Sparsification Lemma for k-SAT and Exponential Time Hypothesis

According to R. Impagliazzo, R. Paturi and F. Zane, 2001 an instance of $k$-SAT is called sparse if $m = O(n)$ where $m$ denotes the number of clauses and $n$ the number of variables. The ...
0
votes
1answer
74 views

Reduction from SAT to binary matrix subset problem

I'm trying to understand the answer by @Denis on this question, where he showed a way to reduce from SAT to the binary matrix column subset selection problem. The reason I'm having to post a new ...
1
vote
0answers
456 views

Equality Constraints over Sets with Tree Automata

Tree Automata can be used to model sets of values of a Herbrand Universe, for example, to model possible values in a functional program. Systems of subtype constraints over set expressions have ...
7
votes
1answer
189 views

How to benchmark #2-SAT counting algorithms?

Are there any libraries of #2-SAT instances that are hard to solve with state-of-the-art exact solvers (sharpSAT, cachet, ...)? Alternatively: are there practical ways to generate hard #2-SAT ...
2
votes
1answer
279 views

Minimum Unsatisfiable Core

Recently in a course I'm taking, we have been learning about the DPLL(T) algorithm for SMT solving. The basic outline goes like this: ...
9
votes
1answer
225 views

Understanding performance of QFBV SMT solvers

SMT solvers such as Z3 or Boolector use a complex set of heuristics to solve problems. However, this also makes predicting the performance of such a solver for a given problem very hard. My question ...
3
votes
1answer
257 views

Is deciding whether all satisfying assignments are NAE assignments coNP-complete?

Let the language $L$ consist of the $k$-CNF formulas $\phi$ with the property that any satisfying assignment $x$ of $\phi$ is a Not-All-Equal (NAE) assignment, i.e. every clause of $\phi$ has at least ...
12
votes
2answers
680 views

Counting the number of satisfying assignments in a POSITIVE CNF-SAT

We know the problem of counting the number of satisfying assignment in a given general boolean formula (CNF-SAT), a given DNF formula, or even a given 2SAT formula is a #P-complete problem. Now, ...
5
votes
1answer
119 views

Reference request: complexity of $k$-partite $k$-SAT

Let's consider following variation of $k$-SAT that I will call $k$-partite $k$-SAT: given $n$ variables that are divided into $k$ groups and a $k$-SAT formula $\phi$ such that each clause has literal ...
7
votes
0answers
245 views

Given a Boolean formula, does there exist a small circuit that computes a satisfying assignment?

The 3-SAT problem can be defined as follows: 3-SAT Input: A 3-CNF formula $\phi$ of size $m$ with $n$ variables. Question: Does there exist a variable assignment that satisfies $\phi$? ...
42
votes
5answers
2k views

Theoretical explanations for practical success of SAT solvers?

What theoretical explanations are there for the practical success of SAT solvers, and can someone give a "wikipedia-style" overview and explanation tying them all together? By analogy, the smoothed ...
9
votes
0answers
294 views

What are the best known reductions from SAT to CNF-SAT?

Problems Let SAT denote the following problem: Given a boolean formula, does there exist a satisfying assignment? Let CNF-SAT denote the following problem: Given a ...
10
votes
1answer
243 views

Is bounded-width SAT decidable in logspace?

Elberfeld, Jakoby, and Tantau 2010 (ECCC TR10-062) proved a space-efficient version of Bodlaender's theorem. They showed that for graphs with treewidth at most $k$, a tree decomposition of width $k$ ...
3
votes
2answers
190 views

Hardness of finding roots of a degree $2$ polynomials over $\mathbb{F}_2$

Since every $3$-SAT instance with $n$ variables can be expressed as a degree-$3$ polynomial over $\mathbb{F}_2$ with $n$ unknowns, the NP-hardness of $3$-SAT directly translates to NP-hardness of ...
5
votes
0answers
75 views

Reference request for a $\Delta_2^P$ satisfiability problem

I am looking for the name and a reference for a $\Delta_2^P$-complete problem that looks like the following Input: A collection of CNF formulas $\phi_i(x_1^i, x_2^i,\dots, x_m^i, z_1, z_2, \dots, z_{...
12
votes
2answers
686 views

Is SAT a context-free language?

I am considering the language of all satisfiable propositional logic formulae, SAT (to ensure that this has a finite alphabet, we would encode propositional letters in some suitable way [edit: the ...
5
votes
0answers
278 views

How to do Type Inference using an SMT solver?

I understand that Hindley-Milner Type Inference can be implemented using an off-the-shelf SMT (Satisfiability Modulo Theories) solver? How would this work, for example for a very simple type system (...
7
votes
0answers
160 views

Converting a Truth Table into k-CNF formula of Minimal Size in Linear Time

Let $T$ be a truth table of a boolean function $f$ on $n$ input bits. More concretely $T$ could be a list of length $2^n$ such that $T[i] = f(bin(i))$, where $bin(i)$ is the binary representation of ...
4
votes
0answers
175 views

Subexponential algorithms vs separations

Williams (see also slide 29 here) has shown that an $\frac{2^{n}}{n^{10}}$ algorithm for satisfiability of circuits belonging to a class $\mathcal{C}$ imply that $\mathrm{NEXP}\nsubseteq \mathcal{C}$. ...
1
vote
1answer
587 views

Positive 1-in-3 SAT FPT or Fixed Parameter Intractable

There are a number of satisfiability problems that are difficult to solve even in the fixed parameter sense. For example, Weighted q-CNF Satisfiability is W[1]-complete when parameterized by the ...
28
votes
2answers
3k views

Do any quantum algorithms improve on classical SAT?

Classical algorithms can solve 3-SAT in $1.3071^n$ time (randomized) or $1.3303^n$ time (deterministic). (Reference: Best Upper Bounds on SAT ) For comparison, using Grover's algorithm on a quantum ...
4
votes
2answers
283 views

Questions regarding SETH

I read about the strong exponential time hypothesis, which states (as far as I understand) that SAT problem cannot be solved in running time $O(2^{\epsilon n})$ for any $\epsilon < 1$, where $n$ is ...
5
votes
1answer
267 views

Proof that the theory of rationals is convex

In Example 10.12 of the book The calculus of computation by Bradley and Manna, it is said The theory of rationals is convex, as it is convex in a geometric sense. How does the geometric sense of ...
-1
votes
1answer
125 views

Given oracle for Max-3SAT compute clauses that cannot be satisfied

We know that Max-3SAT is NP-hard to compute exactly (and also hard to approximate to a particular constant multiplicative factor). However, suppose you are given an oracle for Max-3SAT that tells you ...
4
votes
1answer
168 views

Asymptotic complexity of CDCL SAT solver that only selects negative literals

If a CDCL SAT solver only selects negative literals as decision literals (but can set positive literals through unit propogation) but has a perfect heuristic for determining which literal to select ...