Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #2 to TR15-101 | 16th November 2015 10:23

On the structure of Solution-Graphs for Boolean Formulas

RSS-Feed




Revision #2
Authors: Patrick Scharpfenecker
Accepted on: 16th November 2015 10:24
Downloads: 1091
Keywords: 


Abstract:

In this work we extend the study of solution graphs and prove that for boolean formulas in a class called CPSS, all connected components are partial cubes of small dimension, a statement which was proved only for some cases in [Schwerdtfeger 2013]. In contrast, we show that general Schaefer formulas are powerful enough to encode graphs of exponential isometric dimension and graphs which are not even partial cubes.

Our techniques shed light on the detailed structure of $st$-connectivity for Schaefer and connectivity for CPSS formulas, problems which were already known to be solvable in polynomial time. We refine this classification and show that the problems in these cases are equivalent to the satisfiability problem of related formulas by giving mutual reductions between ($st$-)connectivity and satisfiability. An immediate consequence is that $st$-connectivity in (undirected) solution graphs of Horn-formulas is P-complete while for $2SAT$ formulas $st$-connectivity is NL-complete.


Revision #1 to TR15-101 | 10th August 2015 13:27

On the structure of Solution-Graphs for Boolean Formulas





Revision #1
Authors: Patrick Scharpfenecker
Accepted on: 10th August 2015 13:27
Downloads: 1145
Keywords: 


Abstract:

In this work we extend the study of solution graphs and prove that for boolean formulas in a class called CPSS, all connected components are partial cubes of small dimension, a statement which was proved only for some cases in [Schwerdtfeger 2013]. In contrast, we show that general Schaefer formulas are powerful enough to encode graphs of exponential isometric dimension and graphs which are not even partial cubes.

Our techniques shed light on the detailed structure of $st$-connectivity for Schaefer and connectivity for CPSS formulas, problems which were already known to be solvable in polynomial time. We refine this classification and show that the problems in these cases are equivalent to the satisfiability problem of related formulas by giving mutual reductions between ($st$-)connectivity and satisfiability. An immediate consequence is that $st$-connectivity in (undirected) solution graphs of Horn-formulas is P-complete while for $2SAT$ formulas $st$-connectivity is NL-complete.



Changes to previous version:

Added reference to FCT 2015 publication.
Clarified Corollary 5.
Corrected a typo in Corollary 6.


Paper:

TR15-101 | 15th June 2015 15:56

On the structure of Solution-Graphs for Boolean Formulas





TR15-101
Authors: Patrick Scharpfenecker
Publication: 19th June 2015 23:14
Downloads: 2223
Keywords: 


Abstract:

In this work we extend the study of solution graphs and prove that for boolean formulas in a class called CPSS, all connected components are partial cubes of small dimension, a statement which was proved only for some cases in [Schwerdtfeger 2013]. In contrast, we show that general Schaefer formulas are powerful enough to encode graphs of exponential isometric dimension and graphs which are not even partial cubes.

Our techniques shed light on the detailed structure of $st$-connectivity for Schaefer and connectivity for CPSS formulas, problems which were already known to be solvable in polynomial time. We refine this classification and show that the problems in these cases are equivalent to the satisfiability problem of related formulas by giving mutual reductions between ($st$-)connectivity and satisfiability. An immediate consequence is that $st$-connectivity in (undirected) solution graphs of Horn-formulas is P-complete while for $2SAT$ formulas $st$-connectivity is NL-complete.



ISSN 1433-8092 | Imprint