# Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

280 questions
Filter by
Sorted by
Tagged with
58 views

### Generating hard satisfiability problems with given constraint graph

Is there a systematic way to tune the hardness of a set of satisfiability problems (say 3-SAT or MAX2SAT) where the constraint graphs are always embeddable into a fixed given graph?
271 views

118 views

### Can a tractable sequence distribution prefer satisfying to unsatisfying assignments?

Let $p(x)$ be a Boolean circuit on $n$ bits $x \in \{0,1\}^n$. Consider a program that computes a probability distribution over all sequences $x$, autoregressively factored as \pi(x | p) = \prod_{0 ...
206 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 ...
59 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 ...
75 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 ...
229 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 ...
54 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 ...
70 views

476 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 ...
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 ...
127 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 ...
244 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 ...
359 views

235 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)}$ ...
261 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 ...
46 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 ...
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?...
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 ...
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 ...
249 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, ...
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 ...
117 views

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 ...
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. ...
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 ...
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 ...
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?
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 ...
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 ...
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. ...
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 ...
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 \$\...