liu.seSearch for publications in DiVA

References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt145",{id:"formSmash:upper:j_idt145",widgetVar:"widget_formSmash_upper_j_idt145",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt146_j_idt148",{id:"formSmash:upper:j_idt146:j_idt148",widgetVar:"widget_formSmash_upper_j_idt146_j_idt148",target:"formSmash:upper:j_idt146:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Exact Algorithms for Exact Satisfiability ProblemsPrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
PrimeFaces.cw("AccordionPanel","widget_formSmash_responsibleOrgs",{id:"formSmash:responsibleOrgs",widgetVar:"widget_formSmash_responsibleOrgs",multiple:true}); 2006 (English)Doctoral thesis, monograph (Other academic)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Institutionen för datavetenskap , 2006. , 177 p.
##### Series

Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1013
##### Keyword [en]

NP-hardness, exact algorithms, satisfiability, exact satisfiability
##### National Category

Computer Science
##### Identifiers

URN: urn:nbn:se:liu:diva-6907ISBN: 91-85523-97-6OAI: oai:DiVA.org:liu-6907DiVA: diva2:22042
##### Public defence

2006-06-01, Visionen, Hus B, Campus Valla, Linköpings universitet, Linköping, 13:15 (English)
##### Opponent

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt375",{id:"formSmash:j_idt375",widgetVar:"widget_formSmash_j_idt375",multiple:true});
##### Supervisors

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt381",{id:"formSmash:j_idt381",widgetVar:"widget_formSmash_j_idt381",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt387",{id:"formSmash:j_idt387",widgetVar:"widget_formSmash_j_idt387",multiple:true});
Available from: 2006-06-21 Created: 2006-06-21

This thesis presents exact means to solve a family of NP-hard problems. Starting with the well-studied Exact Satisfiability problem (XSAT) parents, siblings and daughters are derived and studied, each with interesting practical and theoretical properties. While developing exact algorithms to solve the problems, we gain new insights into their structure and mutual similarities and differences.

Given a Boolean formula in CNF, the XSAT problem asks for an assignment to the variables such that each clause contains exactly one true literal. For this problem we present an *O*(1.1730^{n}) time algorithm, where n is the number of variables. XSAT is a special case of the General Exact Satisfiability problem which asks for an assignment such that in each clause exactly i literals be true. For this problem we present an algorithm which runs in *O*(2^{(1-}*ε*^{) }*n*) time, with 0 < *ε* < 1 for every fixed *i*; for *i*=2, 3 and 4 we have running times in *O*(1.4511^{n}), *O*(1.6214^{n}) and *O*(1.6848^{n}) respectively.

For the counting problems we present an O(1.2190^{n}) time algorithm which counts the number of models for an XSAT instance. We also present algorithms for #2SAT*w** *and #3SAT*w**,* two well studied Boolean problems. The algorithms have running times in O(1.2561^{n}) and *O*(1.6737^{n}) respectively.

Finally we study optimisation problems: As a variant of the Maximum Exact Satisfiability problem, consider the problem of finding an assignment exactly satisfying a maximum number of clauses while the rest are left with no true literal. This problem is reducible to #2SAT*w* without the addition of new variables and thus is solvable in time *O*(1.2561^{n}). Another interesting optimisation problem is to find two XSAT models which differ in as many variables as possible. This problem is shown to be solvable in O(1.8348^{n}) time.

References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1080",{id:"formSmash:lower:j_idt1080",widgetVar:"widget_formSmash_lower_j_idt1080",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1081_j_idt1083",{id:"formSmash:lower:j_idt1081:j_idt1083",widgetVar:"widget_formSmash_lower_j_idt1081_j_idt1083",target:"formSmash:lower:j_idt1081:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});