Skip to main content
The 2024 Developer Survey results are live! See the results

Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

Filter by
Sorted by
Tagged with
0 votes
1 answer
510 views

Complexity of a variant of #Positive-2-SAT

#Positive-2SAT is the problem of counting the number of satisfying assignments to a given Positive 2-CNF formula i.e 2-CNF formulas in which each literal is a positive occurrence of a variable. The ...
2 votes
1 answer
89 views

Counting number of assignments restricted by implications

Suppose we have $n$ boolean variables, $x_1, \dots, x_n$. Some boolean variables can have implication relationships, e.g. $x_2 \implies x_5$, which means that if $x_2$ is true $x_5$ must also be true. ...
1 vote
1 answer
192 views

Best compression algorithm for CNF SAT instances in DIMACS

For a CNF SAT instance in the DIMACS format what is the best algorithm to compress it? What is the best algorithm for 3-SAT instances in particular? In 2020 SAT competition used .xz which if I ...
0 votes
0 answers
34 views

Minimum unsat core and generalization

I have a problem that has been in my head for some time, it might be already well known but i cannot find ressources on something similar : The idea came from the will to identify the minimal unsat ...
4 votes
1 answer
359 views

Is 3, 3 satisfiability trivial after all?

Tovey's paper from 1982 clearly states that: Theorem 2.1. Boolean satisfiability is NP-complete when restricted to instances with 2 or 3 variables per clause and at most 3 occurrences per variable. ...
1 vote
2 answers
42 views

Do stably-infinite theories exclude finite sorts?

Nelson-Oppen requires theories to be stably infinite. Meaning, that each theory allows extending models to have an infinite domain. A commonly mentioned counter example is that the theory of bit ...
1 vote
1 answer
26 views

Is stable infinity required of theories combined with model-based theory combination?

In the paper "Model-Based Theory Combination" (1) by De Moura and Bjorner they present an alternative to the Nelson-Oppen method for theory combination. They first describe the Nelson-Oppen ...
17 votes
3 answers
10k views

Prove NP-completeness of deciding satisfiability of monotone boolean formula

I am trying to solve this problem and I am really struggling. A monotone boolean formula is a formula in propositional logic where all the literals are positive. For example, $\qquad (x_1 \lor x_2) ...
4 votes
2 answers
998 views

Practical hard 3-sat instances

The $3-SAT$ problem is known to be NP-complete problem. Which means that (as far as I understand), unless $P \neq NP$, for every algorithm $A$ which decides $3-SAT$, $A$ runs in super polynomial time (...
3 votes
1 answer
44 views

File format for SAT competitions

The file format for SAT competitions is available online here: Rules of the 2011 SAT Competition but is defacto inaccessible because all browsers redirect to the non-existing address. Question: where ...
2 votes
1 answer
56 views

1-in-k-SAT problem restricted to only positive literals and at most two occurrences of a variable

1-in-k-SAT problem is to determine if there’s an assignment to variables such that every clause has exactly one true literal. Is this problem known to be in P when restricted to positive literals, and ...
0 votes
2 answers
167 views

Time complexity to convert a truth table to a boolean circuit

The SAT problem is often explained in terms of truth tables. Given some random boolean circuit, calculate its truth table; does there exist an output of $1$ in the truth table? But how about going the ...
2 votes
1 answer
27 views

Limited constant degree HamCycle

Let $G=(V,E)$ be a directed graph. I am interested in a "relaxed" version of the HamCycle problem. In my first case, the degree of each vertex is exactly 6, such that: 3 are outgoing edges ...
2 votes
1 answer
114 views

Proving satisfiability using resolution and variable elimination

I don't 100% understand this. But I have a entailment, and I want to prove whether it is satisfiable or not, and I will do this using resolution and variable elimination. Here is the formula: $$ (x_1 \...
1 vote
1 answer
47 views

Applications of a SAT Solver Oracle for Determining the Uniqueness of Solutions

I am exploring two kinds of model $𝑝_{𝑚,𝑛,k}$ and $S_{m,n,k}$ within the realm of satisfiability problems (SAT). Formal construction of $𝑝_{𝑚,𝑛,k}$ To construct the $𝑝_{𝑚,𝑛,k}$ model in ...
1 vote
1 answer
85 views

Logical Consequence - Equivalent Assertions

I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
0 votes
1 answer
89 views

Negating a Quantified Boolean Formula (QBF)

I'm reading about quantified boolean formulas. One sentence mentions: You should also verify that the negation of the formula $Q_1x_1\cdot\cdot\cdot Q_nx_n \phi(x_1, ..., x_n)$ is the same as $Q^{\...
1 vote
1 answer
102 views

Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?

I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ...
1 vote
0 answers
17 views

"package" compatibility solver with verion ranges

I am looking for how to solve the package compatibility problem. I have found some relevant research and libraries. But some of them are older. I am wondering if there is any more recent research and ...
1 vote
1 answer
95 views

A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?

I am working on an LRA Theory solver for SymPy, an open source python library for symbolic computations. You can find my work here. Currently I'm trying to optimize it to run faster. My implementation ...
0 votes
1 answer
89 views

Is it an open problem if CDCL algorithms violate SETH?

Strong Exponential Time Hypothesis states that general SAT, where clauses are not limited in length, can't be solved in time $o(2^n)$. It's proven that DPLL algorithm requires $\Omega(2^n)$ time in ...
1 vote
2 answers
55 views

Is there a linear programming method that is polynomial in the number of variables, constraints and bitlength of numbers?

AFAIK, Interior Point method for solving a system of linear inequations is polynomial in the number of variables and constraints. Probably there are others. I don't need to optimize any function (...
2 votes
0 answers
37 views

Satisfiability of a boolean formula with two occurrences of each variable with a special ordering

I am interested in the complexity of a special case of the boolean satisfiability problem: We are given a boolean formula, consisting only of the logical operators $\land$ and $\lor$ (that can be ...
0 votes
1 answer
161 views

Restriction of SAT to CNF

I have spent a lot of time understanding these two issues. If you can help me, please. Prove that the restriction of SAT to CNF formulas in which each variable xi appears at most twice is solvable in ...
1 vote
1 answer
26 views

Size of circuit generating the solutions of a SAT problem

We have a satisfiable CNF formula $F$ which maps $\{0,1\}^n \to \{0,1\}$. Let us call $S\in \{0,1\}^n$ the set of inputs that satisfy $F$, i.e. $F(s)=1 \, \forall s\in S$. There is a circuit $C$ with $...
1 vote
1 answer
12k views

To prove 4-SAT CNF is NP-complete [closed]

I'm looking to prove that 4-SAT, (which will be momentarily defined) is NP-complete. 4-SAT: Given a formula in Conjunctive Normal Form, where each clause contains exactly 4 literals, does it have a ...
0 votes
0 answers
17 views

Finding a common variable value among all SAT solutions

Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
1 vote
0 answers
15 views

Are there ASICs optimized to solve the SAT problem?

Are there ASICs (application-specific integrated circuits) optimized to solve the SAT problem, such as by the DPLL algorithm?
3 votes
2 answers
881 views

How to find a satisfying assignment in polynomial time without the use of randomness?

Assume that we are given a formula in 3-CNF such that at least 1% of the complete assignments satisfy it. My question is how to find a satisfying assignment in polynomial time without the use of ...
1 vote
1 answer
140 views

How to reduce 3SAT to TwoOrMoreSAT?

I want to prove, that 2OrMoreSAT is NP-complete. It's defined as follows: A formula is considered strongly satisfiable if there exists a model such that two or more different literals in every clause ...
0 votes
1 answer
73 views

P=NP? A reduction of CNF boolean satisfiability to the circulation problem in an undirected graph

The picture below shows how to reduce the Boolean Satisfiability problem in CNF to the circulation problem in undirected graph (see here). As you can see, a[i] are ...
0 votes
0 answers
14 views

Check if sum of positive integers is less than a W integer in CNF

As title says, what I am trying to do is to find a way to sum integers and later compare them with another integer W, in a manner that when the sum of integers is less or equal than W, using only CNF. ...
3 votes
1 answer
38 views

Is boolean formula equivalence problem for 2-CNFs $\mathsf{coNP}$-hard?

The problem: Given two boolean formulas in 2-CNF, decide if they are equivalent. I know that the problem is $\mathsf{coNP}$-hard when at least one formula is in 3-CNF. However, the same proof of $\...
0 votes
2 answers
37 views

how to polynomially check if a given boolean formula is unsatisfiable

Since SAT is np-complete, there is a polynomial algorithm to check if a given solution for any particular formula is correct. Just substitute the values and solve. But what if one claims that the ...
4 votes
1 answer
212 views

Tseitin formula on 2-connected graph

How can we prove that for $\\\\$ every $\\\\$ 2-connected graph G with an odd number of vertices, the unsatisfiable Tseitin formula for it is minimally unsatisfiable, that is, if we remove even a ...
1 vote
1 answer
51 views

Complexity of this variant of the Monotone(+,2−) -SAT problem?

In this post,Monotone$(+, 2^-)$-SAT problem is defined as follows: Given a monotone CNF formula $F^+$, where each variable appears exactly once (as a positive literal), and a monotone 2-CNF formula $...
1 vote
1 answer
132 views

Resolution on weakening rule by derived clause

How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule: $\frac{C} {C \vee D}$ (A clause $C$ is implied by $F$ if for ...
4 votes
1 answer
549 views

How to encode reachability in a graph with walls as a SAT problem

Suppose we have a graph that represents a grid of cells. We are given a cell to start in and a cell that's the destination. There are cells that we cannot enter and they are known as walls. Finally we ...
2 votes
1 answer
161 views

SAT solvers for counting the number of solutions

Are there existing SAT solver libraries that can count the number of solutions of a boolean formula? Can you give examples? I mean implementations more efficient than the naive approach, i.e. each ...
1 vote
0 answers
90 views

Sat solvers with backdoor set

I have large cnf with thousands of variables, but with known compact backdoor set. I think this set can be used by CDCL solvers to choose assignment variables to simplify formula much faster, but I ...
1 vote
1 answer
326 views

How fast can we make generalized k-SAT?

Suppose a generalized version of k-SAT where the usual clauses (disjunctions of literals) are generalized to arbitrary Boolean functions of k variables. (For example, $(x \oplus (y \land z)), ((x \...
2 votes
0 answers
76 views

Monotone boolean satisfiability problem : finding minimal solutions

I am very interested in the following questions, which sprang out from the topological study of loops in surfaces and their intersection numbers. Consider, over a finite set of boolean variables $X$, ...
4 votes
1 answer
196 views

SAT formulation of the condition that an even number of a given set of variables must be set to true

Lets say I have a SAT problem with variables $x_1,...,x_n$. For a given subset of the variables I want to create a clause which forces an even number of the variables in $S$ to be true. Of course ...
1 vote
1 answer
182 views

How to find the learned clause from a UIP cut

I would guess that this question is going to make some people wonder how I haven't already found a solution looking through papers -- but I do not see a clear algorithm. In implementing CDCL, I read ...
1 vote
1 answer
44 views

Is it possible to find reductions from problems in $\mathsf{NP}$ to SAT based solely on the certificate verification algorithm?

The following problem has made me ask this question: Given a boolean formula $\varphi(X)$ decide if there exists a quantification of $\varphi(X)$ with $k$ $\forall$ quantifiers that holds true. ...
1 vote
0 answers
23 views

CNF Horn-renamability to 3-CNF Horn-renamability reduction?

A CNF formula is Horn-renamable if you can invert variables in such a way that each clause has at most one positive literal. There is an algorithm based on a reduction to 2-SAT given in Renaming a Set ...
6 votes
0 answers
89 views

Is it possible to reduce functional equations to SAT?

The problem of finding a solution for functional equations can be defined as: Let $A_0, A_1, A_2, \dots, A_n, B_0, B_1, B_2, \dots, B_n, X$ be terms of the $\lambda$-calculus, where all terms are ...
1 vote
1 answer
117 views

Reduce CNF-SAT to decision problem

Given CNF-SAT reduce it to the following decision problem: Given n items, m groups (and for each group a set of items) and a ...
2 votes
4 answers
4k views

Resolution and what it means to derive the empty set

When using resolution, if the empty set {Ø} is derived from a formula like {¬x,¬y} {x,y}, does that mean the formula is unsatisfiable? If this is the case, why is ...
0 votes
0 answers
17 views

Does $\mathsf{NC_1\subsetneq NC}$ imply $\mathsf{NP\neq coNP}$?

Any $\mathsf{NC}$ circuit could be presented in SAT form via Tseytin transform. This applies in the reverse too: an arbitrary SAT instance could encode any $\mathsf{NC}$ circuit. Now, Frege proof ...

1
2 3 4 5
14