As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
We address the problem of representing big sets of binary constraints compactly. Binary constraints in the form of 2-literal clauses are ubiquitous in propositional formulae that represent real-world problems ranging from model-checking problems in computer-aided verification to AI planning problems. Current satisfiability and constraint solvers are applicable to very big problems, and in some cases the physical size of the problem representations prevents solving the problems, not their computational difficulty. Our work is motivated by this observation.
We propose graph-theoretic techniques based on cliques and bicliques for compactly representing big sets of binary constraints that have the form of 2-literal clauses. An n, m biclique in a graph associated with the constraints can be very compactly represented with only n+m binary constraints and one auxiliary variable. Cliques in the graph are associated with at-most-one constraints, and can be represented with a logarithmic number of binary constraints. The clique representation turns out to be a special case of the biclique representation. We demonstrate the effectiveness of the biclique representation in making the representation of big planning problems practical.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.