Questions tagged [sat]
SAT stands for the Boolean satisfiability problem.
276
questions
6
votes
1answer
106 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 ...
1
vote
0answers
58 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 ...
1
vote
1answer
73 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 ...
4
votes
1answer
226 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 ...
3
votes
1answer
53 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 ...
0
votes
0answers
69 views
Hardness of approximation by reduction from MAX-E3SAT
For the MAX-E3SAT define $k=\sum_i^n (g_i-1)$, where $n$ is the number of variables and $g_i=\text{max}(\{\text{occurrences of }x_i, \text{occurrences of }\neg x_i\}), \text{ for each }i=\{1,\ldots,n\}...
3
votes
0answers
94 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 ...
1
vote
0answers
178 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 ...
3
votes
1answer
115 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 ...
5
votes
2answers
311 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, ...
-4
votes
1answer
126 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 ...
1
vote
0answers
72 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 ...
0
votes
0answers
20 views
Smallest/largest number of clauses, of the formula containing them being exact kCNF&there're r(or just r=1) satisfying assignment(s) with n variables?
When I try analysing the property of kCNF.
I meet a seemingly inessential problem that is more likely to be a combinatorial math problem.
What is the smallest/largest number of clauses where the ...
3
votes
2answers
154 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,...
1
vote
1answer
130 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 ...
9
votes
1answer
182 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 ...
1
vote
1answer
284 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)$?
3
votes
2answers
122 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 ...
8
votes
1answer
233 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
407 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
243 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
124 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
234 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 ...
8
votes
1answer
353 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
308 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
232 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)}$ ...
6
votes
0answers
260 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
45 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
161 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
95 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
80 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
248 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
110 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
116 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
141 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
56 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
88 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
76 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 ...
3
votes
0answers
57 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
102 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
80 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
123 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
37 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
324 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
110 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
531 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
128 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
68 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
121 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'...
