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 ...
