Questions tagged [sat]
SAT stands for the Boolean satisfiability problem.
259
questions
1
vote
2answers
74 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 ...
7
votes
1answer
188 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
154 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
200 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
112 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
185 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 ...
6
votes
1answer
317 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
283 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
211 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)}$ ...
7
votes
0answers
240 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
43 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
133 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
93 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
77 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
238 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
96 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
108 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
129 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
46 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
85 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
75 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
53 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
95 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
77 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
119 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
36 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
265 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
104 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
527 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
114 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
52 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
111 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
169 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 ...
5
votes
0answers
193 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
614 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
94 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$ ...
5
votes
1answer
523 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
78 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
457 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
194 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 ...
3
votes
1answer
353 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
259 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 ...
13
votes
2answers
744 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
124 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
251 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$?
...
43
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
320 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
257 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$ ...
