Questions tagged [sat]
SAT stands for the Boolean satisfiability problem.
2
votes
1answer
83 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\...
-2
votes
0answers
47 views
Is there and efficient procedure to test whether a clause is implied by a given CNF formula?
I have a CNF formula $F$ and a clause $c$ defined on the same set of variables. I would like to know if $c$ is implied by $F$ i.e. if $F \vDash c$. To achieve this I could just test if the formula $F\...
8
votes
0answers
112 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
38 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 ...
0
votes
0answers
28 views
How to obtain a resolution derivation of a symmetric image of a clause from its resolution derivation
Suppose we have a CNF formula $F$ and a syntactic symmetry $\sigma$ of $F$. If we have a resolution derivation $( c_1, c_2, \cdots, c_n=c)$ of a clause $c$, then a resolution derivation of the clause $...
2
votes
0answers
79 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
68 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
47 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
77 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
72 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
112 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
33 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
208 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
86 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
494 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
95 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
48 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
101 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
139 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
172 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
515 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
85 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
255 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
72 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
455 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 ...
0
votes
0answers
46 views
Wavelet based Non linear optimization technique
I am outlining a method for solving Non Linear optimization problems.
Consider the system of equations:--------------------------------- 1
f1(a0, a1, a2, a3 ......... an) = 0
f2(a0, a1, a2, a3 ........
7
votes
1answer
183 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
233 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
201 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
254 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
632 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, ...
6
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 ...
8
votes
0answers
242 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
272 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 ...
11
votes
1answer
229 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
171 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 ...
6
votes
0answers
74 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_{...
13
votes
2answers
639 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 ...
4
votes
0answers
249 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 (...
8
votes
0answers
151 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
173 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
479 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
2k 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
274 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
210 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
118 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 ...
5
votes
1answer
154 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 ...
1
vote
1answer
419 views
Complexity of 3SAT where each pair of 3-clauses share at most one variable
Consider the variant of the 3SAT problem with the following restrictions:
Each clause has 2 or 3 literals.
Each pair of 3-literal clauses have at most one common variable.
What is the complexity of ...
