Questions tagged [satisfiability]

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

69 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
6
votes
0answers
141 views

Any Natural Problems shown Easy by Reduction to Horn SAT?

To show that a problem is polynomial-time solvable, an often-successful technique is to reduce it to 2SAT (that is the problem of deciding satisfiability of CNF formulas with every clause containing ...
5
votes
0answers
141 views

Approximate Weighted Partial Max SAT

Given a Weighted Partial Max SAT problem (WPM-SAT) - are there generally used algorithms or techniques to generate 'approximate' solutions, which are not necessarily optimal, but found faster than ...
4
votes
0answers
95 views

What is the generating algorithm for the “komb” instances found on satcompetition.org?

For the 2017 and 2018 Random SAT Tracks of the SAT Competition ran by the International Conference on Theory and Applications of Satisfiability Testing there are small, yet difficult, random 3-SAT ...
4
votes
0answers
42 views

Is there a correspondence of steps between DPLL and sequent-calculus?

Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid? And given ...
4
votes
0answers
70 views

(Historical perspective) CSP and SAT inter-fertilization

[Disclaimer: this is a rather specialized question] It is known that techniques like Conflict-Driven Clause Learning (CDCL) and back-jumping -- which improved the Satisfiability (SAT) strategies ...
3
votes
1answer
106 views

Polynomial-time linear-reduction from Directed Hamiltonian Path Problem to 3SAT

Is there a polynomial-time reduction from Directed Hamiltonian Path Problem to 3SAT which is linear in the number of vertices? That is, it reduces every directed graph $G$ with $n$ vertices to a ...
3
votes
0answers
81 views

Determine if a graph has exactly 1 cycle using a SAT solver

I have a connected undirected graph whose edges are either enabled or disabled. I want to create a set of clauses that are SAT iff all enabled edges are part of a single loop. If I assert that each ...
3
votes
0answers
68 views

relationship between SAT and Min-ones SAT

If SAT can be decided in polynomial time, is it clear that Min-ones SAT can be decided in polynomial time? The idea I had was to take a poly decider of SAT and try it on a formula OR'd with all ...
3
votes
0answers
52 views

What is complexity class for #XOR-2-SAT?

I know that given problem is in $\mathsf{FP}$: if given formula is satisfiable, then it is only needed to find out how many connected components equality (undirected) graph has. In fact problem is to ...
3
votes
0answers
534 views

SAT and TSP Problems

I am trying to build a tool for solving TSP problem using a conversion to SAT. Does there exist an efficient conversion from the Travelling Salesman Problem to the Satisfiability problem? Since they ...
3
votes
0answers
124 views

Solving systems of boolean equations

So I have a system of equations where varibles range over $\{0,1\}$ and the only operation is logical or ($\lor$). Each equation is of the one of two forms 1) $a = b \lor c$ 2) $1 = a \lor b$ where ...
3
votes
0answers
46 views

Knowing if I have an optimal ordering for a OBDD

I'm learning about OBDD and I have learned that the size of a reduced OBDD (ROBDD) is dependent on the ordering of the variables, and that finding an optimal ordering is an NP hard problem. Say I ...
3
votes
0answers
65 views

Results on number of solutions to random 3-SAT?

I'm looking for some published results, either empirical or theoretical, on the number of solutions to random 3-SAT problems. Given $N$ variables and a clause-to-variable ratio $\alpha$, how does the ...
3
votes
0answers
202 views

“Balancing” positive and negative literals in 2-sat

I saw in an answer to this post that it is possible to construct 3-sat clauses with extra variables such that the number of positive and negative literals for each variable are equal. Does anyone ...
3
votes
0answers
64 views

Parameterized complexity of Weighted Satisfiability with few variable occurrences

Given an integer $k$ and a Boolean CNF Formula $\phi$, Weighted Satisfiability asks whether $\phi$ is satisfiable by a model of weight $k$, i.e., a model that sets at most $k$ variables to true. This ...
3
votes
0answers
341 views

smallest satisfiability-equivalent formulas (generalized Tseitin transform)?

What is known about the following optimization problem for formulas in propositional logic: input: formula $F$ output: formula $G$ in CNF with $\mathrm{Var}(G) \supseteq \mathrm{Var}(F)$ such that ...
3
votes
1answer
287 views

Satisfiabililty sufficient condition?

The conjecture itself: k-SAT formula is satisfiable if no pair of unit assignment $l$ and $\overline l$ imply the formula to contain unsatisfiable (k-1)-SAT. Example (XOR-SAT has no edges and cycles ...
2
votes
1answer
108 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
0answers
130 views

Second Order QBF

Consider a universe with two elements 0,1 and a second order formula, i.e. of the form "forall R exists S ... such that F", where R,S are relation symbols of some given arity, and F is some first ...
2
votes
0answers
43 views

Is a “stacked”, “local” version of 3-SAT NP-hard?

In this previous question, I learned that if each variable in a string $C \in 3\text{-SAT}$ appears only "locally", then finding a satisfying assignment is no longer NP-hard. My question below builds ...
2
votes
2answers
185 views

Circuit satisfiability problem : SAT-C to SAT-2C

I have the following language : $L=\{\langle C_1,C_2\rangle \text{ | } C_1 \text{ and } C_2 \text{ are two circuits that calculate different function}\}$. We can call this language SAT-2C. Prove that ...
2
votes
0answers
23 views

Inapproximability result for a special version of 1-in-kSAT

Max 1-in-kSAT is the following maximisation problem : Given $n$ variables $x_1,\dots,x_n$, and $m$ clauses $C_1, \dots, C_m$, find a valuation such that the number of clauses satisfied by exactly one ...
2
votes
0answers
48 views

$X_3SAT$ Loop Reductions

Exactly $1$-in-$3$ SAT ($X_3SAT$) is a variant of the Boolean satisfiability problem. Given a set of clauses, each clause having three literals, is there a set of literals such that each clause ...
2
votes
0answers
124 views

Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
2
votes
0answers
51 views

substituting expressions

I have a set of expressions $E_1 .. E_n$ over boolean variables and I'm looking for an assignment to the variables so that all expressions are satisfied. Normally this would be NP-complete, but I ...
2
votes
0answers
204 views

Is Max-2SAT with exactly 3 occurrences per variable APX-hard?

The Max-2SAT problem asks if at least k clauses of a 2CNF formula can be satisfied. The Max-2SAT(at-most-3) problem is the restriction in which every variable occurs in at most 3 clauses (counting ...
2
votes
0answers
5k views

Reduction of 3-SAT to Vertex Cover?

Can someone explain to me in the simplest possible way, how to reduce $3SAT$ to $Vertex\:Cover$? I am following the explanation here (scroll to the bottom of page 4). I understand the basic setup of ...
2
votes
0answers
29 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
2
votes
0answers
717 views

DPLL time complexity analysis

Consider the most naïve backtracking for CNF-SAT. It only checks if an assignment satisfies the input formula $\phi$ when all the $n$ variables have values assigned. Let $m$ be the size of $\phi$. ...
1
vote
0answers
82 views

Class of languages recognizable by n-bit formulas of size at most $T(n)$

A Boolean (combinatoiral) circuit is a labeled (with the labels: AND, OR, NOT, IN, OUT), directed, acyclic graph, that satisfies: fan-in=2 for the AND and OR nodes fan-n=1 for the NOT nodes fan-...
1
vote
0answers
32 views

Are there any resources or forums online for helping me understand TAOCP?

Context I am doing an undergrad math project that involves exploring Donald Knuth's "TAOCP, Volume 4, fascicle 6: Satisfiability". I am having trouble parsing some of this material. Surely there ...
1
vote
0answers
100 views

Min-Ones-2-SAT getting to vertex cover

In the Min-Ones-2-SAT problem, we are given a 2-CNF formula φ and an integer k, and the objective is to decide whether there exists a satisfying assignment for φ with at most k variables set to true....
1
vote
0answers
145 views

Can someone give me the resolution procedure for 2 SAT, which is O (nˆ2)

According to Wikipedia, Even, S .; Itai, A .; Shamir, A. cited it in "On the complexity of time table and multi-commodity flow problems". The paper can be found here: http://www.cs.technion.ac.il/...
1
vote
0answers
123 views

The NP completeness proof for a variation of the 3CNF-SAT problem

There is a variation of 3CNF-SAT which is called 10-3-CNF-SAT = {<$\Phi$>: $\Phi$ is a satisfiable CNF formula with $\textbf{at most}$ 3 literals per clause and every variable occurs in $\textbf{at ...
1
vote
0answers
89 views

Can I use the Quine-McCluskey to simplify a CNF which is not a product of maxterms?

As I understand it the Quine-McCluskey method allows you to start with a set of maxterms (or minterms), and combine them pairwise in a systematic way into a smaller set of clauses with a smaller set ...
1
vote
0answers
192 views

Is the solution to Independent Set or Vertex Cover from 3-SAT optimum?

There are plenty of resources online discussing 3-SAT reductions to Independent Set or Vertex Cover problem. I am unable to find a resource which states that a satisfiable assignment to 3-SAT results ...
1
vote
0answers
101 views

What can be a Zero Knowledge Proof of a working SAT Algorithm?

Me and my colleague are exploring new ideas to solve SAT efficiently (i.e. in polynomial time) and it's the case that there is a candidate algorithm. Unfortunately, neither of us can write scripts ...
1
vote
0answers
120 views

General Understanding of SMT Solving Across Multiple Theories

My first question was a little too simplified in that it turned out to be an integer linear programming problem solvable with the Simplex Method. However, what I think I am wondering about is how to ...
1
vote
0answers
107 views

Correct implication for 3SAT from this theorem?

Theorem. Let none of the assignments of length $\log n$ make a set of unsatisfiable 2-clauses. Then formula is satisfiable. $n$ is input length here. Let we name an assignment that make the formula ...
1
vote
0answers
65 views

Why does the proof that #SAT is in IP stop after m rounds?

I've been struggling to understand why the interactive proof for #SAT stops after only $m$ rounds, where $m$ is the number of variables in the formula $\phi$. I understand that two polynomials of ...
1
vote
0answers
30 views

Heuristic Arguments against Existence of very inefficient alogirthm for SAT

I am reading the Handbook of Satisfiability and in the preface Martin Davis wrote Of course what is regarded as the most important problem in theoretical computer science, P = ? NP lives right ...
1
vote
0answers
74 views

Complexity Measure and Practical Hardness of SAT

I am study this paper "Relating Proof Complexity Measures and Practical Hardness of SAT". Here the authors propose to use pebble formulas to find a relation between these and practical SAT ...
1
vote
0answers
160 views

Proving the following chain of implications

I'm struggling with a proof in the text for my logic course, and I'm wondering if someone could offer a hint or some help. The question is basically as follows. Show that if the decision problem for ...
1
vote
0answers
42 views

How to get all tree-like refutations of a formula

I need to extract all tree-like refutations of this formula $$(a+b)(a+ b')(a'+c)(a'+c')\,.$$ I get understand this one but how do I get the other ones?
1
vote
0answers
67 views

Efficiently decidable logics

So propositional logic (PL) is efficiently (in P) decidable because I can convert formulas to an equisatisifiable CNF-formula, negate and convert (efficiently, by De Morgans laws) to DNF. I can then ...
1
vote
0answers
50 views

infinite system MAX-SAT

Is there a generalization of maximal satisfaction (MAX-SAT) based on infinitely many variables? One natural occurrence of such problem is the general Ising model in material science.
1
vote
0answers
72 views

How to reduce MaxUNSAT to MaxSAT in a (almost) direct way?

In question How to reduce MaxUNSAT to MaxSAT? I was asking, how to reduce the MaxUNSAT problem to MaxSAT. With help of the given answer I could give a polynomial reduction : $MaxUNSAT \leq ...
0
votes
0answers
59 views

Give me ideas for an undergraduate final year math project about Boolean Satisfiability and SAT solvers

Context I am a student starting an undergrad math project. I was instructed to read Donald Knuth's Fascicle 6: Satisfiability and come up with ideas for a project from this material. I have 13 weeks ...
0
votes
0answers
25 views

CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P

CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P. I found this solution: We use the method of resolution to take the variables out ...
0
votes
0answers
70 views

CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number of literals, but at most one negated literal} ∈ P

The problem derived from the book of Sipser and the question was already posted (link) with partial comments. Let CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number ...