Different way of solving boolean satisfiability

I know there are commonly used boolean satisfiability problem-solving methods (such as DPLL etc.). As far as I know, such methods mostly depend on converting boolean expression into the CNF or DNF form. However, I’m trying to solve the given expressions “as-is”, without conversion to other forms. So, for boolean expression, I’m building a tree, consisting of many logical gates (AND, OR, NOT, XOR, VAR, CONST) and trying to propagate the right values by applying boolean laws.

step 1 – Common boolean laws

In such an approach there are some trivial steps like if AND has a value of 1 then the inputs must be both 1 and 1, or if XOR has a value of 1, and one input is 0, then the second input must be 1, etc. This step I call “propagation of values”, and it is performed until there are no values to resolve.

step 2 – Resolution by conflict

The second step is to assign value to the random gate, without a value assigned/resolved yet, name it X temporarily, then do “propagation of values”, and observe if in the expression tree some conflicts occurred. By conflict, I mean illegal state of the gate like AND(1,1)->0. So if the conflict occurred, this tells us that value assigned to the X gate is illegal, so I can assign the opposite value, and get back to the first step. This step I call “resolution by conflict”.

step 3 – Resolution by commons

The third step is to assign a value of 0 to the random gate, without a value assigned/resolved yet. Perform “propagation of values”, collect results (the assigned values of gates from the tree), in other words, do a “snapshot” of the tree after assignment. Then back to the original state before this step, assign a value of 1 to the same gate, perform propagation of values, then collect the second “snapshot”, then back to the original state again. Now, if the snapshots are both conflict-free, we could look at values that are both the same in the first and the second snapshot. These values are independent of the initial gate assignment and valid, so we can safely assign them to their gates. This step I call “resolution by commons”.

These steps were tested by me (program in C++) and worked pretty well.

Question

So, the question is, what other kinds of steps can apply for this kind of resolution / BSAT solving? I’m asking because there are still some problems that with these steps I can’t go further (algorithm with these steps “see” that is nothing to do more).

If something is unclear, please let me know in the comments. Also if such an approach is known I’ll be thankful for references or links to resources about the topic.

Boolean matrix / satisfiability problem [duplicate]

This question already has an answer here:

  • How to enumerate minimal covers of a set 2 answers

Let $ M$ be an $ m\times n$ matrix with all elements in $ \{1,0\}$ , $ m >> n$ . Let $ \mathbf{v}_0, \ldots, \mathbf{v}_n$ be the columns of $ M$ .

I want to find all sets of columns $ S = \{\mathbf{v}_{i_1}, \ldots, \mathbf{v}_{i_k}\}$ so that for every row there is at least one column $ \mathbf{v}_{i_j}, \ldots, \mathbf{v}_{i_k}$ that has a $ 1$ in that row, with the constraint that $ S$ is minimal in the sense that deleting any element of $ S$ means $ S$ no longer meets these requirements.

Without the minimalness constraint, this is a trivial instance of (monotone) SAT – define a variable corresponding to each column of $ M$ , and just read the CNF clauses from the rows of $ M$ .

How can I approach the problem as described? I tried encoding the minimalness requirement as additional boolean constraints (which would make the problem regular SAT and I could use a SAT solver), but this gives $ n^m$ additional clauses in CNF form, which is intractably large.

Reducing 3-CNFSAT to a particular satisfiability (PA-SAT) problem


The PA-SAT Problem:

PA-SAT is a satisfiability problem where the input is a boolean formula consisting of:

  • a conjunction of clauses, where each clause is either:
    • a disjunction of three boolean variables (without negations)
    • an equivalence between a boolean variable and a negated boolean variable.

Is it possible to satisfy the formula?.
An example of input to the problem is:

(x1 ∨ x2 ∨ x3) ∧ (x1 ∨ x3 ∨ x4) ∧ (x3 ∨ x4 ∨ x5) ∧ (x1 ∨ x5 ∨ x6) ∧ (x1 ≡ x̄5) ∧ (x5 ≡ x̄6)

Reduction:

I need to show that:

  • PA-SAT is NP-complete by showing that:
    • PA-SAT it is part of NP (PA-SAT ∈ NP)
    • PA-SAT is NP-Hard by showing that:
      • it is possible to design a polynomial karp-reduction of the NP-complete problem 3-CNFSAT to PA-SAT (3CNFSAT ≤ PA-SAT).

So my question is: How do I show that PA-SAT is NP-complete?

Can the following problem be reduced to each other to show that the satisfiability of the given boolean formular is NP hard?

Inspired by this problem: MIN-2-XOR-SAT and MAX-2-XOR-SAT: are they NP-hard?

I am interested to know whether or not if the satisfiability check of the following boolean expression is also NP-hard:

$ \bigwedge_{a\in V}\left(\bigvee_{b\in N[a]}(x_a\veebar x_b)\right)$

In the formula above $ V$ are formulas, $ N[a]$ is the set of neighbours of $ a$ a node from $ V$ . $ x\in\{0,1\}$ the formula above is satisfied when each node of type $ 0$ is adjacent to atleast one node of type $ 1$ and vice versa.

Satisfiability Toward A Sequential Circuit

Define a sequential circuit model be a directed graph with each vertices being a boolean gate. The difference is that we allow cycles in the boolean circuit. Each cycle will determine a boolean equation.

For example, constructing a loop by connecting the input and output of a negation gate will yield the equation $ x=\lnot x$ , which is not satisfiable. Given such circuit, the “satisfiability” in the sense naturally occur. My question is:

Is determining whether this circuit can be satisfied known to be hard or easy? Furthermore, is finding or enumerating these configuration known to be hard or easy?

First approach at checking 3×3 satisfiability is incorrect?

Suppose, I define a unique list of 9 elements. And permute them as follows. By following a circular shift to generate complete 9×9 Sudoku grids. Let’s permute [5,9,6,1,2,4,3,7,8]

[8, 5, 9, 6, 1, 2, 4, 3, 7]-----list 1 [7, 8, 5, 9, 6, 1, 2, 4, 3]-----list 2 [3, 7, 8, 5, 9, 6, 1, 2, 4]-----list 3 [4, 3, 7, 8, 5, 9, 6, 1, 2]-----list 4 [2, 4, 3, 7, 8, 5, 9, 6, 1]-----list 5 [1, 2, 4, 3, 7, 8, 5, 9, 6]-----list 6 [6, 1, 2, 4, 3, 7, 8, 5, 9]-----list 7 [9, 6, 1, 2, 4, 3, 7, 8, 5]-----list 8 [5, 9, 6, 1, 2, 4, 3, 7, 8]-----list 9 

Here, we follow the logic of the formula to generate the correct grid. Lets assume that LX follows sequential order.

L1 = list 1

L2 = list 2

L3 = list 3

L4 = list 4

(L1∧L2∧L3)∧(L4∧L5∧L6)∧(L7∧L8∧L9)

Following the formula we generate a 3×3 shift of a list of 9 unique elements to generate a Sudoku Grid.

enter image description here

Is my first approach at reducing satisfiability being implemented correctly?

Checking this algorthim

List of all possible reasoning tasks – satisfiability and theorem proving only?

What is the exhaustive list of reasoning tasks? As far as I can understand, then any logical reasoning reduces to 2 tasks only: 1) satisfiability problem (finding the assignment of the variables) and 2) theorem proving (deducing general statement from the other statements).

https://en.wikipedia.org/wiki/Logical_reasoning lists 3 types of reasoning: 1) deductive; 2) inductive; 3) analogical. But, as far as I understand, then each of those types reduces to some methods/heuristics of forming some statements and again – in the final step one of two reasoning tasks is applied – SAT or theorem proving.

Logic programming in essence if SAT problem as well (at least for stable model semantics/fixed poing semantics): one compiles the list of implicational statements and then tries to find the assignment of variables under which no internal dynamics happen further.

So – are there only those 2 reasoning tasks – SAT and theorem proving? Of course, there are many logics in which those tasks can be completed, but that is other problem, see, e.g. https://kwarc.info/people/frabe/Research/rabe_howto_14.pdf and https://uniformal.github.io/

The question is important when one tries to implement cognitive architecture (https://en.wikipedia.org/wiki/Cognitive_architecture and http://bicasociety.org/cogarch/architectures.php) – one should be sure about the exhaustive list or reasoning tasks to certify that some implementation achieves some generality.

My question is of even more important when one considers neural networks. One can ask – what is the exhaustive list of reasoning tasks that neural networks should be able to do? Of course, generally there are evidence about Turing completeness of neural networks, but my question concerns the cognitive/reasoning subset of general computations.

n-DNF boolean formula k satisfiability

Given an n variable boolean DNF formula and a number k, does this formula has satisfying input combination greater than k?. (0<=k<=2^n). Where input is infinite number of n tuples where repeating tuple is possible. For exampl. F(a,b) =ab + a’b. Input set is (11,00,11,01) and k=2. Answer is 3 here so decision says yes as 3>k. Can i define this problem in more formal way and prove that it is np/npc/ anything else. I am looking for suggestions specially for infinite number of tuples. I am aware of npc and reduction stuffs but need help to classify this problem properly.